[amaybaum]

Accepted head: d83f8723ae2e2cc0544b63900f40b2e1d19213dc.

• Independently reviewed: ACCEPT for the full PR at this head. Commit-1 scope and row 6 also have separate ACCEPT verdicts.
• CI at this head: 25 passed, 1 skipped, 0 failed.
• The owner approved a normal merge at this SHA, in chat on 2026-11-04, conditional on completed green CI and an acceptance covering this exact head.

This is a minimal correction for #1013 / #1015. Several sites stated the finiteness of the whole substratum, hidden sector included, as if it were established. Lemma 1 gives the visible sector's finiteness; the hidden sector's finiteness is a posit (Main §1.2 Remark, §4.5; posit A1 in the book).

Base: main at 1609dc44.

Commits and reviewed scope

1. ea7a3c2c, rows 4, 5, 7, 8, 9 and 12:
   • Main Lemma 3 (papers/Main.md:56) now reads: "On each finite cycle of the reversible representative, the invariant probability measure is unique and uniform". Mirrored at book/ch01-observation.md:38 and FULL:382.
   • Main setup (row 5): C_V is finite by Lemma 1; C_H is finite under the total-finiteness posit (§1.2, §4.5).
   • papers/Explainer.md :44, :145 and :169.
   • book/ch03-structural-realism.md:22 and FULL:896: "…structural lemmas and posit A1 of Chapter 2".
2. c0a2e6d1, row 6 at papers/Main.md:224. Reviewed separately.
3. 93963e14, fixes from the first review:
   • "of the selected reversible model" becomes "of the reversible representative" at Main:56, ch01:38 and FULL:382.
   • The coverage ledger entry MAIN:L-3 now lists "finiteness of S (total-finiteness posit, §1.2 Remark, §4.5)" among its assumptions, matching the Lean witness's [Fintype S].
4. e5b70938, row 6 narrowed: "every result in §2–§3 other than the infinite-region completion (§3.2, §3.4), which is assembled from finite-region stages, runs on finite configuration spaces: Lemma 1 for the visible sector, with the total-finiteness posit (§1.2 Remark, §4.5) where a result also needs the hidden sector finite."
5. d83f8723, regenerated audit JSON:
   • verification/audits/manuscript/bell-operational-reconciliation-20261029/sc42-integration-result.json gains two "chapter line mirrored in FULL" records, for ch01 Lemma 3 and ch03. Both are ok.
   • The normal and optimized outputs agree, and the controls file is unchanged.
   • This file is not a frozen record, and earlier chapter-editing PRs regenerated it the same way.

Bookkeeping files changed:

• Coverage ledger (verification/coverage/LEDGER.json): fingerprints re-affirmed for EXPLAINER:L-1 and MAIN:L-3, plus the MAIN:L-3 assumption above. tools/coverage_check.py passes.
• Generated artifacts: Main, Explainer and the book were rebuilt with build.sh at every commit that changed their sources. No glyphs were dropped, page counts are unchanged (100, 71 and 560), and tools/staleness_check.py passes.

Not in this PR

• Seven sites and their mirrors, now owned by SUBSTATE-1: minimal manuscript scope and finite-S dependency audit #1015 (owner decision, recorded on SUBSTATE-1: minimal manuscript scope and finite-S dependency audit #1015):
  • Main:46 with ch01:28 / FULL:372;
  • Main:718 with GR:589;
  • GR:142;
  • Explainer:1005;
  • ch05:23 / FULL:1350.
    Drafting and review are authorized; merging needs separate approval.
• A separate scientific item: Main:720 and Main:722.
• Listed but not edited:
  • the posit-as-fact sites ch18:290, Explainer:679, appendix-c:114, glossary:11, ch09:36 and appendix-a:48;
  • ch01:41 / FULL:385 ("On a finite set, injectivity implies surjectivity"), which the reviewer flagged as SUBSTATE-1: minimal manuscript scope and finite-S dependency audit #1015's priority;
  • the older "orbit" wording at Explainer:56, Explainer:115, ch01:85, FULL:429 and Main:62;
  • the Lean docstrings in CanonicalMeasure.lean that still quote the old Lemma 3 wording.

🤖 Generated with Claude Code

https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

[amaybaum]

Merge record. Normal merge f2feecc19adda4d5508662ba413175b16137a711 of the approved head d83f8723.

• Approval: the owner's exact-SHA approval, in chat on 2026-11-04. It was conditional on completed green CI and an acceptance covering the exact head; both held.
• Parents: main b2e053f3, the Research (WIP): SUBSTATE-1 finite-boundary / infinite-hidden countercontrols #1016 merge, whose main CI is green with 25 passed and 1 skipped; and d83f8723.
• Tree: 6a88338a is identical to a clean merge of those two parents. It changes the same 13 files, with the same line counts, as the PR diff from 1609dc44.
• Main CI on the merge is running and will be recorded here.

---

Generated by Claude Code

[amaybaum]

Main CI on merge f2feecc1: green. All 26 check runs completed with no failures (25 passed, 1 skipped).

---

Generated by Claude Code