[amaybaum]

#1029 NEW-B — unit 1: evidence metadata and docstrings only

Base: main 01a096a95a02caa1c471d892f34db919593783d9.
Head: 57f43dafa3540d7d32315fea624f664f84fd2777.
Authority: owner direction to prioritize and complete #1029 before returning to #1037; issue #1029 scope decision. Independent paper-only mapping ACCEPT with final check was recorded in #1029 comments 6567726906 / 6567736044. This PR is a new exact-head review gate, not a claim that prior paper review covers these committed bytes.

Exactly three files; no publication source or build

1. verification/lean-mathlib/OIBridge/C3Necessity.lean: fix two docstring-only section pointers from Main §3.3 to §3.4 (O5).
2. verification/lean-manuscript-census.json: record joint-law kernel scope and the independent-review hold on TrajectoryMemory's time-t interpretation (O8). Existing anchors/status/supersessions unchanged.
3. verification/coverage/LEDGER.json: two text-only delta corrections:
   • MAIN:C-per-process-capacity-bound: records the kernel finite-family/joint-law form, unreviewed time-t/supremum bridge, and unformalized accumulated-capacity form.
   • MAIN:T-finite-horizon-process-dilation: records the weaker correlated-initial-law S_imp_D theorem and unformalized independence of μ_H in the paper result.

Guardrails

• Keep both affected LEDGER rows P, with no new Lean checks; no grade rises. Keep the two K3 entries MAIN:T-c3-necessity and MAIN:T-unavoidable-hidden-predictive-memory completely unchanged pending Research backlog: advance downgraded and conditional scientific claims from corpus audit #970 P1/P2.
• No changes to Lean theorem statements, manuscript claims, C1–C4, publication sources, .tex, .pdf, or FULL. JSON was parsed after exact changes; diff inspected against pinned main and restricted to 2+1+2 changed lines in three files.
• No unreviewed time-t promotion, proof claim, rewrite of frozen records, or reclassification of prior evidence.
• Remaining Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 units (orphans 18, 27, 30, 32, 34, 38, 39 and remaining parts of 28) still open. They must be independently scoped/reviewed and publication-built as required; Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 must not be closed on this PR alone.
• Main:218 stays with Correction planning: scientific overclaims and status corrections (from the 2026-11-01 disposition) #1028; Explainer:1019 was corrected by merged Fast-bath correction: suppression not exclusion; C2-slow vs C2-structural; P-divisibility scope (#1028 unit 1) #1035. docs: distinguish bounded observer access from finite total substratum #1036's authorized README change is deferred while Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 occupies the active slot; OI-CARD: finite observational underdetermination, reversible undecidability, and interface-relative gauge — gated research units #1037 U0–U6 and five holds are unchanged.

Review gates

Independently verify this exact head against the recorded source statements and coverage tool; ordinary CI/Lean/registry checks must pass. Draft/unmerged — no merge authorization.

[amaybaum]

Independent exact-head review: READY-WITH-NITS (2026-11-02). Head reviewed: 57f43dafa3540d7d32315fea624f664f84fd2777. Base: main 01a096a9.

Scope. The diff touches 3 files, with 5 lines changed. These are all untouched:

• the two K3 rows MAIN:T-c3-necessity and MAIN:T-unavoidable-hidden-predictive-memory;
• every grade and fingerprint;
• every Lean statement;
• every manuscript file.

Fidelity to the accepted #1029 mapping and review (comments 6567726906 / 6567736044):

• O5 now reads §3.4, which is correct at 01a096a9.
• O8, the census scope note, limits only the time-t form, keeping clause (c) for hidden predictive memory and the joint-law K3 scope.
• :1138 matches the reviewed replacement word for word: I* is a maximum over a finite family of joint-law slices (card_hidden_ge_two_pow_Istar); the supremum over all times is in the unreviewed trajectory_capacity; the accumulated form is not formalized.
• :1159 is accurate. Independent μ_H has no Lean statement, and the weaker correlated-initial-law form is S_imp_D.

Tools at the head (run in a temporary worktree):

• coverage_check exits 0. It reads only checks, never delta, so a P row whose delta names a lemma passes.
• The census tool exits 0.
• No guard pins the edited census note.

CI: 26 check-runs: 25 succeeded and 1 was skipped by its condition. Mergeability: git merge-tree against main is clean, and the merge would be a fast-forward.

Nit (non-blocking, wording already owner-approved). In O8, "…pending independent confirmation…, and is otherwise on paper" binds "otherwise on paper" to the time-t form. A clearer form for a later edit would be: "…interpretation; the remaining time-t content (memory clauses (a) and (b)) is on paper".

The PR stays draft and unmerged; merging needs the owner's exact-SHA approval. #1029 stays open for its remaining units (18, 27, 32, 34, 38, 39 and the rest of 28).

---

Generated by Claude Code

[amaybaum]

Merge record: #1038 (#1029 unit 1)

Merged with a normal merge commit at the owner-approved exact head 57f43dafa3540d7d32315fea624f664f84fd2777, giving main = ce8e1de26e417651549514f450f8b7a7c88cf9b2.

Post-merge checks.

• Parents are 01a096a9 (previous main) and 57f43daf.
• The merge tree is identical to the approved head's tree.
• 3 files changed, with 5 lines added and 5 removed: C3Necessity.lean (2 docstring lines), lean-manuscript-census.json (1 note line) and LEDGER.json (2 delta lines).
• main CI on ce8e1de2 (verify, push event, run 41436712381) is green: 25 jobs passed and 1 was skipped by its condition. The Lean kernel check, Mathlib bridge and every numerical probe shard are included.

Scope. This was an evidence-traceability correction:

• Lean statements, census anchors and supersessions are unchanged.
• LEDGER grades and fingerprints are unchanged.
• No manuscript, .tex, .pdf or FULL file was touched.
• Correctness bands are unchanged.

Deferred. The exact-head review raised one non-blocking nit on the census note (O8). In "…is formalized in an unreviewed Lean module (…), pending …, and is otherwise on paper", the final clause reads as attaching to the time-t form. Suggested wording for a later touch: "…interpretation; the remaining time-t content (memory clauses (a) and (b)) is on paper". It is tracked on #1029 for a later unit.

The five standing holds (#1009, #1023, #1011, #1003, #918) are unchanged.

---

Generated by Claude Code