[amaybaum]

Draft. Guiding PR for #924 (F13), the imported ≤ n³ dilation bound.

Purpose

This PR carries the correction the owner scoped for #924. It is one guiding draft PR (§A.43), kept separate from the other Main threads. It has two stages:

• First: two low-risk citation and wording fixes, M3 and M4. These are the commits here now.
• Later: M1 and M2. They land together because they are coupled, after review of this stage.

The literature check is the first-hand reading of [11] (arXiv:2309.03085v2) and [12] (arXiv:2302.10778v3 = Philosophy of Physics 3(1):8). That reading was reviewed and accepted.

Scope of this stage

• M3: Main §3.1, scope paragraph. The citation labels were swapped. "Philosophy of Physics 3(1):8, 2025 [11]; proof in [12]" becomes "… 2025 [12]; proof in [11]", which matches the bibliography: [11] is the arXiv theorem paper, whose §5 proves the theorem, and [12] is the published paper. No pinpoints are added: the original sentence had none, and the defect is the swap.
• M4: Explainer §3.1, "The core statement." "Any P-indivisible stochastic process …" limited the class to P-indivisible processes. It now reads "Any process in Barandes' class — a broad one, including Markov chains — …", the class wording of the same section's next paragraph. This agrees with Main §3.1/§3.4 and with [11] §3.3/§4.1.

Each edit changes one sentence. Main.tex/.pdf and Explainer.tex/.pdf were regenerated with sh ./build.sh Main Explainer. Each .tex differs only in the edited sentence and its source-sha256 stamp, and each PDF's extracted text differs only at the edited lines.

Propagation (§A.25). I grepped papers/*.md, book/*.md and book/The-Incompleteness-of-Observation-FULL.md for both defects: every Barandes bibliography entry and its in-text labels, "3(1):8", "proof in [", and every statement of the embedding class. Neither defect recurs anywhere else. The book carries neither.

Not changed in this stage

• M1 (and its LEDGER update). Main's definition of "unitarily evolving QM" (dimension ≤ n³ and a fixed Ĥ), the lemma that realizes its fixed-Ĥ form, and the sites that attribute a ≤ n³ fixed-Ĥ form to the source. M1 moves the statement fingerprints of MAIN:D-unitarily-evolving-qm and MAIN:L-fixed-hat-h-form-realized, so it lands with their verification/coverage/LEDGER.json update.
• M2. Main's "n² at a single step, within the source's ≤ n³ bound" contrast, and the "compressed form" import sites across Main, the Explainer, Methodology, Structure, the book and the FULL mirror. M2 lands together with M1, with the n² form attributed to the literature. It also needs a re-check of architecture_check.py's compressed exemptions.
• Kept separate: Structure:1272's statement of the correspondence (M5), SM's journal reference for arXiv:2302.10778 (M6), and the Explainer's numeric citations "Barandes [10,11]" (:1008) and "Wolpert … [19]" (:619), which point nowhere because the Explainer has no bibliography (in Main, [10] is Milz et al. and Wolpert is [50]). GR:20's "bridge from P-indivisible … processes" was considered and is left for M2.
• Unaffected: Lean modules, the census registry and the verification records.

No LEDGER fingerprint moves in this stage. coverage_check.py passes with LEDGER.json unchanged. Bands unchanged.

Checks (local, at the head of this stage)

• Build. sh ./build.sh Main Explainer: build OK, no dropped glyphs. Main is 99 pages and Explainer is 71, both unchanged. Median characters per page are unchanged (Main 3302, Explainer 2879).
• Release-gate steps run locally, exit 0:
  • toolchain, staleness, baseline-label, voice, voice-scope, ci-gate-presence;
  • artifact-placement, manifest-drift, claims, duplicate, mirror, citation, architecture;
  • dependency-label --strict, coverage, lean-manuscript, v3-self-test.
• Not decidable locally (shallow clone):
  • legacy-records, v3-receipts and citation-roles report UNDECIDABLE undecidable:shallow-repository;
  • v3-corpus's only three mismatches are the s8-landed-* history vectors, for the same reason.
  • These steps need full history and run in CI. No file under verification/ is touched.
• Not run: Lean, lean-axioms and probe suites. Nothing in this stage changes their inputs.
• Independent review: accepted with nits; the reviewer re-ran coverage, architecture, voice, voice-scope, census, citation and staleness checks (all pass) and confirmed the shallow-clone UNDECIDABLE result is identical on unchanged main.

Links

• Issue: F13: the imported ≤ n³ dilation bound — hypotheses, attribution and manuscript scope #924
• Related: Introduction paper: reconcile sources and integrate scoped theorem recoveries #918 (the Bar26 Thm 3.3 attribution for the n² form is coordinated there for M2)

---

Generated by Claude Code

[amaybaum]

Exact-head review: #1026 at 9bf42d591d7b61d59776b32350b71ffda895ae76

Verdict: READY-FOR-OWNER-MERGE-DECISION. This review is read-only. It does not approve a merge. Merging requires the owner's explicit approval of the exact SHA 9bf42d591d7b61d59776b32350b71ffda895ae76.

Head

• The PR head is 9bf42d59… and branch fix/dilation-citation-924-20261101 points to the same commit. This is the expected head, and the branch has not moved since the pre-push review.
• The base is 07d94f2c, and main is still 07d94f2c618c17237bea5b8bbf914417e598940b, so there is no base drift.
• There are two commits, each single-parent and linear: f32d0546 (M3) on 07d94f2c, then 9bf42d59 (M4).

Scope (diff 07d94f2c..9bf42d59, 6 files, +10 −9)

• papers/Main.md: one line changes, :218. "[11]; proof in [12]" becomes "[12]; proof in [11]".
• papers/Explainer.md: one line changes, :282. "Any P-indivisible stochastic process" becomes "Any process in Barandes' class — a broad one, including Markov chains —".
• papers/Main.tex and papers/Explainer.tex change only in the edited sentence and the source-sha256 stamp. Each stamp equals the sha256 of its .md.
• papers/Main.pdf and papers/Explainer.pdf were regenerated. The extracted text has the new wording and not the old. Page counts are unchanged: 99 and 71.
• Nothing else changes. There is no M1 or M2 content: the fixed-Ĥ definition, the n² single-step contrast and the "compressed form" sites are untouched. Nothing under verification/ changes, so LEDGER.json is unchanged.

CI at the exact head (structured results)

There is one workflow run, verify (run 41330970936, event pull_request, attempt 1, conclusion success). It reported 26 check-runs on head_sha 9bf42d59, all completed:

• 25 concluded success. These are Lean kernel check, Mathlib bridge, Numerical probes and its 22 matrix jobs.
• 1 concluded skipped: Numerical probes / A42 exclusion (${{ matrix.part }}), the matrix template entry.
• Mathlib bridge checks out with fetch-depth: 0. Its Release gate step concluded success.
  • That step runs tools/release_gate.py, which exits 0 only if every gate step exits 0.
  • The gate steps include legacy-records, v3-corpus (every vector as expected, including the three s8-landed-* history vectors), v3-receipts and citation-roles.
  • All four were undecidable in the local shallow clone and are decided here on full history.
  • The only skipped step in that job is the KTRANS-SEP-2 negative marker. Skipped is its passing state.
• Numerical probes / core B step SC-42 integration source scope and must-fail controls concluded success.

The run tests the synthetic merge 229c4577 (parents 07d94f2c, 9bf42d59). Its tree fa496c4d is identical to the head's tree, so the result applies to the head's content. This is PR verification only; no V3 round is involved.

Mergeability and other open PRs

• mergeable: true, mergeable_state: clean.
• No other open PR has a .md hunk overlapping Main:218 or Explainer:282, each checked on that PR's own base.
• Expect mechanical conflicts in the generated artifacts: the last-line source-sha256 stamp and the binary PDF. Whichever PR lands second regenerates them.
  • Main.tex and Main.pdf: SC-29: kernel scope — strongly continuous drive, joint-law form of the memory and C3 theorems, ledger levels #961, SC-34: cycle ergodicity on energy shells — map named at every site; false for the exact linear rule, unsupported for the rounded rule #971, SC-41: Pauli-twirl classical-memory decomposition of the uniform-slot card game in Main §4.5 #972, SC-35 (PR-G): kernel-only results into Main, with census anchors #973, SC-40: (C2)/(C3) statements and probe evidence in Main §1.3 #974, SC-38: probe evidence labels and horizon in Main §3.4 #975.
  • Explainer.tex and Explainer.pdf: SC-29: kernel scope — strongly continuous drive, joint-law form of the memory and C3 theorems, ledger levels #961, SC-17 (Explainer): Bell at Main §3.3's scope, the dynamics' form fixed up to one coefficient, chirality without the memory claim #963, SC-34: cycle ergodicity on energy shells — map named at every site; false for the exact linear rule, unsupported for the rounded rule #971, SC-38: probe evidence labels and horizon in Main §3.4 #975.
• Research audit: observer-relative finiteness and finite-carrier proof boundaries #1017 does not touch these files. Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028 and Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 are planning Issues with no PR yet.
• Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028 assigns a later edit to Main:218 (TC D-6) to F13: the imported ≤ n³ dilation bound — hypotheses, attribution and manuscript scope #924. Main:218 is a single-line paragraph, so that edit should be cut on top of this one.

Scientific and editorial check

• M3 is correct. Main's bibliography lists [11] as "The Stochastic-Quantum Theorem" (arXiv:2309.03085) and [12] as "The Stochastic-Quantum Correspondence" (Philosophy of Physics 3(1):8, 2025). The published paper is [12], and [11] contains the proof (its §5). The change is the minimal label swap. No pinpoint is added, because the original had none.
• M4 is correct. The new wording matches the class statement in the same section (Explainer:288, "his class — a broad one, including Markov chains"). It also matches Main §3.1 (iii) and Main §3.4, and [11] §3.3/§4.1.
  • It keeps the finite-configuration restriction and adds no claim.
  • It does not assert a fixed generator; that question is left to M1.
• Register. Both edits change one sentence each. The added text has no self-narration, history voice, caps emphasis or overclaim (§A.32, §A.33).
• Local checks re-run at this head, all exit 0: staleness, voice, coverage (134 statements), mirror, and citation (112 citations, 0 broken). The tree was clean afterwards.

Verdict

READY-FOR-OWNER-MERGE-DECISION. The scope matches the approved stage-1 scope. CI is fully green at the exact head, including the full-history gate steps. The PR is cleanly mergeable on unchanged main, and both edits are accurate against their sources. Merging requires the owner's exact-SHA approval of 9bf42d591d7b61d59776b32350b71ffda895ae76. If the branch or main moves first, this review must be repeated.

---

Generated by Claude Code

[amaybaum]

Merge record (verification). The merge commit is 151626057492bb1e2a74000fb85498f842860260, with parents 07d94f2c (main) and 9bf42d591d7b61d59776b32350b71ffda895ae76 (the owner-approved exact head). The merge tree is identical to the head tree. Push CI on the merge commit, run 41373401328, passed: 25 jobs succeeded and 1 was skipped as expected. Nothing else is open on this PR.

---

Generated by Claude Code