Main §1.5: foundational equivalence S ⟺ D and the S_imp_D statement by amaybaum · Pull Request #922 · amaybaum/incompleteness

amaybaum · 2026-10-25T14:40:51Z

Objective

This PR corrects Main §1.5's foundational equivalence display, the statement and comment of S_imp_D, and the statements that depend on them directly. Nothing else is in scope. The finding came from the theorem audit carried out under #918.

Merge: not authorized. This is a draft. Merging needs the owner's separate approval at an exact SHA.

Base: main at c91bf5dd84b6415e1c59820ae0333f3b062d10b6
Head: e470204c39d843e8935ba3c5ea242702c7fe6f5b
Tree: d07acd1ebedb5f93d9d5d486594fbaeb8508e943

What changes

Main:98–99.
- The Layer-1 display now states S ⟺ D. The earlier display equated non-Markovianity with a finite-horizon condition, and Main:597 refutes that form.
- The class sentence says what "faithful realization" ranges over: a system as in class (D), meaning a bijection of C_V × C_H with an initial law that may correlate the hidden and visible coordinates, under which the visible trajectory (x₀,…,x_K) has the given law.
- Witnesses for each direction:
  - ⊆ is pushforward_identity / distinguishability_floor;
  - ⊇ is S_imp_D.
- Reading a realization's time-t law as that joint law is a step the kernel does not formalize, and the sentence labels it as such for both directions (§A.34).
Main:500. The process-dilation pointer is scoped to S_imp_D.
Main:532. The S⇒D carrier pointer now says the initial law "may correlate" the coordinates.
verification/lean-manuscript-census.json. Only the note of the family "equivalence chain and memory" changes. Anchors, status and supersessions are unchanged (§A.35).
OIBridge/Equivalence.lean and OIBridge/EquivalenceChain.lean. Comment-only edits: the section comment above S_imp_D, and the header on the stochastic-inverse lemma's role. With comments stripped, the code tokens are identical to c91bf5dd.
papers/Main.tex is regenerated with the build.sh recipe.
papers/Main.pdf is rebuilt from 1614aa58 with sh ./build.sh Main (XeTeX, TeX Live 2023):
- 90 pages, 0 missing glyphs, sha256 4f7c6251e7ad634f43a7ac69ddbc1efda0833ecd382ea1e9b8e1a491e811ec97;
- the display sets within the margins on page 11;
- the build leaves Main.tex byte-identical.

In total, 6 files change. LEDGER.json is unchanged, and no fingerprinted statement line is touched.

Commits

#	Commit	Content
1	`0c0f6111`	The display and its memory sentence, the Main:500 and :532 pointers, and the census note
2	`aae3c2cc`	Class (D) named; "may correlate" at Main:532
3	`5e3b9ac1`	Lean comment-only corrections
4	`2367afa4`	"May correlate" in the Lean comment
5	`b4c3a083`	Review nits N1–N4 and N6: the class sentence, the formalization label on both directions, a two-line display, the census note wording
6	`1614aa58`	N7: faithfulness stated as the law of the whole visible trajectory
7	`e470204c`	The Main PDF rebuilt from `1614aa58` (PDF only)

Commits 1–4 were cherry-picked, with the original messages kept, from a combined local draft that was never pushed. Their messages cite that draft's SHAs. The mapping (review nit N5) is:

Combined draft	This branch
`28efb93e` (A)	`0c0f6111`
`732b81d9` (A-fix)	`aae3c2cc`
`b6c6fefd` (K)	`5e3b9ac1`
`af30e58f` (K-fix)	`2367afa4`

A git merge-tree of this branch with the follow-ups branch reproduces every source blob of af30e58f. Splitting the work therefore loses nothing.

Review

An independent review accepts the branch at 1614aa58. Its verdicts for each commit:

Commit	Verdict
`0c0f6111`	ACCEPT WITH NITS, superseded within the branch
`aae3c2cc`	ACCEPT
`5e3b9ac1`	ACCEPT WITH NITS, superseded within the branch
`2367afa4`	ACCEPT
`b4c3a083`	ACCEPT WITH NITS (N7, fixed by `1614aa58`)
`1614aa58`	ACCEPT

N1–N4, N6 and N7 are resolved, and N5 is the mapping above. Its observations O1–O4 are for follow-ups only.

Checks at `1614aa58`

All of the following exit 0:

toolchain, staleness, voice, voice-scope, ci-gate-presence, artifact-placement, manifest-drift;
claims, duplicate, mirror, citation, architecture, dependency-label --strict;
coverage, lean-manuscript census, baseline-label;
legacy_records_check.py at HEAD;
v3_verifier.py --self-test and --corpus;
edge_rigidity_probe.py, with R7-PTR, R7-RCH and R7-RCL all passing;
finite_horizon_equivalence_probe.py, equivalence_chain_probe.py, bohr_frequency_probe.py;
process_dilation_probes.py, memory_probes.py, c4_backflow_probes.py, review4_probes.py.

The scan of added lines (§A.32/§A.33 and secrets) has no hits.

Re-grep for the false display: "finite-horizon non-Markovianity" no longer occurs anywhere under papers/ or book/, in either README, or in any verification/*.json. The bare form remains only at Main:597, where Main refutes it.

Not run locally: lake build, lean-axioms and v3-receipts. This PR's CI covers them.

Out of scope (separate decisions)

The Part B precision edits on the follow-ups branch (22625cd2): F3, F4, F5, F6, F10, F12. These land after this PR.
The ≤ n³ bound (F13), which waits on the full-text literature check.
The F11 kernel citation.
Main:594, 598 and 604; Substratum:126.
The capacity assumption-watch item.

Generated by Claude Code

… to S_imp_D Part A of the Main mathematical-fidelity correction (local draft, not pushed). - Main 1.5: the display "finite-horizon non-Markovianity <=> exists finite reversible hidden-state realization" contradicted Main 3.4 (Remark, the conditions are diagnostics), which shows the bare form false because the process-dilation construction realizes Markov laws. The display now states the class equality S <=> D with its kernel witnesses per direction (S_imp_D for one inclusion, D_imp_Qfb with Qfb_imp_S for the other, in finite_horizon_equivalence), and the sentence states the universal hidden-memory statement direction by direction (pushforward_identity, distinguishability_floor; existence of a faithful realization from S_imp_D; the conditional-mutual-information vanishing criterion named as standard and not formalized). - Main 3.4, process dilation: the kernel pointer to S_imp_D is scoped. Its class (D) admits an initial law correlating hidden and visible coordinates (RevReal docstring); the hidden prior independent of the visible initial state rests on the prose construction and the cited probes and is not formalized. No kernel identifier proves that form (RootedClassification's common-prior realization covers rooted one-time families, not multi-time joint laws). - Main 3.4, S => D proof: the pointer records that S_imp_D uses a different carrier (clock and complete trajectory record) from the response-table construction the prose proof uses. - Registry note of "equivalence chain and memory" updated to match (A.35 same-commit rule); anchors unchanged. Main.tex regenerated with pandoc 3.1.3 (build.sh recipe; reproduces the checked-in Main.tex byte for byte from the unmodified source). STALE: papers/Main.pdf not rebuilt -- xelatex unavailable in this environment; rebuild with sh ./build.sh Main on the canonical toolchain before release. Corpus scan (A.25): no book chapter, FULL.md, companion paper or README carries the false display; all other "non-Markovianity <=>" sites carry C1/C3/C4 (the characterization theorem) and are unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

Fix commit for Part A (28efb93e), from the independent fidelity review (local draft, not pushed). - N1, Main 1.5: the converse's existence witness is named as a realization of class (D) (S_imp_D yields a RevReal); reading its time-t law as the joint law of HiddenMemory.Realization is stated as a step not formalized. - N2, Main 3.4 S => D proof pointer: 'correlates' -> 'may correlate' (a degenerate X_0 gives a product initial law), matching Main 3.4's process-dilation pointer and the census note. Main.tex regenerated (pandoc 3.1.3). STALE: papers/Main.pdf not rebuilt -- xelatex unavailable; rebuild with sh ./build.sh Main before release. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

…hastic-inverse lemma's role (K) Kernel-comment part K (local draft, not pushed; comments only, no statement or proof changed; not lake-built here -- lake is unavailable locally, the edits are inside existing /-! -/ and /- -/ blocks). - Equivalence.lean, section comment above S_imp_D (F2b): it called the carrier "the manuscript's multi-time response-table carrier". The body (Hid := Fin (K+1) x Traj V K; init pushed along tau -> (tau 0, (0, tau))) and the RevReal docstring say it is a clock-and-record carrier with a correlated initial law, not the independent-prior response-table form. The comment now says so. - EquivalenceChain.lean header (F11): "the whole indivisibility argument rests on" the stochastic-inverse lemma; RecurrenceHorizon.lean reaches the matrix-level no-go by total-variation contraction without it. The header now confines the dependence to the manuscript's argument. Probes that read these sources pass locally: equivalence_chain_probe.py, finite_horizon_equivalence_probe.py, edge_rigidity_probe.py (all guards). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

Fix commit for Part K (b6c6fefd), from the independent fidelity review, N2 (local draft, not pushed). The section comment above S_imp_D said the carrier's initial law 'correlates' the hidden and visible coordinates; a degenerate X_0 gives a product law, so it now says 'may correlate', matching Main 3.4 and the census note. Comment-only: after stripping nested /- -/ blocks and -- line comments, the code tokens of Equivalence.lean and EquivalenceChain.lean are identical to the base c91bf5d. Not lake-built locally (no toolchain); CI's bridge build is the check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

…ions, display fits the measure Review nits on the foundational correction. - N1, Main 1.5: the sentence states the class that "every faithful realization" ranges over -- class (D), a bijection with an initial law on C_V x C_H that may correlate the hidden and visible coordinates. The forward direction holds for every member (pushforward_identity holds for any joint law); the converse's witness is S_imp_D, a member of the class. - N2, Main 1.5: the not-formalized step (reading a realization's time-t law as the joint law of HiddenMemory) is attached to the pushforward_identity and distinguishability_floor pointer, so it covers both directions; the converse's pointer is S_imp_D alone. - N3, Main 1.5: the display is set as a two-line gathered block and the S <=> D tag moved into the prose. In a scratch xelatex build the display's Overfull \hbox (125.72pt; 3.69pt at base) is gone. The remaining seven overfull boxes are pre-existing and unchanged. 90 pages, 0 missing glyphs. - N6, Main 1.5: "The realization theorem" -> "The equivalence S <=> D". - N4, census registry note: the 1.5 pointers are described as inline in the summary paragraph, separately from the 3.4 proof-paragraph pointers. Main.tex regenerated (pandoc 3.1.3). Main.pdf not in this commit; rebuild it in a separate step with sh ./build.sh Main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

Review nit N7 on the foundational correction. In the class sentence, "whose visible marginal is the given law" could attach to the initial law, so that faithfulness would require only the law of x_0 to match, and the forward direction would then fail. It now reads "under which the visible trajectory (x_0, ..., x_K) has the given law". "a member of class (D)" becomes "a system as in class (D)", since Main 3.4 defines (D) as a class of laws (the visible marginals of finite reversible deterministic systems). Main.tex regenerated (pandoc 3.1.3). Scratch xelatex build: no overfull box from the Layer-1 display; the seven pre-existing overfull boxes are unchanged; 90 pages, 0 missing glyphs. Main.pdf is not in this commit. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

papers/Main.pdf is rebuilt with `sh ./build.sh Main` from the source at 1614aa5 (XeTeX, TeX Live 2023; pandoc 3.1.3). The build reports no missing glyphs and leaves the committed Main.tex byte-identical; the corrected Layer-1 display sets within the margins on page 11. 90 pages, sha256 4f7c6251e7ad634f43a7ac69ddbc1efda0833ecd382ea1e9b8e1a491e811ec97. No source, .tex or other file changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

claude added 7 commits October 25, 2026 12:37

amaybaum marked this pull request as ready for review October 25, 2026 17:45

amaybaum merged commit 8dc36d5 into main Oct 25, 2026
26 checks passed

amaybaum deleted the draft/main-foundational-correction branch October 25, 2026 17:45

This was referenced Oct 25, 2026

F13: the imported ≤ n³ dilation bound — hypotheses, attribution and manuscript scope #924

Open

Main: precision follow-ups to the foundational correction (status, scope, pointers) #925

Merged

Navigation Menu

Repository navigation

Main §1.5: foundational equivalence S ⟺ D and the S_imp_D statement - #922

Main §1.5: foundational equivalence S ⟺ D and the S_imp_D statement#922
amaybaum merged 7 commits into
mainfrom
draft/main-foundational-correction

amaybaum commented Oct 25, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

amaybaum commented Oct 25, 2026

Objective

What changes

Commits

Review

Checks at 1614aa58

Out of scope (separate decisions)

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Checks at `1614aa58`