hyperpolymath · Nov 5, 2026 · Nov 5, 2026 · Nov 5, 2026 · Nov 5, 2026
@@ -16,10 +16,9 @@
 # `coq_makefile`-driven compilation of `formal/_CoqProject` fails
 # here BEFORE the admin-merge button is reachable for the auto-bot.
 #
-# The job also `Print Assumptions`-checks the four Phase D top-level
-# results (preservation_l1 at L1; preservation_l2_via_l1 plus the two
-# β-case lemmas at L2) so any new `Admitted.` / `Axiom` slippage shows
-# up as a diff in the workflow output.
+# The job also runs the no-False gate: no `Admitted.` / `Axiom` /
+# `Parameter` in any `_CoqProject` file, and the refutations plus the
+# conditional L2 results must print "Closed under the global context".
 #
 # **Why an aggregator gate?** The `coq-build` job is path-filtered: it
 # only does real work when `formal/**` or this workflow file changes.
@@ -128,26 +127,40 @@ jobs:
           coq_makefile -f _CoqProject -o build.mk
           make -f build.mk
 
-      - name: Print Assumptions of Phase D theorems
+      - name: No-False gate (D0/D0b, owner-ratified 2026-11-05)
         working-directory: formal
         run: |
-          # Surfaces any new Admitted / Axiom additions feeding into
-          # the four Phase D top-level results. A diff in this output
-          # between PRs is the canonical "did this PR introduce a new
-          # admit" signal.
-          #   preservation_l1                                (Semantics_L1.v)
-          #   preservation_l2_via_l1                         (TypingL2.v)
-          #   preservation_l2_app_eff_beta_linear            (TypingL2.v, #228)
-          #   preservation_l2_app_eff_beta_ground_nonlinear  (TypingL2.v, #233)
-          # Single coqtop session amortises ML startup across four prints.
-          coqtop -R . Ephapax 2>&1 <<'EOF' | tail -160
-          From Ephapax Require Import Semantics_L1.
-          From Ephapax Require Import TypingL2.
-          Print Assumptions preservation_l1.
+          # The build is axiom-free: no `Admitted.` and no `Axiom` /
+          # `Parameter` in any `_CoqProject` file. While a refuted
+          # statement was `Admitted`, the build could derive `False`
+          # (see docs/reports/2026-11-04-v2-survey, F0/F1). Assuming
+          # Coq's own consistency, an axiom-free build cannot.
+          set -euo pipefail
+          FILES=$(grep -E '\.v$' _CoqProject)
+          if grep -nE '^[[:space:]]*(Admitted\.|Axiom[[:space:]]|Parameter[[:space:]])' $FILES; then
+            echo "no-False gate: Admitted/Axiom/Parameter found above -> FAIL"
+            exit 1
+          fi
+          # Every headline and refutation must be closed under the global
+          # context; any `Axioms:` block fails the gate.
+          OUT=$(coqtop -R . Ephapax 2>&1 <<'EOF2'
+          From Ephapax Require Import Semantics Semantics_L1 TypingL2.
+          From Ephapax Require Import Counterexample Counterexample_StepPop Counterexample_PreservationL1.
+          Print Assumptions Counterexample.preservation_false.
+          Print Assumptions Counterexample_StepPop.step_pop_disjoint_from_type_l1_FALSE.
+          Print Assumptions Counterexample_PreservationL1.preservation_l1_FALSE.
           Print Assumptions preservation_l2_via_l1.
           Print Assumptions preservation_l2_app_eff_beta_linear.
           Print Assumptions preservation_l2_app_eff_beta_ground_nonlinear.
-          EOF
+          EOF2
+          )
+          echo "$OUT" | tail -60
+          if echo "$OUT" | grep -qE '^Axioms:|Error'; then
+            echo "no-False gate: a printed result depends on an axiom, or coqtop errored -> FAIL"
+            exit 1
+          fi
+          test "$(echo "$OUT" | grep -c 'Closed under the global context')" -eq 6
+          echo "no-False gate: PASS (0 Admitted, 0 Axiom, 6/6 closed)"
 
   # Always-on aggregator. This is the ONLY job listed in the Base ruleset's
   # required_status_checks rule (#244). If detect-relevant-changes determined

@@ -100,7 +100,18 @@ redesign and state sound replacement theorems, not to prove refuted ones.
 - **Proof, L4** — Phase A scaffold landed; mother–child dyadic
   semantics (`PRESERVATION-DESIGN.adoc §7`) is the next design step.
 
-## 🛑 Owner directive snapshot (2026-05-27) — legacy fence plus later L1 regressions
+## 🛑 Owner directive snapshot (2026-05-27, revised 2026-11-05) — legacy fence plus later L1 regressions
+
+> **2026-11-05 revision (owner-ratified D0 and D0b).** The three refuted
+> statements are retired, not closed: `Semantics.preservation` is now
+> `preservation_stmt : Prop`, refuted by `Counterexample.preservation_false`;
+> `step_pop_disjoint_from_type_l1` and `preservation_l1` are now
+> `…_stmt : Prop`, refuted by `Counterexample_StepPop.v` and
+> `Counterexample_PreservationL1.v`. While they were `Admitted`, the build
+> could derive `False`. `formal/` now has **0 `Admitted` and 0 `Axiom`**,
+> and CI's no-False gate (`coq-build.yml`) blocks any new
+> `Admitted`/`Axiom`/`Parameter`. The fence below is unchanged in spirit:
+> never try to prove a refuted statement.
 
 > The guardrails below protect pinned counterexamples and the false
 > statements they refute. They do **not** mean "skip this repo." The
@@ -113,10 +124,10 @@ redesign and state sound replacement theorems, not to prove refuted ones.
 Ephapax preservation as originally stated in `formal/Semantics.v` is
 **provably false** — and that is a *result*, not a defeat:
 `formal/Counterexample.v` exhibits a concrete configuration that types,
-steps, and lands at an untypable post-state (5 lemmas `Qed`), which
+steps, and lands at an untypable post-state (now 6 lemmas `Qed`, incl. `preservation_false`), which
 named an invariant missing from the legacy judgment. So the work is **not**
-to close `Theorem preservation` in `Semantics.v` (no closure exists; the
-`Admitted` is deliberate). Nor should the current unrestricted L1
+to close the legacy preservation in `Semantics.v` (no closure exists; it
+is retired to `preservation_stmt : Prop`, refuted by `preservation_false`). Nor should the current unrestricted L1
 preservation be treated as routine debt: `Counterexample_StepPop.v` and
 `Counterexample_PreservationL1.v` refute its supporting claim and capstone.
 There is no unconditional L2 preservation theorem; the L2 β-case helpers
@@ -130,9 +141,11 @@ counterexample and state any replacement theorem with its exact boundary.
 These are anti-patterns that have wasted real session time. Refuse
 them if asked; if asked anyway, push back and link this section.
 
-1. **DO NOT close `Theorem preservation` in `formal/Semantics.v`.**
-   It is FALSE. No proof technique closes it because no proof
-   exists. The `Admitted.` is correct.
+1. **DO NOT prove or restate the legacy preservation in
+   `formal/Semantics.v`.** It is FALSE and is refuted by
+   `Counterexample.preservation_false`. It stays `preservation_stmt : Prop`;
+   never turn it back into a `Theorem`/`Lemma`, and never re-add an
+   `Admitted.` for it.
 
 2. **DO NOT extend `formal/Semantics.v`** with new lemmas aimed at
    closing the legacy preservation: not Lemma B variants
@@ -144,10 +157,12 @@ them if asked; if asked anyway, push back and link this section.
    invariant the counterexample demands; no lemma collection bolted
    onto it will help.
 
-3. **DO NOT try to complete the current unrestricted
-   `step_pop_disjoint_from_type_l1` or `preservation_l1` statements in
-   `formal/Semantics_L1.v`.** Both are refuted by pinned witnesses; their
-   `Admitted.` markers are transparent boundaries, not ordinary debt.
+3. **DO NOT try to prove the unrestricted
+   `step_pop_disjoint_from_type_l1_stmt` or `preservation_l1_stmt`
+   statements in `formal/Semantics_L1.v`.** Both are refuted by pinned
+   witnesses and retired to `Prop`; they are not debt. Results that need
+   them take them as explicit hypotheses (as `preservation_l2_via_l1`
+   now does).
    Do not route around the counterexamples with ad-hoc side conditions or
    helper-signature changes. A separately stated sound theorem after an
    owner-approved judgment/step redesign is allowed and expected.
@@ -162,7 +177,7 @@ them if asked; if asked anyway, push back and link this section.
 
 5. **DO NOT patch the legacy `Typing.v` judgment.** It is the
    pre-redesign judgment. `Counterexample.v` depends on its
-   falsity for the regression theorem. Leave it.
+   falsity for `preservation_false`. Leave it.
 
 ### DO
 
@@ -212,8 +227,9 @@ escalate to the owner:
 - region-weakening predicates indexed on syntactic shape,
 - admit-shuffling between `Semantics.v` and a new lemma,
 - "the previous-PR-line-of-attack just needs one more lemma,"
-- proposing to close `Theorem preservation` in `Semantics.v` to
-  `Qed.` by any chain of reasoning,
+- proposing to prove `preservation_stmt` (or turn it back into a
+  `Theorem`) by any chain of reasoning,
+- re-adding any `Admitted.` to `formal/` (the no-False gate will fail),
 - adding new `Axiom` declarations to discharge L1/L2 gaps.
 
 ### If you're unsure

@@ -224,10 +224,14 @@ the exact preservation boundary is recorded below.
 .Post-counterexample 2026-05-26 — read this before any older proof claim
 ====
 The legacy preservation theorem in `formal/Semantics.v` is **provably
-false**. `formal/Counterexample.v` (5 Qed lemmas) demonstrates a
+false**. `formal/Counterexample.v` (6 Qed lemmas) demonstrates a
 configuration that types under the legacy judgment, steps via the
-operational semantics, and lands at an untypable post-state. The
-`Admitted.` on `Theorem preservation` is correct — no proof closes it.
+operational semantics, and lands at an untypable post-state, and
+`preservation_false` refutes the statement outright. No proof closes it:
+since the owner-ratified D0b (2026-11-05) it is retired to
+`preservation_stmt : Prop` rather than kept `Admitted`, because an
+`Admitted` false statement let the build derive `False`. `formal/` now has
+0 `Admitted` and 0 `Axiom`.
 
 The post-discovery architecture is a design program, not yet a sound
 replacement. The unrestricted L1 preservation statement is refuted by
@@ -257,7 +261,7 @@ Qed results are scoped to matching echo rule pairs.
 
 | L1 semantics
 | 🛑 Current unrestricted preservation statements refuted
-| `formal/Semantics_L1.v` has two outer `Admitted.` markers: `step_pop_disjoint_from_type_l1` and `preservation_l1`. Both unrestricted statements have pinned Coq counterexamples; they are not routine open proof debt. See `PROOF-NEEDS.adoc`.
+| `formal/Semantics_L1.v` retires `step_pop_disjoint_from_type_l1` and `preservation_l1` to `Prop` statements (`…_stmt`, D0, 2026-11-05); it has no `Admitted`. Both unrestricted statements have pinned Coq counterexamples; they are not open proof debt. See `PROOF-NEEDS.adoc`.
 
 | L2 modality (`Modality.v`)
 | ✅ Core landed (1 Qed, 0 axioms)
@@ -272,8 +276,8 @@ Qed results are scoped to matching echo rule pairs.
 | `PModeLinear` / `PModeAffine` / `PModeBoundaryMix` enum + `program_mode_to_modality` round-trip. No theorems by design. Design in `formal/PRESERVATION-DESIGN.adoc §7`.
 
 | Legacy `Theorem preservation` (`formal/Semantics.v`)
-| 🛑 Provably false (Admitted)
-| Pinned by `Counterexample.v`. **Do not attempt closure.** Archaeology.
+| 🛑 Provably false (retired to `preservation_stmt : Prop`, D0b 2026-11-05)
+| Refuted by `Counterexample.preservation_false`. **Do not attempt closure.** Archaeology.
 |===
 
 What's done = `Modality.linear_to_affine` (Linear ⇒ Affine weakening,
@@ -310,8 +314,8 @@ documentation comments were clarified.
 |Coq 8.18.0; project build recipe above
 |`+formal/Counterexample.v+`: `+bad_typable+`, `+bad_step+`, `+bad_post_untypable+`
 |Concrete witness refutes the legacy universal statement only. It proves
-no redesign or implementation refinement; retain the separate legacy
-`+Admitted.+` unchanged.
+no redesign or implementation refinement. The legacy statement is
+retired to `+preservation_stmt+` and refuted by `+preservation_false+`.
 
 |`+step_pop_disjoint_from_type_l1+` is false as stated |proven
 |Coq 8.18.0; project build recipe above

@@ -33,9 +33,24 @@ This file is the proof-status audit for Ephapax. It supersedes earlier
 versions that treated the legacy preservation closure plan as viable.
 Keep these categories distinct:
 
-* *Legacy archaeology*: the original `+preservation+` statement is false;
-  its durable `+Admitted.+` and pinned five-`+Qed+` regression in
-  `+formal/Counterexample.v+` are intentional and must remain together.
+* *Legacy archaeology*: the original `+preservation+` statement is false.
+  Since the owner-ratified D0b (2026-11-05) it is retired to
+  `+preservation_stmt : Prop+` (not closed) and refuted outright by
+  `+preservation_false+` in `+formal/Counterexample.v+` (6 `+Qed+`).
+
+[IMPORTANT]
+====
+*D0/D0b retirement (owner-ratified 2026-11-05).* `+formal/+` now has
+*0* `+Admitted.+` and *0* `+Axiom+`. The three refuted statements
+(`+Semantics.preservation+`, `+step_pop_disjoint_from_type_l1+`,
+`+preservation_l1+`) are `+Prop+` definitions, each refuted by a `+Qed+`
+counterexample. While they were `+Admitted+`, the build could derive
+`+False+`; CI's no-False gate (`+coq-build.yml+`) now blocks any new
+`+Admitted+`/`+Axiom+`/`+Parameter+`. The L2 corollaries
+`+preservation_l2_via_l1+` and `+preservation_l2_lift_case+` take
+`+preservation_l1_stmt+` as an explicit hypothesis. Dated sections below
+that count outer `+Admitted.+` markers are historical.
+====
 * *Redesigned judgments*: L1/L2 change typing interfaces; conceptual
   vocabulary or results from another repo do not discharge Ephapax's
   language-soundness obligations.
@@ -51,13 +66,12 @@ The current preservation boundary is:
 [cols="18%,26%,56%",options="header"]
 |===
 |Layer |Status |Evidence / boundary
-|Legacy |*False as stated; pinned archaeology* |`+Counterexample.v+` has
-5 `+Qed+` lemmas. Keep the one durable `+Admitted.+` in
-`+Semantics.v+`; do not relabel it ordinary debt or replace it with a fake
-proof.
-|L1 |*Current universal statement false as stated* |`+Counterexample_StepPop.v+`
-refutes `+step_pop_disjoint_from_type_l1+`; `+Counterexample_PreservationL1.v+`
-refutes the modality-polymorphic `+preservation_l1+` via its Linear
+|Legacy |*False as stated; retired, refuted* |`+Counterexample.v+` has
+6 `+Qed+` lemmas, including `+preservation_false : ~ preservation_stmt+`.
+The statement is a `+Prop+`, not a theorem; never state it as proved.
+|L1 |*Current universal statement false as stated; retired* |`+Counterexample_StepPop.v+`
+refutes `+step_pop_disjoint_from_type_l1_stmt+`; `+Counterexample_PreservationL1.v+`
+refutes the modality-polymorphic `+preservation_l1_stmt+` via its Linear
 instance (the pre-state witness types in both modes). It does not by itself
 refute a separate Affine-only theorem. The existing
 `+bad_input_untypable_l1+` only rejects the original legacy witness; it does
@@ -136,8 +150,8 @@ link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`].
 |`+formal/Echo.v+` |12 Qed, 0 admits
 
 |Linear-mode forward progress lemmas |`+formal/Semantics_L1.v+` |37 Qed;
-*2* outer `+Admitted.+` markers (`+step_pop_disjoint_from_type_l1+` /
-`+preservation_l1+`) cover *2* internal `+admit.+` cases at current
+0 `+Admitted.+` since D0 (2026-11-05). Historical note: *2* outer `+Admitted.+` markers (`+step_pop_disjoint_from_type_l1+` /
+`+preservation_l1+`) covered *2* internal `+admit.+` cases at then-current
 lines 3315/3336 (rebuilt `+coqc 8.18.0+` ground truth 2026-06-27; the
 earlier 5-internal / lines-576/646/1994/2014/3132 figure is
 pre-dissolution, superseded by the §4 marker = 3 total). Phase 3b Stage
@@ -201,9 +215,9 @@ graceful abandonment
 |Stage 3b and β-case helpers landed with explicit premises; they are not
 unconditional preservation theorems. The unrestricted region-shrink helper
 and former region-liveness lemma were refuted and removed; the restricted
-`+region_shrink_msperm+`/value/neutral results are Qed. Two outer L1
-`+Admitted+` markers remain, and both unrestricted statements are now
-refuted by pinned counterexamples (see §1 boundary and §4 seam audit).
+`+region_shrink_msperm+`/value/neutral results are Qed. The two former
+outer L1 `+Admitted+` markers are retired to `+Prop+` statements (D0,
+2026-11-05); both are refuted by pinned counterexamples.
 |===
 
 ==== Counterexample regression
@@ -429,8 +443,10 @@ These are not preferences. They are explicit, durable, owner-issued
 
 ==== A. Do not close the legacy preservation theorem
 
-* ❌ `+Theorem preservation+` in `+formal/Semantics.v+` is *provably
-false*. No proof closes it. The `+Admitted.+` is correct. Leave it.
+* ❌ The legacy preservation statement in `+formal/Semantics.v+` is *provably
+false*. No proof closes it. Since D0b (2026-11-05) it is
+`+preservation_stmt : Prop+`, refuted by `+Counterexample.preservation_false+`;
+do not restate it as a `+Theorem+` or `+Lemma+`.
 * ❌ Do not add lemmas to `+formal/Semantics.v+` aimed at that closure.
 Examples that have wasted real session time:
 ** Lemma B variants (`+step_preserves_type+`,
@@ -511,20 +527,19 @@ the owner*:
 
 === §4. Counts + file-by-file map
 
-Coq `+Admitted.+` marker count: *3* (current source inventory): one
-legacy marker plus two in `+Semantics_L1.v+`. This is a marker count, not
-a count of sound obligations still awaiting routine proof.
+Coq `+Admitted.+` marker count: *0* (D0/D0b retirement, 2026-11-05).
+The build is axiom-free; CI's no-False gate enforces it.
 
 CI count marker only (source markers, not routine proof debt):
-Coq admitted proofs remaining: 3
+Coq admitted proofs remaining: 0
 
 
-* `+formal/Semantics.v+` `+preservation+`: false as stated; durable
-  legacy archaeology, pinned by `+Counterexample.v+`.
-* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1+` and
-  `+preservation_l1+`: both unrestricted statements are refuted by
-  `+Counterexample_StepPop.v+` and
-  `+Counterexample_PreservationL1.v+`; neither is ordinary proof debt.
+* `+formal/Semantics.v+` `+preservation_stmt+`: false as stated; retired
+  to a `+Prop+` and refuted by `+Counterexample.preservation_false+`.
+* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1_stmt+` and
+  `+preservation_l1_stmt+`: both unrestricted statements are retired to
+  `+Prop+` and refuted by `+Counterexample_StepPop.v+` and
+  `+Counterexample_PreservationL1.v+`; neither is proof debt.
 * The false unrestricted region-shrink helper was replaced by
   `+region_shrink_msperm+` and proved value/neutral corollaries. The
   false unconditional region-liveness helper was removed and replaced at

@@ -21,9 +21,9 @@ compliance, 16 tests)
 performance, correctness, 13 tests)
 * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`,
 `+src/ephapax-vram-cache/benches/cache_bench.rs+`
-* Total: *488 tests* (`+cargo test --workspace --all-targets+`);
+* Total: *504 tests* (`+cargo test --workspace --all-targets+`);
 pass/fail enforced by `+rust-ci.yml+`
-* Documented all-target tests: 488
+* Documented all-target tests: 504
 
 === CRG Testing Taxonomy — Status