Skip to content

SC-35 (PR-G): kernel-only results into Main, with census anchors - #973

Closed
amaybaum wants to merge 2 commits into
mainfrom
corpus/sc35-kernel-anchors
Closed

SC-35 (PR-G): kernel-only results into Main, with census anchors#973
amaybaum wants to merge 2 commits into
mainfrom
corpus/sc35-kernel-anchors

Conversation

@amaybaum

@amaybaum amaybaum commented Oct 28, 2026

Copy link
Copy Markdown
Owner

This is a source-correction unit for #946 (gate) and #918 (Introduction). Its finding comes from the full-corpus audit of #918 at 60c976fe, unit PR-G.

Base: main at 0d917665. Head: 07af6cf3. The independent review returned ACCEPT on this exact head after one fix round (F1–F5).

Finding

Three kernel results that the Introduction states or will state were carried by no manuscript. Their census families were kernel-only, so the census checked none of them.

  • Main §2.3 understated the kernel. It named only the stochastic-inverse lemma as kernel-checked. The composition with P-divisibility is kernel-proved by pIndivisible_of_rooted_identity_return_of_overlap.
  • Routed readback, in both of its formalized readings, was stated nowhere. The two readings are incomparable, and OD-5 makes the storage-time reading primary.
  • Main omitted the all-time classification of rooted realizability (finiteRootedRealizable_iff_pper), and its open item still listed that case as open.

Changes

  • papers/Main.md §2.3:

    • A new Theorem (overlap and return) states every hypothesis of the kernel theorem: finite sets, a bijection, one shared hidden prior with no support condition, Γ_n = I, and an overlap at some s < n. Its conclusion is the kernel's.
    • The history-readback parenthetical now separates what the kernel proves from what is proved on paper.

  • Routed readback: stated in both readings. The text names what is not established and what is not an accessible window.

  • Rooted classification: stated with separate §A.34 witnesses for each direction:

    • forward: pper_of_finiteRootedRealizable;
    • converse: pper_has_responseRealization;
    • assembled: finiteRootedRealizable_iff_pper.

    Main:640 and :733 and verification/ROADMAP.md are aligned with it.

  • Census: the four families move from kernel-only to current, with anchors (§A.35).

  • Coverage:

    • A new entry MAIN:T-overlap-return at K3.
    • MAIN:T-history-readback-finite-recurrence-implies stays at P, its base grade. Its note records that the final clause is kernel-proved through MAIN:T-overlap-return, and that three steps remain on paper.

  • Guards: in edge_rigidity_probe.py, R7-RCH and R7-RCL ban these modules outside Main and pin the scope phrases. A mutation script fails all six mutations, one at a time, and restores the files byte for byte.

  • Regenerated: Main.tex and Main.pdf, 98 pages.

  • Lean: no Lean file changed.

Checks at 07af6cf3

The reviewer re-ran each of these independently:

  • tools/coverage_check.py: OK, 129 canonical statements.
  • tools/lean_manuscript_census.py: OK.
  • verification/lean/edge_rigidity_probe.py: all checks pass.
  • sc35_check.py: OK, 90 checks.
  • sc35_guard_mutations.py: 6 of 6 mutations fail their named guard.
  • tools/release_gate.py: every step passes except lean-axioms, which needs the Lean toolchain and runs in CI.

The per-claim record and the cross-unit list are in verification/audits/manuscript/intro-corpus-audit-20261026/tracks/SC35-kernel-anchors/README.md.

No merge is authorized. Merging needs owner approval at an exact SHA and a normal merge commit.

Generated by Claude Code

claude added 2 commits October 28, 2026 04:21
@claude
SC-35 (PR-G): kernel-only results into Main, with census anchors
7b25ac6 
Main §2.3:
- the history-readback theorem's kernel note now cites
  pIndivisible_of_rooted_identity_return_of_overlap for its final clause and
  names the three steps that stay on paper (CON-41);
- new Theorem (overlap and return) at the kernel theorem's exact strength,
  with every hypothesis: finite sets, a bijection, one hidden prior shared by
  every root and not required to have full support, Gamma_n = I, and an
  overlap of two distinct rows at some s < n;
- new routed-readback paragraph (CON-43, OD-5): the storage-time reading is
  primary, the seed-conditioned one secondary; the conclusion is indivisible
  at every return after s; the readings are incomparable as exhibited at
  K = 2; the clause is not established at a physical cut.

Main §3.4: the consolidation remark states the rooted all-time
classification with a witness for each direction (§A.34) and narrows open
item (a) to multi-time laws (CON-28). The status ledger row and ROADMAP
carry the same narrowing.

Census (§A.35):
- RecurrenceHorizon, PhysicalC4Discharge, PhysicalC4StorageReadback and
  RootedClassification* move from kernel-only to current, with Main anchors;
- the census note's rows are updated;
- guards R7-RCH and R7-RCL are re-pinned to the new state (mutation-tested);
- Introduction is not added to the manuscripts list: no tool reads it.

Coverage: new MAIN:T-overlap-return at K3; the history-readback theorem is
regraded from P to K2, with the paper steps named in delta.

Main.tex/.pdf rebuilt (98 pages). No Lean file changed. Track README and
check under
verification/audits/manuscript/intro-corpus-audit-20261026/tracks/SC35-kernel-anchors/.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y87wExth9RoUb3dtbumhTb
@claude
SC-35 review fixes: keep the history theorem at P, exact ROADMAP and …
07af6cf 
…Main wording, harden guards

Applies the independent review of 7b25ac6 (ACCEPT WITH CHANGES).

F1: MAIN:T-history-readback-finite-recurrence-implies returns to P, with
its base checks and delta. The note records that the final clause is
kernel-proved through MAIN:T-overlap-return (its own K3 entry), and that
three steps stay on paper:
- the history-to-non-permutation step;
- the non-permutation-to-overlap step;
- Gamma_L = I.

F2: ROADMAP gives the classification's setting (a finite visible set; one
finite hidden set, one bijection, one shared prior) and the witness of each
direction.

F3: in the Main status ledger, "classified (identity root, row-stochastic,
periodic; kernel)".

F4: in the Main consolidation remark, "has an exact answer".

F5: R7-RCH and R7-RCL ban RecurrenceHorizon and RootedClassification in
every scanned manuscript except Main. R7-RCH pins "not an accessible
window" and "is not established" in the routed-readback paragraph.
sc35_guard_mutations.py catches all six one-at-a-time mutations; its
output is retained.

The track README and sc35_check.py are updated to match. Main.tex/.pdf are
rebuilt (98 pages).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y87wExth9RoUb3dtbumhTb
This was referenced Oct 28, 2026
Closed
Closed
Merged
Closed
Merged
amaybaum pushed a commit that referenced this pull request Oct 31, 2026
@claude
fix(D-10): Main kernel anchors for the overlap route, routed readback…
1bc80f2 
… and rooted classification

Re-applies #973's (SC-35) kernel anchors onto main; wording from refs/audit/pr973, every cited
Lean statement re-read. No theorem upgrade, no existing grade changed, no Lean code changed.

- Main 2.3:139 (history-readback proof note): final clause cited to
  pIndivisible_of_rooted_identity_return_of_overlap; the three remaining paper steps named.
- Main 2.3:143-147 (new): Theorem (overlap and return) with proof and kernel note; Routed
  readback paragraph (storage-time and seed-conditioned readings, return-horizon scope,
  incomparability at K = 2, not established at a physical cut).
- Main 3.4:640 (consolidation remark): rooted all-time classification with a witness per
  direction (A.34); open item (a) narrowed to multi-time laws.
- Main 4.5:733 (status row) and verification/ROADMAP.md:1571: same narrowing (A.25).
- lean-manuscript-census.json: four families kernel-only -> current with Main anchors and one
  note sentence each, applied to main's current registry (A.35); census note rows to match.
- edge_rigidity_probe.py R7-RCH/R7-RCL re-pinned as in #973 (module names allowed in Main only;
  Main statements' hypotheses pinned); mutation-checked locally.
- coverage/LEDGER.json: new MAIN:T-overlap-return entry (K3, required by coverage completeness);
  history-readback entry keeps P, note added.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
This was referenced Nov 1, 2026
Open
Merged
Open
Merged
@amaybaum Claude

amaybaum commented Nov 3, 2026

Copy link
Copy Markdown
Owner Author

Closed unmerged: fully landed. #1019 D-10 1bc80f20 (+ review fix 1cfbe6b1 at Main:139) carries:

  • the Theorem (overlap and return), Routed readback, the rooted all-time classification and the status row. Main :143–147, :640 and :733 are verbatim equal to this PR's head 07af6cf3;
  • the census anchors;
  • LEDGER MAIN:T-overlap-return K3;
  • the R7-RCH/RCL re-pins.

D-10's commit message cites refs/audit/pr973, which is not a ref in the repository. The wording's only resolvable source is this branch, corpus/sc35-kernel-anchors at 07af6cf3, which is kept for that reason. The SC35 check scripts support no claim beyond the kernel, census and guards on main.

Generated by Claude Code

@amaybaum amaybaum closed this Nov 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@amaybaum @claude