wave 10b of 16

[phasetr]

Refs #4984

Wave 10b of 16 — AmbientLattice/SpecialCases/ header rewrite (remaining 9 families)

Split from wave 10 (originally scaffolded as the full 149-file SpecialCases/ wave in PR
#5009 — that exceeded the design report's ≤100-file/wave and came within 1 declaration of the
≤300-declaration/wave guard rails, §3). Split along family boundaries into 10a
(docs/4984-w10-specialcases-headers, PR #5009, HighTemperature*/Mayer*) and 10b (this PR,
the other 9 families). Neither family is divided between the two sub-waves. Overall campaign
wave count stays 16 (this is two PRs replacing one, not a renumbering of waves 11–16).

Scope frozen against main = 7ea1cbdd5549b566730db46d3192f26fc1468adb (wave 9 / PR #5006's
merge commit, unchanged since the original wave-10 freeze), recorded in the freeze comments:

• Original wave-10 freeze (149-file measurement this sub-wave is drawn from):
  Batch-migrate the remaining stale header charges to intension-only prose (PR-3+ wave campaign, 16 waves: all merged; Lean lane at zero, docs lane D1 open/unscoped) #4984 (comment)
• This sub-wave's split freeze (single source of truth for the exact 75-file set — this body
  does not restate it):
  Batch-migrate the remaining stale header charges to intension-only prose (PR-3+ wave campaign, 16 waves: all merged; Lean lane at zero, docs lane D1 open/unscoped) #4984 (comment)

Scope

metric	value
files	75 (9 families other than HighTemperature*/Mayer*)
charges	137
declarations	131
MISSING_MODULE_DOC	0 (pure rewording)

Per-family subtotals:

family (filename prefix)	files	charges	declarations
PolymerFreeEnergy*	26	49	46
PartitionFreeEnergy*	15	29	26
JointRegularity*	7	13	10
Susceptibility*	7	11	11
FreeEnergy*	6	10	12
JointAnalyticity*	5	10	10
PartitionFunction*	4	8	6
VdPolymerFamilies*	3	5	6
InfiniteVolume*	2	2	4
total	75	137	131

Frozen file set (75 files)

See the split freeze comment for the full list — not restated here to avoid a second copy that
can drift: #4984 (comment)

Acceptance criteria (AC1–AC8, carried forward from #4984 — all lessons from waves 1–9 apply)

• AC1 — coverage. Exactly the 75 frozen files, only them; intension-only conversion
  (R1/R2: counts, exhaustive enumerations, ## Moved: blocks, in-header PR provenance all
  removed, not just number-corrected). Cardinality-idiom sweep reported as measured hits with
  adjudications, never a blanket "0 hits".
  • git diff --name-only origin/main...HEAD = 76 paths: the 75 frozen files (set-differenced
    against the freeze list, empty both ways) plus scripts/audit/header_claim_baseline.tsv,
    the only non-frozen path. Diffstat 733 insertions(+), 1403 deletions(-). Cardinality-idiom
    sweep: 0 surviving hits, one draft hit found and fixed before push.
• AC2 — ratchet. --findings reports 0 charges on all 75 files; --check green with
  baseline ratcheted as a multiset; --check-baseline-drift green; --self-test green,
  instrument unmodified in this PR. Review on the --findings diff, never totals. Any
  deviation explained in this body, not absorbed silently. Re-derive the NARROW_CHILD/
  RELOCATION class split for this 75-file subset at implementation time (the wave-10
  freeze's combined 143/126 covers the full 149, not this sub-wave alone). This sub-wave
  lands after 10a if both are open concurrently — re-verify --check PASS on the current
  baseline before implementing (10a's merge moves the baseline; do not assume it is still at
  the freeze-time 453/362 figures).
  • --check before: baseline 363 charges / 277 keys, live 363/277, K0–K4 PASS.
  • --check after: pre-re-pin live 262 / 190 ("87 baseline key(s) now below their pin",
    informational); after --baseline re-pin, PASS, live == baseline at 262 charges / 190
    keys, K0–K4 PASS. Movement −101 charges (exactly the 75 files' charged population), −87
    keys; telemetry 39 → 3, not pinned.
  • --findings on the 75 files after: 0 rows, charged or telemetry.
  • --check-baseline-drift: PASS, base 9c21660a via origin/main. --self-test: OK, 184
    tests, instrument unmodified (git diff origin/main --stat -- scripts/ = one file,
    header_claim_baseline.tsv, −87 lines).
• AC3 — header truth, 100% of the wave, not a sample. Every file reviewed against its
  actual declaration list: identifiers in a statement/proof (not just a name); citation span
  covers every realized §x.y; strength words realized by an actual conclusion head;
  universal words true of every declaration; hypotheses at binder precision; route verbs
  match the actual tactic script.
  • Zero/nonzero mathematical characterization defect class (wave 9 lesson, mandatory here).
    Any header sentence giving a closed-form expression and asserting it vanishes / does not
    vanish / has a fixed sign states, in order: the closed form itself → the admissible domain
    of every free parameter under the file's own hypotheses → the exact root set of the
    expression restricted to that domain → the sign on each remaining sub-interval. Do not check
    only "the expression" in isolation from the hypothesis-admissible parameter range (wave 9's
    M1/M2 both failed exactly this way). This sub-wave carries closed-form-heavy families
    (PartitionFunctionClosedForms*) — sweep all zero/nonzero/vanishing/sign claims across the
    75 files explicitly, not just the files whose names suggest it.
  • No negative provenance claims (wave 9 lesson, N1, mandatory here). State only what a
    proof is (the positive fact, discharged by exhibiting the proof term or citing the exact
    upstream lemma it applies). Never state what a proof is not derived from, or that some
    fact does not follow from some other route — a negative claim requires exhausting the
    transitive proof chain, and wave 9 produced a false one on the first attempt.
• AC4 — zero Lean logic change. Comment-stripped token stream + non-blank comment-stripped
  line list byte-identical to main; comment-aware per-file import-list equality (not
  git diff -G'^import'); every non-blank diff line inside a comment span, and every
  blank-line deletion counted and reported separately — blank lines are invisible to all three
  facets above, so the criterion states them rather than asserting them away.
  • AC4: 75 file(s) compared against origin/main; PASS -- no Lean content changed
    (.self-local/tmp/w10b/ac4_check.py, --self-test OK, 16 checks). Diff line census over the
    75 files: 1194 comment lines removed / 705 added; 94 blank lines removed / 0 added, in 35
    files, outside any comment span; 0 code-carrying lines touched. The 94 blank lines are the
    separators that sat between a deleted ## Moved: / section block and the following code.
    Net line movement 583 agrees with git diff --stat (1316 − 733 on the 75 Lean files) and with
    the reviewer's independent classifier.
• AC5 — gates, zero regressions, evidence filled incrementally as each gate runs (not
  left as scaffold past the point real output exists):
  • lake build: exit 0, 4944 jobs, 0 warnings, 0 errors, 15 min 45 s wall; recompile cone
    1096 modules rebuilt of 4944 jobs. Independently re-run by review: token-identity (AC4)
    makes a build regression impossible in principle, and CI's build job on 4bfc5c9b is
    pass (26m16s).
  • lake exe GKSTest: exit 0, "=== All tests passed ===".
  • lake build test.IsingModel.SentinelProps: exit 0, 901 jobs, 0 warnings.
  • scripts/audit_gate.py --self-test then --full: OK, 179 tests (1 skipped), then
    PASS — V1 no axiom (1922 files), V2 no sorry/admit/native_decide (1922 files), V3 13
    capstones all ⊆ {propext, Classical.choice, Quot.sound}, V4 no Japanese (1977 tracked files).
    Independently re-run by review with the same result.
  • scripts/citation_audit.py (pre-registered expect 0 net movement): PASS, findings 694,
    self-refs 112, ratchet "37 cleared, 0 new" — byte-identical to the pre-edit run. Independently
    re-run by review with the same result.
  • scripts/import_dag_contract.py --check + scripts/test_import_dag_contract.py: PASS, 0
    baseline entries, unchanged; OK, 77 tests. Independently re-run by review with the same
    result.
  • grep -rn "sorry" IsingModel/ = 2 hits, both the phrase "no sorry" inside doc comments of
    files this wave did not touch; 0 in code.
  • codepoint line length ≤100 over every touched file: max 94 over every non-import line
    in the 75 files; 2 lines exceed 100, both pre-existing import lines left byte-identical
    by this PR. Independently re-verified by review with an oracle written from scratch: same 2
    lines, same max 94.
  • all edited prose English only: 0 Japanese codepoints in the 75 headers, confirmed
    independently by audit_gate.py V4 and by review's own sweep.
• AC6 — review discipline + coverage attestation. dev-review + independent Codex
  cross-review to a clean round (zero findings both sides); sampling forbidden; full
  re-review after every fix; dev-issue-manager resolution verification before any
  completion claim. Each reviewer, each round, records: reviewed commit SHA; H/H module
  headers; D/D declarations (denominator 131, to be confirmed); A/A newly authored
  headers (denominator 0); per-family D/D subtotals mandatory — the 9 strata above, no
  blanket sentence spanning a family boundary unless independently substantiated in each
  family it touches.
  • Round 1 (reviewed commit 4bfc5c9b): dev-review's own verdict on the Lean content is
    APPROVE — no defect in the diff, in any of the 75 headers, or in any of the 131
    declarations, verified against a from-scratch kernel telescope (lake env lean + #check on
    all 131) and independent AC4/zero-nonzero/negative-provenance/exclusivity/mixed-layer sweeps.
    Codex's independent cross-review returned REQUEST CHANGES (one BLOCKING on AC4 wording,
    one MEDIUM on issue Errata: the polymerFreeEnergy_le_of_le_strict_form tower proves one proposition twice at five layers, and neither member is strict #5013's census); dev-review reproduced both measurements exactly and
    downgraded the BLOCKING finding to LOW (claim-precision, not code) — nothing about "zero
    Lean logic change" was violated, only the comparator's PASS message asserted more than the
    three facets it actually compares (blind to blank-line-only deletions). Coverage attestation:
    75/75 module headers, 131/131 declarations, 0/0 newly authored headers, both
    reviewer and implementer independently. Per-family D/D (both sides agree): PolymerFreeEnergy*
    46/46, PartitionFreeEnergy* 26/26, FreeEnergy* 12/12, Susceptibility* 11/11,
    JointRegularity* 10/10, JointAnalyticity* 10/10, PartitionFunction* 6/6,
    VdPolymerFamilies* 6/6, InfiniteVolume* 4/4.
    • F1 (LOW, claim precision) — fixed without touching Lean: ac4_check.py's message and
      this body's AC4 criterion corrected to state "every non-blank diff line inside a
      comment span, and every blank-line deletion counted and reported separately"; the census
      (94 blank / 35 files / 0 code) is now printed and self-tested (16 checks, up from the
      original set).
    • F2 (MED, errata accuracy, outside this PR's files) — issue Errata: the polymerFreeEnergy_le_of_le_strict_form tower proves one proposition twice at five layers, and neither member is strict #5013's layer census was
      short by one layer (4 layers/8 declarations, correct figure 5 layers/10 declarations, both
      reviewer and implementer independently found the same fifth pair); fixed by rewriting
      Errata: the polymerFreeEnergy_le_of_le_strict_form tower proves one proposition twice at five layers, and neither member is strict #5013's body directly on GitHub (title, table, consumer census, completeness check) and
      posting a correction comment. No Lean file touched, as Errata: the polymerFreeEnergy_le_of_le_strict_form tower proves one proposition twice at five layers, and neither member is strict #5013 stays out of this wave's
      scope.
    • Round 1 is the only round — no second round was required (both findings were claim-layer,
      fixed without a Lean-content change, and re-verified against the same reviewed commit
      4bfc5c9b).
• AC7 — falsification rule. ≤3 rounds confirms the size premise at 75 files / 131
  declarations for pure rewording (well within the 299-declaration/149-file anchor the
  un-split wave 10 would have tested); 4+ rounds falls back to the largest declaration count
  smaller than this one that has actually closed at ≤3 rounds. New-authoring risk
  calibration caveat (wave 9 lesson, mandatory to state, not to apply here): this sub-wave
  carries 0 authoring files (MISSING_MODULE_DOC = 0), so the authoring-risk multiplier
  does not apply.
  • Result: 1 round, with a minor claim-precision correction (F1) — matches wave 10a's
    clean-round-1 result on a 9-family, non-uniform-instance-telescope corpus (168/168 declarations
    shared one instance binder in 10a; here 3 of 131 deviate in three different ways, all found
    and correctly disclosed before review). The size premise is confirmed at 75 files / 131
    declarations.
• AC8 — pre-review checklist over 100% before round 1. Predicate noun phrases resolved
  against repo defs; binder-level hypothesis scoping by machine telescope for all 131;
  bare-cardinality idiom sweep (measured, not assumed 0); same-file /-- ↔ /-! consistency;
  page-scoped citation verification (pdftotext -f N -l N, never flat OCR nor another repo
  copy); per-item scope-qualifier check on any mixed-layer headers; instance-binder census;
  PR-body raw-HTML self-check; AC5 evidence inline with real numbers, never left [PENDING]
  past the point the gate has actually run.
  • Predicate noun phrases resolved against repo defs (e.g. "vertex-disjoint compatible polymer
    families" ↔ vdCompatiblePolymerFamilies, "polymer set" ↔ allPolymers, "bounded edge
    density" ↔ BoundedEdgeDensity).
  • Binder-level hypothesis scoping by machine telescope for all 131: 76 declarations have an
    empty Prop-hypothesis list, 55 have a non-empty one; independently reproduced by review's own
    lake env lean telescope (131 entries, 0 errors), which additionally surveyed the instance
    list of all 131 (128 share [DecidableEq V] + one stagewise Fintype; the 3 deviations are
    exactly the 3 the implementer disclosed, all CONFIRMED).
  • Bare-cardinality idiom sweep: measured, 0 surviving hits (implementer, adversarially
    self-tested regex); review's own wider sweep found 1 hit, adjudicated as the named-objects
    exception (a hypothesis list of 4 pairwise-distinct indices, "the six inequalities").
  • Same-file /-- ↔ /-! consistency: machine probe, 0 flagged; review independently
    confirmed all 131 /-- blocks are byte-identical to origin/main (this PR modified no
    declaration doc).
  • Page-scoped citation verification: not applicable — no produced header carries a
    literature citation (citations live in the untouched /-- docs), following wave 10a's
    established style; this also keeps the wave clear of Errata: 373 tracked occurrences (over 363 lines) cite the section-18 programme marker as "GJ §18.x", but Glimm-Jaffe Chapter 18 is the continuum cluster expansion; the lattice anchor is Friedli-Velenik §3.7.3 (3.45)/(3.46), pp. 116-117 #4998's §18.x mislabelling.
  • Mixed-layer scope check: 3 instance-mixed files (FreeEnergy.lean, FreeEnergyTrivialSlicesJZero.lean,
    InfiniteVolume.lean's inducedGraph_bot) each state their per-declaration instance/Prop
    split rather than a blanket claim; review independently confirmed the PolymerFreeEnergy*
    stage-subgraph vs along-exhaustion distinction with 0 misattributions across all 26 files.
  • PR-body raw-HTML self-check: none present.
  • AC5 evidence inline with real numbers: see AC5 above.

Accumulated lessons carried forward from waves 1–9 (standing checklist)

• Waves 1–4: predicate noun phrase must resolve against a repo def; binder-level hypothesis
  scoping; bare-cardinality idioms eliminated semantically, not regex-dodged; same-file /-- ↔
  /-! consistency.
• Wave 5/6: declaration counts must be comment-and-attribute-aware (strip comments, then peel
  leading @[...] attribute groups and modifiers before matching a declaration keyword). AC5
  evidence must be filled incrementally as gates actually run, never left as a stale scaffold.
• Wave 7/8: per-item scope-qualifier check required on mixed-layer files; freeze-time charge
  counts can conflate --findings rows with charges — recount and correct in-body if the
  two diverge.
• Wave 9 — three methodology lessons, carried into AC3/AC7 above:
  1. New-authoring risk calibration is not transferable and does not apply here (0 authoring
     files).
  2. The "zero/nonzero mathematical characterization" defect class: closed form → admissible
     domain → root set → sign, always in that order.
  3. No negative provenance claims — state only positive facts about what a proof is.

What the gates do not guarantee

Nothing mechanical in this repository checks header truth. The ratchet detects only
recognized legacy inventory syntax; lake build never reads comment content; audit_gate V1–V4
are axiom/sorry/capstone/Japanese only; citation_audit has previously been shown insensitive to
citation-only diffs; import_dag_contract sees no prose. The truth guarantee for this wave rests
on the manual read and on the independent review passes.