proofs: Print Assumptions audit — certify which axioms each layer-keystone surfaces (closes P10/P32) (#270)

## Summary

Closes proof-debt P10/P32 from the comprehensive inventory. Adds `Print
Assumptions` blocks at the end of `formal/Semantics_L1.v` (9 lemmas) and
`formal/TypingL2.v` (6 lemmas) so the build oracle mechanically
certifies which axioms each layer-keystone theorem surfaces.

## Findings

### 🎯 Phase 3b Stage 1b ships ZERO-AXIOM

Both `subst_typing_gen_l1_m_tfuneff` and
`preservation_l2_app_eff_beta_tfuneff` print `Closed under the global
context`. The three side conditions (P1 leaf-only + P2 regions ⊆ R_in_v
+ P3 closed-below-0) make the proof go through without leaning on ANY
pre-existing structural admit. Empirical seal on the cleanliness of
Stage 1b.

### 🎯 L2 lift is exactly as advertised

`preservation_l2_via_l1` surfaces ONLY `preservation_l1` — certifies the
"L1-conditional lift" claim in `PROOF-NEEDS.md §1`.

### ⚠️ Soundness-leak alert

`preservation_l2_app_eff_beta_linear` AND `subst_typing_gen_l1_m` both
transitively depend on `region_liveness_at_split_l1_gen`, which is
**provably false as stated** in its residual `[binder = rv]` sub-case
(counterexample documented in source at `Semantics_L1.v:1923-1926`).
Closure requires Phase D reformulation, not direct proof — this is the
leak the `PROOF-NEEDS.md §4` falsity audit calls out. Mechanical capture
here means any future Qed silently accruing this axiom can't escape
notice.

### ✅ L3 drop-echo is clean

`preservation_l3_drop_echo` is zero-axiom; only `region_active_echo`
depends on `region_shrink_preserves_typing_l1_gen_m`.

## Full audit results

**`Semantics_L1.v` block:**

| Lemma | Surfaces |
|---|---|
| `ground_nonlinear_retype_l1_m` | (none) |
| `tfuneff_lambda_retype_l1_m` | (none) |
| `subst_typing_gen_l1_m` | `region_liveness_at_split_l1_gen` |
| `subst_typing_gen_l1_m_ground_nonlinear` | (none) |
| `subst_typing_gen_l1_m_tfuneff` | (none) ⭐ |
| `preservation_l1` | `preservation_l1` (self — outer Admitted) |
| `preservation_l3_region_active_echo` |
`region_shrink_preserves_typing_l1_gen_m` |
| `preservation_l3_drop_echo` | (none) |
| `preservation_l3` | `region_shrink_preserves_typing_l1_gen_m` |

**`TypingL2.v` block:**

| Lemma | Surfaces |
|---|---|
| `weaken_modality` | (none) |
| `preservation_l2_via_l1` | `preservation_l1` |
| `linear_value_retype_l1_m` | (none) |
| `preservation_l2_app_eff_beta_linear` |
`region_liveness_at_split_l1_gen` |
| `preservation_l2_app_eff_beta_ground_nonlinear` | (none) |
| `preservation_l2_app_eff_beta_tfuneff` | (none) ⭐ |

## Test plan

- [x] Local Coq build oracle green (`just -f formal/Justfile all`)
- [x] Output captured in build log; CI artefacts will preserve it
- [x] Zero new admits / axioms / Admitted; pure observation lemmas

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Semantics_L1.v

@@ -3265,3 +3265,47 @@ Proof.
   - exact preservation_l3_region_active_echo.
   - exact preservation_l3_drop_echo.
 Qed.
+
+(* ============================================================
+   Print Assumptions audit — L1 + L3 axiom inventory
+   ============================================================
+
+   Companion to the L2-side audit at the end of TypingL2.v.
+   Closes proof-debt P10/P32: certify exactly which axioms each
+   layer-keystone theorem surfaces, mechanically.
+
+   Expected per the design:
+
+   - [region_shrink_preserves_typing_l1_gen_m]  Admitted at
+     :678 → surfaces itself as an axiom (its outer Admitted is
+     listed). Once the list-vs-multiset gap closes, this drops.
+
+   - [region_liveness_at_split_l1_gen]  Admitted at :2028 →
+     surfaces itself. Provably-false-as-stated in the residual
+     [binder = rv] sub-case (counterexample documented in source
+     at :1923-:1926); closure requires Phase D reformulation.
+
+   - [preservation_l1]  Admitted at :3133 → surfaces itself plus
+     any structural debt its conditional Qed-portion already
+     pulls in.
+
+   - [preservation_l3] / [preservation_l3_region_active_echo] /
+     [preservation_l3_drop_echo]  surface
+     [region_shrink_preserves_typing_l1_gen_m] only (the L1
+     structural admit they're conditional on). [drop_echo] is
+     additionally expected to be axiom-free (it doesn't traverse
+     region-shrink).
+
+   - [subst_typing_gen_l1_m_tfuneff] (Phase 3b Stage 1b) should
+     be zero-axiom under its three side conditions (P1+P2+P3) —
+     this is the cleanliness claim of Stage 1b. *)
+
+Print Assumptions ground_nonlinear_retype_l1_m.
+Print Assumptions tfuneff_lambda_retype_l1_m.
+Print Assumptions subst_typing_gen_l1_m.
+Print Assumptions subst_typing_gen_l1_m_ground_nonlinear.
+Print Assumptions subst_typing_gen_l1_m_tfuneff.
+Print Assumptions preservation_l1.
+Print Assumptions preservation_l3_region_active_echo.
+Print Assumptions preservation_l3_drop_echo.
+Print Assumptions preservation_l3.

formal/TypingL2.v

@@ -693,3 +693,51 @@ Proof.
     eapply preservation_l2_app_eff_beta_tfuneff_l1; eassumption.
   - exfalso. inversion Hval.
 Qed.
+
+(* ============================================================
+   Print Assumptions audit — L2 lift honest-ness seal
+   ============================================================
+
+   Closes proof-debt P10/P32 (per the PROOF-NEEDS.md inventory):
+   formally certify which axioms / Admitted lemmas surface through
+   each L2 β-case and the lift theorem. Without this audit, the
+   "L2 lift is honest" claim in PROOF-NEEDS.md §1 ("conditional on
+   preservation_l1") is unverified — `Print Assumptions` is the
+   build oracle for that claim.
+
+   Expected (per the design):
+
+   - [preservation_l2_via_l1]  surfaces [preservation_l1] only.
+     This is the canonical L1-conditional lift; no other axioms.
+
+   - [preservation_l2_app_eff_beta_linear]  surfaces structural
+     L1 admits via [subst_typing_gen_l1_m] +
+     [region_shrink_preserves_typing_l1_gen_m].
+
+   - [preservation_l2_app_eff_beta_ground_nonlinear]  surfaces
+     [ground_nonlinear_retype_l1_m] + structural L1 admits.
+
+   - [preservation_l2_app_eff_beta_tfuneff]  surfaces Phase 3b
+     Stage 1b machinery + the three side conditions (P1 leaf-only,
+     P2 regions ⊆ R_in_v, P3 closed-below-0) + structural L1
+     admits.
+
+   - [weaken_modality]  zero axioms.
+
+   - [linear_to_affine] (TypingL1.v)  zero axioms.
+
+   Verifying these mechanically means a future Qed silently
+   accruing an undocumented Axiom (the historical anti-pattern
+   that produced the legacy [region_liveness_at_split_l1] axiom)
+   would be caught at the next [Print Assumptions] re-run.
+
+   Build-oracle conformance: `just -f formal/Justfile all` prints
+   these blocks at compile time; CI (coq-build.yml) preserves
+   them in the artefacts. *)
+
+Print Assumptions weaken_modality.
+Print Assumptions preservation_l2_via_l1.
+Print Assumptions linear_value_retype_l1_m.
+Print Assumptions preservation_l2_app_eff_beta_linear.
+Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear.
+Print Assumptions preservation_l2_app_eff_beta_tfuneff.