docs(EXPLAINME): add L1/L3/L4 claim sections per PRESERVATION-DESIGN §12.3#257
Merged
Conversation
…N §12.2 + L4 truth fix Executes `formal/PRESERVATION-DESIGN.md` §12.2 steps 1-4 verbatim: 1. Add a new `== The four layers` section between `== What this is` and `== Three superpowers`, listing L1-L4 in a `[cols="1,3"]` table. 2. Update the "Dyadic discipline" row to label `(L2)` and cross-reference the new section. 3. Replace the "Region-based memory" row with the L1 framing (capability threading + sibling region-exit invariant). 4. Add the "Soundness story" footnote block linking the four-layer separation to the verified counterexample. Also fixes a stale truth claim on line 66: "`L4` (dyadic mode) not started" → scaffold has landed (`formal/L4.v` carries `ProgramMode` + `program_mode_to_modality`). Source authority: `formal/PRESERVATION-DESIGN.md §12.2` (the rollout spec) + `formal/L4-DYADIC.md` (which prescribes L4 as definitions-only by design, hence no proof obligations claim in the README table). No proof, code, or workflow changes. Pure documentation rollout. Closes the README half of `PRESERVATION-DESIGN.md §12.2`; companion edits to EXPLAINME.adoc / ROADMAP.adoc / SPEC.md are §12.3-12.7 and not in scope of this PR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…§12.3 Executes `formal/PRESERVATION-DESIGN.md` §12.3 (EXPLAINME rollout): 1. **Weaken the "Dyadic Type System" claim** by labelling it `(L2)` and adding a cross-reference to the README four-layers section and `EPHAPAX-VISION.adoc`. Also adds the Coq-side L2 evidence pointer (`linear_to_affine` Qed in `formal/Modality.v`). 2. **New claim block: "Sibling-safe region capabilities (L1)"** inserted after "Region-Based Memory". Cites the `Counterexample.v` `Qed` lemmas, the `has_type_l1` judgment in `formal/TypingL1.v`, and the §3-§4 design rationale. Honestly marks the 9 residual L1 admits as L2-integration debt. 3. **New claim block: "Irreversibility residue is first-class (L3, planned)"** with both upstream (`echo-types`) and local (`formal/Echo.v`) evidence pointers. Honestly labels integration as planned — `Echo.v` is mechanised, but no ephapax typing rule yet introduces `TEcho`. 4. **New claim block: "Dyadic mode is project-level only (L4)"** citing `formal/L4.v` definitions + `formal/L4-DYADIC.md` design note. Explicitly says no theorems by design, surface syntax not yet wired. The honesty constraint from §12.3 is preserved throughout: where evidence is a design doc or planned, it is labelled as such — not presented as a passing proof. No proof, code, workflow, or schema changes. Pure documentation rollout. Companion to README #256 (the §12.2 half). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
3 tasks
This was referenced May 30, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Executes
formal/PRESERVATION-DESIGN.md§12.3 — the EXPLAINME rollout.What changed
EPHAPAX-VISION.adoc. Adds the Coq-side L2 evidence pointer (linear_to_affineQed informal/Modality.v).Counterexample.v+has_type_l1judgment + §3-§4 design rationale. Honestly labels 9 residual L1 admits as L2-integration debt.formal/L4.vdefinitions +L4-DYADIC.mddesign note; explicit "no theorems by design" claim.Honesty constraint preserved
§12.3 explicitly says: "the evidence is the design doc + counterexample, not a passing proof — say so honestly". The new sections follow that — where evidence is a design doc or planned, it is labelled as such.
Scope
Pure documentation. Companion to README #256 (§12.2 half).
Test plan
🤖 Generated with Claude Code