feat: forget-witness-encoding-has-section — universal LL-encoding gap

[hyperpolymath]

What

Closes the universal LL-encoding gap that EchoLLEncoding flagged in its companion remark — strengthening the existence theorem ll-encoding-gap (the trivial ⊤-shadow) to a universal statement over the forget-witness class.

How

The encoded analogue of no-section-weaken was shown to fail for one encoding. It actually fails for the whole class of witness-forgetting shadows:

ForgetsWitness E = (x y : X linear) → x ≡ y          -- X linear is a proposition

forget-witness-encoding-has-section :
  (E : LLShallowEncoding) → ForgetsWitness E →
  Σ (X affine → X linear) (λ s → ∀ x → s (wX x) ≡ x)

The section is the constant map at a fixed linear inhabitant enc echo-true, correct because forget-witness propositionality makes every X linear element equal to it — uniform over the class, no cherry-picked carrier. Two companions:

• trivial-forgets-witness — the ⊤-shadow is a member (⊤ is a proposition);
• trivial-via-universal — the original existence form is recovered as the universal one instantiated at the trivial encoding (the generalisation is checked, not asserted).

The sharpened dichotomy

• Forget the witness (X linear a proposition) ⇒ an encoded section always exists — universal.
• Keep the witness (re-introduce the second-projection equality into X linear, so it isn't a proposition) ⇒ no-section may be preserved, but the encoding is then no longer the standard !A := 1 LL shadow.

So the only way a shallow LL encoding can carry Echo's no-section discipline is to stop being a witness-forgetting shadow. Header headline list, scope guardrail, and companion remark updated to state both strengths honestly.

Discipline

• --safe --without-K, zero postulates.
• 4 Smoke pins; EchoLLEncoding already classified (lemmas added, no new module) ⇒ kernel-guard PASS.
• Verified on latest main: EchoLLEncoding.agda, Smoke.agda, All.agda all exit 0 (captured locally).

🤖 Generated with Claude Code

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 6 issues detected

Severity	Count
🔴 Critical	0
🟠 High	3
🟡 Medium	3

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 8 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