docs: port §4.8.1 + §5.1 + L1 admit enumeration to main

[hyperpolymath]

Summary

Brings three doc-only improvements from the (now-superseded) design branch onto main. All are pure documentation; no source/proof changes.

What this PR adds

1. PRESERVATION-DESIGN.md §4.8.1 (from design-branch PR #170)

Records that path (3) — T_Var_*_L1 strengthening — landed via the m-indexed has_type_l1 in #176. Documents what it closes (source-level variable soundness gap) and what it does not (the lambda-rigidity gap in S_App_Step2 / S_Pair_Step2).

2. PRESERVATION-DESIGN.md §5.1 (from design-branch PR #172)

L1's lambda-rigidity gap closes at L2 Phase 2 via effect-typed TFun, not at L1. Documents:

• The §5 table's "✓ (L1 fix)" cell flagged with (*conditional on §5.1*).
• Why path (3) (T_Var strengthening) is necessary-not-sufficient.
• Proposed effect-typed TFun signature: TFun T1 T2 (R_in : region_env) (R_out : region_env).
• Why effect-typing is L2's job (typing-layer concern, not region-layer).
• Sequencing: L2 Phase 2 follow-up to current T_Lam_L1_* rules.

3. docs/proof-debt.adoc — L1 admit enumeration (from design-branch PR #169)

Adds the eight current escape-hatch sites in Semantics_L1.v listed by file:line per the standards#203 trusted-base policy substring-match convention:

• L343, L400, L412, L520 (region-shrink admits)
• L608 (Axiom region_liveness_at_split_l1)
• L632 (preservation_l1 Admitted)
• L703 / L704 (lambda-rigidity admit + Admitted)

Plus the Echo.v K-closure note (from PR #173's main re-port).

Why this matters

Three independent improvements that the parallel-session #176 bundling didn't include. Each is small enough to ship as part of a single docs cleanup:

• §4.8.1: makes the §4.8 status accurate post-proof(L1.G): strengthen T_Var_*_L1 with region well-formedness (§4.8 path 3) #170/proof(L2): hybrid — has_type_l1 m-indexed + Modality.v + linear_to_affine Qed (zero axioms) #176 landing.
• §5.1: makes the §5 table honest about the lambda-rigidity gap.
• proof-debt.adoc: enables trusted-base reduction policy check to substring-match all current L1 escape-hatch sites by file:line.

Companion PRs

• proof(L3.K): rewrite Echo.v K-free — eliminate eq_rect_eq dependency #180 — K-free Echo.v rewrite (port of design-branch proof(L3.K): rewrite Echo.v K-free — eliminate eq_rect_eq dependency #173). No conflict with this PR.
• proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit #181 — Axiom→Lemma conversion for region_liveness_at_split_l1 (port of proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit #178, adapted to m-indexed has_type_l1). When proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit #181 lands, the L608 Axiom entry in this PR's proof-debt.adoc will become stale — follow-up doc tweak to update the line numbers post-proof(L1.G): convert Axiom region_liveness_at_split_l1 to Lemma with 1 narrow admit #181.

Test plan

• Asciidoc / Markdown lints (renders in GitHub preview)
• All eight current L1 escape-hatch sites covered by file:line substring matches
• §4.8.1 + §5.1 wording matches the design-branch versions
• CI green (the doc changes shouldn't trigger any Coq build steps)

Refs design-branch PRs #169 / #170 / #172 / #173, PR #176 (L2 hybrid), PRs #180 and #181 (companion).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 38 issues detected

Severity	Count
🔴 Critical	9
🟠 High	10
🟡 Medium	19

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Admitted leaves proof hole (12 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (6 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics_L1.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "Admitted leaves proof hole (3 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Coq admit tactic leaves goal unproven (7 occurrences, CWE-704)",
    "type": "coq_admit_tactic",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (1 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/ephapax/ephapax/src/ephapax-repl/src/lib.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence