[amaybaum]

This PR is the follow-up to #937 that the owner directed on 2026-10-26: "Correct the remaining 'ħ is derived' claims to distinguish genuine derivations from calibration or consistency relations. Reconcile θ₀ against one authoritative definition."

Change

Owner decisions. The owner (amaybaum, 2026-10-26) chose O1-A, O2-a, O3-b, O4-a, O5-a, O6-A and O7-a, with two qualifications:

• O4: the 95% dressing interval is conditional on the linear-response model, the sensitivity coefficient κ ≈ −35 and the range of λ_E/λ_A1. It is not a model-independent exclusion, and the loop comparison is compatible with it, not a confirmed prediction.
• O6: renormalization-group running is one possible explanation, not a demonstrated mechanism.

Corrections. There are 106 edits across 25 manuscript files, 70 of them mirrored into FULL:

• 46 ħ edits, distinguishing derivation from calibration and consistency;
• 19 θ₀ edits, on the PDG 2024 basis of SM:903: θ₀ = 0.2222248 ± 0.0000063, 0.001% from 2/9;
• 8 stale mass rows, plus the decision sites and two residue sites.

Review finding F1. H-slope is now stated in Lemma 23.0 and in the proofs of Lemma 23.0 and Theorem 23, within O1-A.

Ledger. SUBSTRATUM:T-23 and SUBSTRATUM:L-23.0 are re-affirmed.

Rebuilt. GR, SM, Main, Substratum, Structure, Methodology, Explainer, Juno and the book.

Record

The record is in verification/audits/manuscript/hbar-theta0-20261026/:

• AUDIT.md;
• decisions/DECISIONS.md, with the exact texts;
• CHANGE-NOTE.md, listing every site old → new;
• review/REVIEW.md, the review of the audit;
• review/REVIEW-CORRECTIONS.md, the independent review of the corrections. Its verdict was REVISE (F1). The confirmation of 3165af1c is ACCEPT.

Verification

• CI: run 40390672238 on 3165af1c is green: 25 checks pass and 1 placeholder job is skipped. main (b64919cd) is an ancestor of the head.
• Local checks: coverage, voice, claims, duplicate, staleness, mirror, citation, architecture, dependency-label --strict, census and legacy-records all pass.

Merge approval: the owner, 2026-10-26, at 3165af1c.

🤖 Generated with Claude Code

https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

[amaybaum]

CI on 016696c3: "Mathlib bridge" failed in its Install elan step, before any build ran. The cause is that releases.lean-lang.org returned HTTP 504 during the toolchain download. The same outage hit #935 and #938 at the same time.

This is not a failure of this PR. The commit adds only audit records, and no Lean code ran. I will re-run the failed job once when the run completes.

---

Generated by Claude Code

[amaybaum]

Ready for merge approval at 3165af1c712d799e31058ad1b767815c79d46dc3. Merge approval itself is still yours.

Owner decisions applied (amaybaum, 2026-10-26): O1-A, O2-a, O3-b, O4-a, O5-a, O6-A and O7-a, with the two qualifications:

• O4: the 95% interval is stated as conditional on the linear-response model, the sensitivity coefficient κ ≈ −35 and the range of λ_E/λ_A1. It is not described as a model-independent exclusion. The loop is described as compatible with the interval, not as a confirmed prediction.
• O6: renormalization-group running is presented as one possible explanation. The text adds that the agreement of the mass ratios does not by itself establish it.

Commits

• 4ed4c6e6: merge of main b64919cd; no conflicts.
• 2cb44824: the full approved set.
  • 106 edits across 25 manuscript files, 70 of them mirrored into FULL.
  • The ħ, θ₀ and stale-mass-row corrections, plus two residue fixes the final search turned up (R1 at ch06:179, R2 at ch07:8).
  • SUBSTRATUM:T-23 re-affirmed.
  • GR, SM, Main, Substratum, Structure, Methodology, Explainer, Juno and the book rebuilt.
• 3165af1c: the independent review's required change, F1.
  • H-slope stated in Lemma 23.0 and in the proofs of Lemma 23.0 and Theorem 23. This falls within O1-A.
  • SUBSTRATUM:L-23.0 re-affirmed (11c8a93f… → fd8439a8…).
  • Nit N1 applied to the O4 sentence.

Review

• review/REVIEW-CORRECTIONS.md reviews 2cb44824, verdict REVISE (F1). It checks:
  • every changed site against the DECISIONS texts, by mechanical re-application;
  • that FULL mirrors the chapter edits;
  • that both qualification adjustments meet the owner's wording;
  • the residue fixes;
  • stale figures, by re-grep;
  • the Category A count, which is 8.
• The reviewer's confirmation of 3165af1c is ACCEPT: the diff is exactly F1, N1 and the ledger change, plus the rebuilt outputs and the records.

CI. Run 40390672238 on 3165af1c is green: 25 checks pass and 1 placeholder job is skipped. Main (b64919cd) is an ancestor of the head and has not moved, so the pull-request merge tree is the head tree.

Local checks. All pass: coverage (128 statements), voice, claims, duplicate, staleness, mirror, citation, architecture, dependency-label --strict, census and legacy-records.

---

Generated by Claude Code

[amaybaum]

Merge record

Merge commit: eae01647f50d9e2aa90957fbd6c59d8cf44e7681 on main, a normal merge commit.

Verified after the merge:

• Parents: b64919cd, the previous main, and 3165af1c, the reviewed and approved head.
• Tree: 769915427f6debcc9278f2e9090b08823087b391, identical to the tree of 3165af1c. The change set is the reviewed one.
• Reachability: 3165af1c is an ancestor of main.
• Main CI: push run 40395660130 on eae01647 is green.

Before the merge:

• Owner's conditions (amaybaum, 2026-10-26): all were met at 3165af1c.
  • The independent review was ACCEPT on that exact head.
  • PR CI run 40390672238 was green on that head, with main an ancestor of it.
  • O1–O7 and both qualifications are applied with no expansion of scope.
  • The ledger and the FULL mirrors are synchronized.

---

Generated by Claude Code