feat(L1): Phase D slice 4 Phase 2 — subst_typing_gen_l1_m_ground_nonlinear + helpers

[hyperpolymath]

Summary

Phase 2 of the non-linear substitution-lemma generalisation per formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md §"Phase 2". Builds on Phase 1's ground_nonlinear_retype_l1_m (#219).

Adds three pieces of NEW infrastructure to formal/Semantics_L1.v, all orthogonal to legacy preservation in Semantics.v:

1. Phase 1 generalisation

ground_nonlinear_retype_l1_m extended from (m monomorphic, G monomorphic) to (m → m', G → G')-polymorphic. The 3 ground typing rules (T_Unit_L1 / T_Bool_L1 / T_I32_L1) are themselves polymorphic in both, so the proof is unchanged. Phase 2 needs the cross-modality bridge to lift the Linear-typed Hv_type into the active modality m inside the substitution lemma's compound cases.

2. ground_nonlinear_value_shift_id_l1 helper

Ground non-linear values (EUnit / EBool b / EI32 n) are closed terms, so de Bruijn shift c d v = v for any c, d. Used to rewrite away the shift 0 1 vv that subst introduces when descending through term binders.

3. subst_typing_gen_l1_m_ground_nonlinear parallel lemma

forall m R Gin e T R' Gout,
  has_type_l1 m R Gin e T R' Gout ->
  forall k T1 v u_in,
    nth_error Gin k = Some (T1, u_in) ->
    is_value v ->
    is_ground_nonlinear_ty T1 = true ->
    R; remove_at k Gin |=L1 v : T1 -| R; remove_at k Gin ->
    forall u_out,
      nth_error Gout k = Some (T1, u_out) ->
      has_type_l1 m R (remove_at k Gin) (subst k v e) T R' (remove_at k Gout).

Mirrors subst_typing_gen_l1_m's 28+ case structure. Three key divergences from the linear lemma:

• T_Var_Lin_L1 with i = k0: rule's is_linear_ty T = true premise contradicts is_ground_nonlinear_ty Tsub = true (discharged via exfalso).
• T_Var_Unr_L1 with i = k0: CONSTRUCTIVE here (the symmetric case in the linear lemma is the exfalso branch). The substituted value vv is lifted from Linear into the active modality m via ground_nonlinear_retype_l1_m.
• Compound rules: ground_nonlinear_retype_l1_m replaces the linear_value_is_loc_l1 + loc_retype_at_R_l1_m + region_liveness_at_split_l1_gen pipeline. The retype takes any R', G', m', so no liveness side-condition is required.

Why this matters

Phase 2 unblocks:

• Phase 3: tfuneff_lambda_retype_l1_m + extend substitution to TFunEff T1 lambdas.
• Phase 4: close preservation_l2's T_App_L2_Eff β-case for ground non-linear T1 (in TFunEff T1 T2 R_in R_out lambdas with T1 ∈ {TBase TUnit, TBase TBool, TBase TI32}).

Ships as a sibling lemma rather than folding case-split into the existing subst_typing_gen_l1_m to preserve the ~30 Qed downstreams.

Owner-directive compliance

Per CLAUDE.md 2026-05-27:

• Does NOT close Theorem preservation in Semantics.v.
• Does NOT extend Semantics.v / Typing.v / Counterexample.v (all untouched).
• Does NOT close residual Semantics_L1.v admits via this work — strictly NEW infrastructure.
• Adds no new Axiom or Admitted declarations.

Test plan

• just clean && just all in formal/ — clean rebuild of all 10 .v files (coqc 8.18.0).
• Zero new admits/axioms (all proofs Qed).
• Semantics.v/Typing.v/Counterexample.v untouched.
• GPG-signed commit.
• STATE.a2ml next_action shifted to Phase 3.

Diff

• formal/Semantics_L1.v +322 (lemma + 2 helpers + doc comments)
• .machine_readable/6a2/STATE.a2ml +1/-1 (state journal advance)

Refs

Refs hyperpolymath/standards#134 (sub-issue of hyperpolymath/standards#124 estate proof-debt epic). Follows #219 (Phase 1). Phase 3 (TFunEff lambda retype) is the next slice.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 74 issues detected

Severity	Count
🔴 Critical	13
🟠 High	13
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in abi-verify.yml",
    "type": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence