Skip to content

SC-40: (C2)/(C3) statements and probe evidence in Main §1.3 - #974

Closed
amaybaum wants to merge 3 commits into
mainfrom
corpus/sc40-c2-c3-statements
Closed

amaybaum wants to merge 3 commits into
mainfrom
corpus/sc40-c2-c3-statements

Conversation

@amaybaum

Copy link
Copy Markdown
Owner

Source-correction unit for #946 (gate) and #918 (Introduction), from the full-corpus audit of #918 at 60c976fe.

Base and history

  • Base: main at 0d917665.
  • Head: e27f7866.
  • The independent review returned ACCEPT at a9480336, after one fix round (B1, B2 and O1–O6).
  • e27f7866 adds one doc-only change to the unit README, applying that review's optional finding. It changes no manuscript, ledger or script.

Corrections

  • Main:620 (B1, O5). (C3) holds in every faithful realization, by data processing applied to the whole visible future. The bound $\log_2|\mathcal C_H|\ge I^*$ is attained by some realizations. The probe sentence now matches primitive_probes.py:
    • it checks C1 ⇐ C4 in exact rational arithmetic at small sizes;
    • it checks the capacity bound only in its per-order form, $\max_k M_k\le\log_2|\mathcal C_H|$, over realizations with a readback gap, in floating point.
  • LEDGER primitive_probes.py row (B2). Each clause now carries its sizes, orders and arithmetic. The CMI>0 test uses a 1e-12 floating-point threshold. The prior is uniform throughout.
  • Main:82 (O1). C1 is a necessary diagnostic. C3 holds in every faithful realization by the capacity bound.
  • Main:78 (O2). An exact attainment witness: the swap $\varphi(v,h)=(h,v)$ at (2,2), with $M_k=I^*=1$ bit $=\log_2|\mathcal C_H|$. It is check (5) in c2_c3_check.py, all in exact arithmetic.
  • primitive_probes.py (O3). Only strings and comments change. The code AST is identical, and the outputs differ in the two (B) print lines.
  • Main:463 (O4). The physical-memory theorem's coupling-step model and conditional-mixing hypothesis are restated exactly. The model references at Main:76 and :732, Substratum:129 and :137, and glossary:27 / FULL:6627 point to that theorem.
  • Coverage.
    • MAIN:T-physical-memory-c2-process-form is re-affirmed at P.
    • MAIN:T-statement is re-affirmed at SUM.
    • No level changes.
  • Rebuilt. Main, Substratum, GR and the book.
  • Lean. No Lean change.

Checks

The reviewer re-ran these from copies, under python3 -I.

  • c2_c3_check.py: ALL PASS. The output is byte-identical to the committed .out.
  • primitive_probes.py: passes at both heads.
  • coverage_check: OK, 128 statements.
  • edge_rigidity_probe: all checks pass.
  • release_gate: every step passes except lean-axioms, which runs in CI.

Overlaps, resolved at reconciliation

The per-claim record is in verification/audits/manuscript/intro-corpus-audit-20261026/tracks/SC40-c2-c3-statements/README.md.

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


Generated by Claude Code

…om (C4)

- Physical-memory theorem (Main §3.4): the contrapositive is stated in the
  bounded quantity M_k = I(X_<k; X_k+1 | X_k) at coupling time k, with
  eps_min(M, n_V) defined (the I* form does not follow and is ill-posed for
  I* >= 2 log n_V). Propagated to Main :76, :453, :472, :492, :732,
  Substratum :129, :137, glossary :27 and FULL.
- SC-19: (C1) follows from (C4); (C3) holds in every faithful realization by
  the whole-future data-processing bound. Main :72, :78, :620, GR :52,
  Substratum :129, ch00 :37, ch01 :133/:201/:259, ch07 :30, glossary :29, FULL.
- Coverage: MAIN:T-physical-memory-c2-process-form fingerprint re-affirmed (P).
- Rebuilt Main, Substratum, GR and the book. Track record, exact check and
  output under tracks/SC40-c2-c3-statements/.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y87wExth9RoUb3dtbumhTb
… the physical-memory theorem

- B1: Main :620 states what primitive_probes.py checks (C1 from C4 exact; the
  per-order capacity bound on gap realizations in floating point); O5
  "checkable necessary conditions". Absorbs SC-38's edit to the same line.
- B2: LEDGER.json unattached-checker text for primitive_probes.py restated
  clause by clause against the probe.
- O1: Main :82, C1 follows from C4 and C3 holds by the capacity bound.
- O2: Main :78 gives the probe's scope and the exact swap witness.
- O3: primitive_probes.py strings and comments only (AST identical with prints
  and docstrings excluded; output differs only in two print lines).
- O4: physical-memory theorem head names the coupling-step model; references
  in Main, Substratum and the glossary/FULL point to it. Fingerprints of
  MAIN:T-physical-memory-c2-process-form and MAIN:T-statement re-affirmed.
- O6: README evidence labels; overlaps with #968 (:82) and SC-38 (:620).
- Rebuilt Main, Substratum and the book; check (5) added for the witness.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y87wExth9RoUb3dtbumhTb
…ew, not by a track script (#946)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Y87wExth9RoUb3dtbumhTb

Copy link
Copy Markdown
Owner Author

Lean kernel check failed on e27f7866 (run 40634057548) at its install step, before any check ran.

  • The download of the Lean toolchain (lean-4.35.0-linux.tar.zst from releases.lean-lang.org) failed with an SSL connect error.
  • This PR changes no Lean file and nothing in the workflow.
  • I will re-run the failed job once the run finishes. If it fails again, I will treat it as a real failure and investigate it.

Generated by Claude Code

amaybaum pushed a commit that referenced this pull request Oct 31, 2026
…nd in M_k

#974 (SC-40), checked against Main 3.4 on main: Theorem (C3 necessity)
(:500) bounds I(X_<t; X_>t | X_t) <= log2 m from determinism alone, so C3
holds in every faithful realization and does not follow from C4; the
physical-memory display (:464) bounds M_k = I(X_<k; X_{k+1} | X_k) only,
not I* = sup_t I(X_<t; X_>t | X_t) (:508), so the contrapositive is
eps_min(M_k, n_V) at an accessible order k.
- C1/C3 attribution: Main.md:72, :78, :82 (main's wording differs from
  #974's base; only the C1/C3 clause changed), :620; GR.md:52;
  Substratum.md:129; ch00:37; ch01:133, :201, :259; ch07:30; FULL:273,
  :477, :545, :603, :1905 (mirrors).
- eps_min(I*) -> eps_min(M_k, n_V), "M_k > 0 at an accessible order k":
  Main.md:76, :453, :465 (with the definition and existence of eps_min),
  :472, :492, :732; Substratum.md:129, :137; glossary:27 / FULL:6630.
- Main.md:78 "finds the bound SATURATED" -> per-order max check (floating
  point) plus the exact swap witness (M_k = 1 bit = log2|C_H| at (2,2));
  caps removed (§A.33).
- Main.md:463: coupling-step model stated.
- glossary:29 / FULL:6632: bound stated for the whole visible future.
- primitive_probes.py: header comments and two printed claims aligned
  ("C4 forces C3" removed); no logic change.
- LEDGER.json: primitive_probes certified scope as #974; MAIN:T-statement
  and MAIN:T-physical-memory-c2-process-form fingerprints re-affirmed
  (summary row; P row, probe c2_mixing_probes unchanged), assumptions
  state the coupling-step model.
Left unchanged: ch01:155 / FULL:499 ("C1 and C3 are its preconditions"),
Substratum:373 ("C1 and C3 diagnose"): both true as necessary conditions.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb
amaybaum pushed a commit that referenced this pull request Oct 31, 2026
…d scope

#975 (SC-38). sc38_exact.py from refs/audit/pr975 re-run here (python3 -I,
scratch dir): output byte-identical to the PR's committed sc38_exact.out;
at (n_V,|C_H|) = (2,3), t = 2, uniform prior, 16 laws of (X0..X3) with
M_2 > 0, 2 attaining M_det = M_t, max residual 2/3 bit exactly (C2, C5);
memory_probes.py's old signature merged two laws (C3, C4: "1 of 15").
- Main.md:610: "one of fifteen distinct processes ... 0.667 bits" ->
  "sixteen distinct laws of (X0..X3) ... M_det = M_t for two of them ...
  2/3 bit"; agreeing laws prior-independent.
- Main.md:170, :606, :616: "Certified exactly" / "exact" -> checked, with
  laws/gaps in exact rational arithmetic and information quantities (or the
  predictive floor) in floating point, as the cited probes compute them.
- Main.md:178 "A Minimal Model" -> "A Six-Hidden-State Model" (Main's
  two-hidden-state revival example is smaller); ch01:135 / FULL:479,
  ch01:273 / FULL:617 (mirrors), Explainer.md:725, main_repro/README.md:8
  (also "exact enumeration" -> floating point: numpy).
- Main.md:620: already #974's line (D-6), which carries #975's labels.
- memory_probes.py: groups by the law of (X0..X3); prints "2 of 16 laws"
  (re-run: ALL CHECKS PASS). c4_backflow_probes.py, hidden_memory_probe.py:
  printed wording ("certified"; "M_det = M_t remains OPEN") aligned with
  Main:170 / :610.
- LEDGER.json: MAIN:T-canonical-predictive-quotient-purification-ingredient
  fingerprint re-affirmed (wording of the check parenthetical only).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum commented Nov 3, 2026

Copy link
Copy Markdown
Owner Author

Closed unmerged.

Branch corpus/sc40-c2-c3-statements is kept.


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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants