{{ message }}
proof(entropy): entropy-blind-parametric — parametric-distribution non-distinguishing#261
Merged
Merged
Conversation
…n-distinguishing Generalises EchoEntropy's discrete fibre-count blindness (Headline 3, entropy-shadow-blind, a function of a single ℕ count) to the parametric form the companion remark flagged open: any information functional H : (Fin 2 → W) → X of any fibre-determined distribution over the fibre of collapse at tt agrees on echo-true and echo-false (entropy-blind-parametric), paired with the matched-negative that a witness-determined distribution distinguishes (entropy-witness-distinguishes, via sigma-distinguishes). The non-distinguishing now holds for ANY real-/rational-/abstract-valued entropy, Renyi entropy or mutual-information functional once supplied — no reals/log library needed, the blindness is structural. Constructing a concrete real-valued H(P) = -Sigma p log p remains an orthogonal reals+logarithm task, independent of Echo, and is deliberately not attempted. Verified: agda proofs/agda/Smoke.agda + proofs/agda/All.agda exit 0 under --safe --without-K, zero postulates, no funext. Both headlines pinned in Smoke.agda. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG
🔍 Hypatia Security ScanFindings: 6 issues detected View findings[
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/echo-types/echo-types",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
"type": "StaticAnalysis",
"file": "/home/runner/work/echo-types/echo-types",
"action": "auto_fix",
"rule_module": "scorecard",
"severity": "medium",
"remediation": "Add CodeQL or equivalent SAST workflow.",
"scorecard_check": "SAST"
},
{
"reason": "Repository has 7 non-main remote branch(es). Policy: single main branch only.",
"type": "GS007",
"file": ".",
"action": "delete_remote_branches",
"rule_module": "git_state",
"severity": "medium"
},
{
"reason": "Code scanning (Scorecard): TokenPermissionsID -- Token-Permissions -- 18 day(s) old [STALE]",
"type": "CSA001",
"file": ".github/workflows/scorecard.yml",
"action": "escalate",
"rule_module": "code_scanning_alerts",
"severity": "high"
},
{
"reason": "Code-scanning alert TokenPermissionsID (high) at .github/workflows/scorecard.yml is 18 days old (threshold: 7 days) -- overdue for remediation",
"type": "CSA003",
"file": ".github/workflows/scorecard.yml",
"action": "escalate",
"rule_module": "code_scanning_alerts",
"severity": "high"
},
{
"reason": "Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' -- ensure dismissal is documented and justified",
"type": "CSA004",
"file": "proofs/agda/EchoImageFactorizationPropPostulated.agda",
"action": "review",
"rule_module": "code_scanning_alerts",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
3 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the Echo-relevant half of the one genuinely-open Agda obligation in the repo — the
EchoEntropycompanion remark's "real-valued / parametric-distribution" item — at the honest scope.What lands
Two new headlines in
EchoEntropy.agda, in the module's own positive + matched-negative idiom:entropy-blind-parametric(positive, parametric).entropy-shadow-blind(Headline 3) only covered any function of the fibre count — a singleℕ. This generalises to any information functionalH : (Fin 2 → W) → Xof a fibre-determined distributionPover the fibre ofcollapseattt: it agrees onecho-trueandecho-false. The fibre is shared by both echoes, so a distribution read off the fibre (not the witness) doesn't mention the echo — blindness is structural. This covers any real-/rational-/abstract-valued entropy, Rényi entropy, or mutual-information functional the moment one is supplied.entropy-witness-distinguishes(matched-negative). A witness-determined distribution (the point-mass carryingproj₁ sigma-distinguishes e) does separate the two echoes under a sampling functional. Blindness ⟺ fibre-determined; distinguishing ⟺ witness-determined — mirroring the discrete result's fibre-vs-witness split.Honest scope (deliberately not over-claimed)
The construction of a concrete real-valued
H(P) = -Σ p log pis not attempted: it needs a reals + logarithm formalisation, which is an analysis task orthogonal to Echo (not aProbability-interface gap), and faking it would breach the zero-postulate discipline. The point is that the non-distinguishing — the only Echo-side content — now holds for any such functional regardless. The module header (scope guardrail + headline list) and companion remark are updated to say exactly this.Verification
agda proofs/agda/EchoEntropy.agda→ exit 0agda proofs/agda/Smoke.agda→ exit 0 (both new headlines pinned)agda proofs/agda/All.agda→ exit 0--safe --without-K, zero postulates (grep-checked), no funext, no escape pragmas.🤖 Generated with Claude Code
https://claude.ai/code/session_01PWMMxryCcPrAjJ8tuGvygG
Generated by Claude Code