fix(formal): restore TFunEff dev clobbered by #294 merge + fix Coq header syntax

Two problems on main, both from the #294 auto-merge (commit 49cac03
"resolve conflicts and fix headers"):

1. REGRESSION. main's branch carried an advanced effect-typed-lambda
   development (TFunEff: function types annotated with R_in/R_out,
   plus tfuneff_lambda_retype_l1_m / subst_typing_gen_l1_m_tfuneff —
   PRs #240/#249/#253). The #294 merge took the *older*
   proof/l2-modality branch's Semantics_L1.v / TypingL1.v
   (modality-migration, no TFunEff) over main's, clobbering
   Semantics_L1.v from 3737 -> 1644 lines while KEEPING main's
   TFunEff-bearing Syntax.v. Result: incoherent (non-TFunEff L1 proofs
   vs TFunEff Syntax) and the formal build broke.

   Fix: restore TypingL1.v, Semantics_L1.v, Counterexample.v to their
   pre-merge TFunEff versions (c07928f). main is coherent again.

2. BUILD-BREAK. The merge's header step injected a C-style
   `// Owner: …` line into every source file. `//` is not valid Coq
   (coqc: "illegal begin of vernac"), so all formal/*.v failed to
   parse; it also broke _CoqProject (coq_makefile: "Unknown option").

   Fix: convert the attribution line to the correct comment delimiter
   per file — `(* Owner: … *)` for .v, `# Owner: …` for _CoqProject /
   Justfile / .a2ml. This is a SYNTAX correction that preserves the
   attribution content; it is deliberately NOT a bulk attribution edit
   (the ~300 non-formal files the wholesale merge-revert would have
   stripped are left untouched).

Verification: `make -f build.mk clean && make -f build.mk` → exit 0,
all 12 modules compile. The remaining Print Assumptions axioms
(preservation_l1, step_pop_disjoint_from_type_l1,
region_shrink_preserves_typing_l1_gen_m, region_liveness_at_split_l1_gen)
are main's own documented TFunEff admits, unchanged by this commit.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Counterexample.v

@@ -1,7 +1,28 @@
-(* SPDX-License-Identifier: PMPL-1.0-or-later *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* SPDX-License-Identifier: MPL-2.0 *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
+(**
+
+  *********************************************************************
+  ***  📌 PINNED REGRESSION WITNESS                                   ***
+  ***                                                                ***
+  ***  5 Qed lemmas. Authoritative source of the 2026-05-26          ***
+  ***  soundness gap.                                                ***
+  ***                                                                ***
+  ***  This file SHOULD NOT BE WEAKENED. Any future proof work must  ***
+  ***  coexist with these lemmas. The legacy judgment's falsity is   ***
+  ***  load-bearing for the regression theorem; do not "fix" the     ***
+  ***  legacy judgment to make these lemmas fail.                    ***
+  ***                                                                ***
+  ***  bad_input_untypable_l1 is also Qed under BOTH modalities,     ***
+  ***  showing that the new L1 judgment closes the gap regardless of ***
+  ***  Linear vs Affine.                                             ***
+  ***                                                                ***
+  ***  See `STATUS.adoc`, `formal/PRESERVATION-DESIGN.md §1`.        ***
+  *********************************************************************
+
+*)
+
 (** * Soundness gap: counterexample to preservation as currently stated
 
     Exhibits a concrete configuration where the calculus's typing rules
@@ -173,8 +194,12 @@ Section L1Fix.
     inversion H; subst; split; reflexivity.
   Qed.
 
-  (** The L1 regression theorem: the bad input is untypable in EVERY
-      modality (linear and affine alike). *)
+  (** The L1 regression theorem.
+
+      Generalised to [forall m : Modality, ...] per L2: the bad
+      input is untypable in BOTH ephapax-linear AND ephapax-affine.
+      The inversion logic is mode-polymorphic — the region-threading
+      contradiction surfaces identically in both modes. *)
   Lemma bad_input_untypable_l1 :
     forall m R_out G_out,
       ~ has_type_l1 m (r0 :: r1 :: nil) nil e_bad T_bad R_out G_out.

formal/Counterexample_L2.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
 (** * Soundness gap (L2): preservation_l2 fails for TFunEff substituends

formal/Counterexample_L2_nested.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
 (** * Soundness gap (L2): preservation_l2 fails for nested-TFunEff

formal/Echo.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
 (**

formal/Justfile

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # Justfile for Ephapax Rocq proofs
 
 set shell := ["bash", "-euo", "pipefail", "-c"]

formal/L4.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
 (**

formal/Modality.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *)
 
 (**

formal/PROOF-STATUS.a2ml

@@ -1,5 +1,5 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # PROOF-STATUS.a2ml — machine-readable Coq proof state

formal/Semantics.v

@@ -1,5 +1,5 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+(* Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
 (* SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell *)
 
 (**