feat(coq): prove the reversibility↔CNO bridge MAA cites (A2, zero axioms)#109
Merged
Merged
Conversation
…xioms) The theorem hyperpolymath/maa-framework (aletheia) cites — the general reversibility<->CNO characterisation — did not exist at the general level. Add it to proofs/coq/common/CNO.v, machine-checked under coqc 8.18.0 with every new result `Closed under the global context` (zero project axioms): - reverses / reversible_iff_exists_reverses: the repo's one-sided `reversible` is exactly "exists a left inverse". - reverses_seq_computes_identity: core lemma — a left inverse sequenced after p computes the state-identity on every composite transition (via eval_app + the existing eval_deterministic). - cno_equiv_seq_empty_of_reverses: repackaged as cno_equiv (p;;p_inv) [] (CNO-equivalence to the canonical no-op). - reversible_bridge_forward: the faithful FORWARD direction of the aletheia contract — a two-sided inverse makes BOTH composites cno_equiv _ []. - reversible_bridge_backward_upto: the BACKWARD direction, necessarily up to =st=, with an explicit p_inv-termination hypothesis. - eval_nil_eq: small helper (eval [] s s' -> s' = s). Honesty finding (documented in-file and in PROOF-STATUS.adoc): the literal `reversible p <-> exists p_inv, is_CNO(p;;p_inv) /\ is_CNO(p_inv;;p)` is NOT provable here and is deliberately not asserted — is_CNO over-demands purity/totality (so "=== CNO" is rendered by cno_equiv _ []); state_eq excludes the program counter while eval propagates it (the unsound eval_respects_state_eq_* axioms were removed 2026-05-20), forcing the backward direction up to =st=; and reversible is one-sided while the contract is two-sided. The takeaway for aletheia: state the contract two-sided and =st=-relative. Verified: from-scratch `coq_makefile -f _CoqProject && make` builds 14/14 theories with zero errors; `Print Assumptions` on all five new results reports "Closed under the global context". Lean mirror deferred. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz
hyperpolymath
marked this pull request as ready for review
July 17, 2026 04:23
hyperpolymath
added a commit
that referenced
this pull request
Jul 17, 2026
…blocked) (#110) ## What A Lean 4 mirror of the Coq A2 bridge (merged in #109), as `proofs/lean4/CNOBridge.lean` — the five results `reverses`, `reverses_seq_computes_identity`, `cnoEquiv_seq_empty_of_reverses`, `reversible_bridge_forward`, `reversible_bridge_backward`, plus a functional-model biconditional corollary. ##⚠️ Verification status — UNVERIFIED in this environment I could **not** machine-check this file where it was authored: the Lean toolchain and Mathlib cache download from GitHub **release assets**, which this environment's egress policy blocked (HTTP **403** — confirmed on both the `elan` release and the `lean4 v4.16.0` toolchain; these are org-policy denials the proxy README says to report, not retry). So I made it safe and honest rather than pretend: - Registered in `lakefile.lean` as a **non-`@[default_target]`** `lean_lib` — the standard `lake build` (your green proof suite) is **not** affected by it. - Loudly labelled UNVERIFIED in the file header with the exact verify command. - Disclosed in `PROOF-STATUS.adoc`. - **No Coq files touched** — the merged A2 development is unchanged. **To verify (where the toolchain is reachable):** ``` cd proofs/lean4 && lake exe cache get && lake build CNOBridge ``` plus `#print axioms` on each theorem. ## Modelling note (disclosed cross-model difference) Lean's `eval` is a **total function** and `ProgramState.eq` **includes** the PC, whereas Coq's `eval` is a relation and `=st=` **excludes** it. So the mirror states the bridge with **syntactic** state equality — a stronger, cleaner form that needs no determinism lemma (free for a function) and no "up-to-`=st=`" slack on the backward direction. It is the functional-model analogue, not a literal transcription — consistent with the repo's "each prover checks its own formalisation" stance. ## Your call If you'd rather not carry an unverified file in-tree, say so and I'll drop it — or once you confirm it builds on your end, I can flip it to `@[default_target]` and record it as verified in `PROOF-STATUS.adoc`. ## Context Thread 2 of a three-thread follow-up (Lean mirror → estate dashboard checker → januskey Phase B). Draft pending human review. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz --- _Generated by [Claude Code](https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 17, 2026
….a2ml (#111) ## What & why `.claude/CLAUDE.md` listed the machine-readable metadata as `STATE.scm`, `META.scm`, … directly under `.machine_readable/`, and the language table's Guile Scheme row named the same `.scm` files. **None of those `.scm` files exist** — the real metadata lives in `.machine_readable/descriptiles/*.a2ml` (and a2ml is TOML-flavoured, not Guile Scheme). This is the documented CLAUDE.md drift the estate's STATE files flag. ## Change - Point the "Machine-Readable Artefacts" list at `.machine_readable/descriptiles/*.a2ml` (the files that actually exist: `STATE`, `META`, `ECOSYSTEM`, `AGENTIC`, `NEUROSYM`, `PLAYBOOK`). - Fix the Guile Scheme row to stop claiming the state/meta files are `.scm`. Docs/config only; single file. ## Context Loose-end cleanup after the A2 Coq (#109) and Lean-mirror (#110) work. Draft pending review. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz --- _Generated by [Claude Code](https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz)_ Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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.
What & why
The theorem
hyperpolymath/maa-framework(aletheia) cites — the general reversibility↔CNO characterisation — did not exist at the general level (only a filesystem-specific instance). This lands it inproofs/coq/common/CNO.v, machine-checked undercoqc 8.18.0, with every new resultClosed under the global context(zero project axioms).New results (all axiom-free)
reverses/reversible_iff_exists_reverses— the repo's one-sidedreversibleis exactly "∃ a left inverse".reverses_seq_computes_identity— core lemma: a left inverse sequenced afterpcomputes the state-identity on every composite transition (viaeval_app+ the existingeval_deterministic).cno_equiv_seq_empty_of_reverses— repackaged ascno_equiv (p ;; p_inv) [](CNO-equivalence to the canonical no-op).reversible_bridge_forward— the faithful forward direction of the aletheia contract: a two-sided inverse makes both compositescno_equiv _ [].reversible_bridge_backward_upto— the backward direction, necessarily up to=st=, with an explicitp_inv-termination hypothesis.eval_nil_eq— small helper (eval [] s s' → s' = s).Honesty finding (this is the valuable part)
The literal
reversible p ↔ ∃ p_inv, is_CNO (p;;p_inv) ∧ is_CNO (p_inv;;p)is not provable under these definitions and is deliberately not asserted:is_CNOalso demands purity and totality-everywhere — areversibleprogram need not have either — so "≡ CNO" is faithfully rendered bycno_equiv _ [](the identity-on-state component).state_eq(=st=) excludes the program counter whileevalpropagates it (theeval_respects_state_eq_*axioms were removed as unsound on 2026-05-20), forcing the backward direction to be up-to-=st=.reversibleis one-sided; the aletheia contract is two-sided.Takeaway for aletheia: state the contract two-sided and
=st=-relative. Documented in the in-file section header andPROOF-STATUS.adoc.Verification
coq_makefile -f _CoqProject && makebuilds 14/14 theories, zero errors.Print Assumptionson all five new results → "Closed under the global context".Context
Task A2 of the estate assessment — the one still-open Phase A proof item after PR #100 landed OND-1..5 and discharged the filesystem/quantum-existence axioms. Docs updated:
PROOF-STATUS.adoc(new bridge subsection),ROADMAP.adoc(Milestone 1 checkbox). Draft pending human review.🤖 Generated with Claude Code
https://claude.ai/code/session_015qwVESTcbfanY2iJPQNoSz
Generated by Claude Code