wave 10a of 16

[phasetr]

Refs #4984

Wave 10a of 16 — AmbientLattice/SpecialCases/HighTemperature* + Mayer* header rewrite

COMPLETE. Split from wave 10 (was previously scaffolded as the full 149-file
SpecialCases/ wave — that exceeded the design report's less-than-or-equal-to 100-file/wave
and came within 1 declaration of the less-than-or-equal-to 300-declaration/wave guard rails,
design report section 3). Split along family boundaries into 10a (this PR,
HighTemperature*/Mayer*) and 10b (branch docs/4984-w10b-specialcases-headers, scaffolded
as PR #5010, the other 9 families, not yet implemented). 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 74-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	74 (HighTemperature* 50 + Mayer* 24)
--findings rows (charged + telemetry)	132
charged population (the ratchet's authoritative figure)	90 (32 NARROW_CHILD + 58 RELOCATION)
declarations	168
MISSING_MODULE_DOC	0 (pure rewording)

Correction to the freeze figure (filed as new issue #5012): the freeze recorded "132
charges" for this sub-wave. 132 is the --findings row count, which mixes the ratchet's
90 charged rows with 42 rows the ratchet's own report prints under
# TELEMETRY (NON-AUTHORITATIVE) ... NOT part of the population, never pinned. The charged
population is 90, and the ratchet baseline (below) fell by exactly 90. This is a recurrence of
the wave 7/8 lesson already recorded in this PR's own standing checklist ("freeze-time charge
counts can conflate --findings rows with charges") — the freeze was written after that
lesson and conflated them anyway, so #5012 exists to fix the freeze procedure rather than
re-deriving the arithmetic by hand every wave.

Per-family subtotals (row counts, with the charged/telemetry split):

family (filename prefix)	files	--findings rows	charged	NARROW_CHILD	RELOCATION	telemetry	declarations
HighTemperature*	50	94	69	25	44	25	85
Mayer* (all Mayer-prefixed variants)	24	38	21	7	14	17	83
total (74 files)	74	132	90	32	58	42	168

Frozen file set (74 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. git diff --name-only 2b9cd775..HEAD = the 74 frozen files exactly,
  plus scripts/audit/header_claim_baseline.tsv (75 paths total, machine set-differenced
  against the frozen list; the baseline is the only non-frozen path). Intension-only
  conversion applied throughout: counts, exhaustive declaration enumerations,
  ## Moved:/## Removed: blocks, in-header PR provenance, and .lean path references
  were removed, not renumbered. Cardinality-idiom sweep: all draft occurrences of "Both
  statements ..." (6 files) rewritten to "Each statement ..."; 0 surviving bare-cardinality
  idioms about module inventory ("the two wrappers", "the three lemmas", "N theorems").
  Counts of named mathematical objects (two-sided bounds, two named trivial slices) are
  retained under the named-objects exception, not counted as defects.
• AC2 — ratchet.
  • --check before (base 7ea1cbdd): baseline 453 charged / 362 keys.
  • --check after (head c913cca4): PASS, live == baseline at 363 charged / 277
    keys, all five conservation laws (K0-K4) PASS.
  • --findings on the 74 files after: 0 rows, charged or telemetry.
  • --check-baseline-drift: PASS ("the pin moved only where this diff explains it"),
    base commit 7ea1cbdd via origin/main.
  • --self-test: OK, 184 tests. Instrument unmodified in this PR (only the baseline TSV
    changed, -85 lines, nothing else).
  • Class split for this 74-file subset, re-derived at implementation time (not copied from
    the combined wave-10 freeze's 143/126 over the full 149): 32 NARROW_CHILD + 58
    RELOCATION = 90 charged, matching the per-family table above exactly.
• AC3 — header truth, 100% of the wave, not a sample. Every one of the 74 files
  reviewed against its actual declaration list (identifiers, citation spans, strength
  words, universal words, binder-precision hypotheses, route verbs).
  • Zero/nonzero mathematical characterization sweep (wave 9 lesson). All 74 files
    scanned, not only files whose names suggest a closed-form claim. 26 sites make a
    vanishing/non-vanishing/positivity/strict-inequality claim; 25 are verbatim
    restatements of the pinned theorem (hypotheses included), 1 is derived and was derived
    in full (MayerEdgeCases: each zero-activity slice reduces Real.tanh applied to an
    argument that is exactly 0 by zero_mul/mul_zero/the hypothesis, admissible domain
    is all of ℝ for the remaining free parameter, so the claim is unconditional on that
    domain rather than a root-set statement). Independently re-derived by dev-review with a
    wider regex over all 74 headers: same 26-site set, no site outside it. No header
    asserts non-vanishing anywhere (0 hits for nonzero|non-zero|non-vanish|never,
    confirmed independently by dev-review).
  • Negative-provenance sweep (wave 9 lesson N1). Grepped the produced headers for
    rather than | not derived | NOT | neither | without | no hypothesis | unrestricted | instead of | as opposed | \bnot\b. 7 found in the first draft, all 7 eliminated
    before the first commit (e.g. "takes the stage volume's nonemptiness rather than
    0 < |Λ|" to "takes the stage volume's nonemptiness as a hypothesis"; "Without a
    hypothesis on |Λ|" to "Under 0 ≤ J and 0 < β alone"). A self-contradiction was
    caught in the same pass and fixed: a draft scope sentence claimed every statement in
    ...ExpansionLowerUpperConsistency carries DecidableEq V, immediately followed by "both
    statements additionally omit the DecidableEq V instance" — both theorems do carry
    omit [DecidableEq V] in, so the shared sentence was false; replaced with a file-local
    scope sentence.
    • Sweep-methodology correction (dev-review LOW-2, applied here): the implementer's
      grep pattern did not include the word "omit", so it could not have caught — and was
      never meant to catch — the one surviving sentence that legitimately uses "omits" as a
      positive deviation disclosure ("... and omits DecidableEq V",
      HighTemperatureBoundsExpansionLowerUpperConsistency.lean:8, verified true: it is the
      only file in the wave with an omit [DecidableEq V] in site). That sentence is
      correct and required, not a banned negative-provenance claim; the sweep's pattern
      description is stated here with that carve-out made explicit, rather than described as
      an unqualified "0 hits" that would misleadingly imply the pattern covers all
      negative-sounding vocabulary. dev-review's own wider regex (superset, includes
      omits?) found exactly this one additional hit and classified it correctly as a
      required disclosure, not a defect.
• AC4 — zero Lean logic change. Two independent oracles, both confirming 0 differences
  over all 74 files:
  1. In-tool guard: nesting-aware comment-stripped line list recomputed before/after every
     file, aborts on any difference — 74/74 passed.
  2. Post-hoc, independently re-derived by dev-review with a stricter oracle written from
     scratch (comment-stripped byte-exact non-comment lines with indentation preserved, not
     the implementer's whitespace-collapsed token stream): 0 differences, all 74 files.
  3. Comment-aware per-file import-list equality (not git diff -G'^import'): 196 import
     lines across the 74 files, order included, 0 files changed — confirmed independently
     by dev-review.
     Every diff hunk lies inside a comment span. git diff --check: clean.
• AC5 — gates, zero regressions.
  • lake build: exit 0, Build completed successfully (4944 jobs), wall 5:45. Zero
    warnings (grep -inE "warning|error|sorry" over the full log: 0 hits). Recompile cone:
    173 modules (74 edited + 99 downstream) = 9.0% of the 1916 tracked IsingModel
    modules, predicted from the import graph before building and confirmed after (173
    Built lines).
  • lake exe GKSTest: exit 0, all tests passed.
  • lake build test.IsingModel.SentinelProps: exit 0, 901 jobs, no warnings.
  • scripts/audit_gate.py --self-test: OK, 179 tests (1 skipped). --full: PASS (V1 0
    axiom decls / 1922 files; V2 0 sorry/admit/native_decide / 1922 files; V3 13 capstones,
    union {Classical.choice, Quot.sound, propext}; V4 0 Japanese / 1977 tracked files).
  • scripts/citation_audit.py: PASS, byte-identical before/after (verified against a
    detached git worktree at 2b9cd775): citations 2693 -> 2827 (+134); ratchet: OK -- 37 finding(s) cleared, 0 new. Zero net movement caused by this wave (inherited branch
    state).
  • scripts/import_dag_contract.py --check: PASS, 0 baseline entries, unchanged.
    scripts/test_import_dag_contract.py: OK, 77 tests. No import line added, removed, or
    moved (git diff -G'^import' and git diff -U0 | grep '^[+-]import ' both empty).
  • grep -rn "sorry" IsingModel/: 2 hits, both the literal words "no sorry" inside
    pre-existing doc comments outside this wave's files, both present verbatim on main.
    audit_gate.py V2 (the authoritative check) distinguishes these and is PASS.
  • Codepoint line length: exactly 1 line over 100 codepoints across the 74 files
    (HighTemperatureBoundsRatioLogFeFreeEnergyBoundOnly.lean:2, a 101-codepoint import
    line), byte-identical to 2b9cd775 and pre-existing/unbreakable, accepted by lake build under the repo's linter settings. Every line the implementer authored is <=92
    codepoints.
  • English only: 0 Japanese by audit_gate.py V4 and by an independent Unicode-class grep
    over the 74 files.
• AC6 — review discipline + coverage attestation.
  • Round 1 (only round — clean on first pass), reviewed commit c913cca4:
    • dev-review verdict: APPROVE. H/H = 74/74 headers. D/D = 168/168 declarations
      (HighTemperature* 85/85, Mayer* 83/83, both independently machine-counted). A/A =
      0/0 (no newly authored headers, MISSING_MODULE_DOC = 0). ~40/74 files read in full
      depth (header + every statement); the remaining 34 covered by machine sweeps
      (hypothesis-disclosure coverage over all 74, identifier existence over 31 backticked
      candidates, instance-binder census over all 168, layer partition over 8 mixed-layer
      files, AC4). 3 LOW findings, all report/PR-body layer, none in code or headers (the 3
      corrections applied in this body). No High, no Medium.
    • Codex independent cross-review verdict: APPROVE ("No real defects found"), 27
      files read in depth. Report: .self-local/tmp/codex-w10a-out.txt.
    • Full report: .self-local/reports/dev-review-4984-w10a.md.
  • dev-issue-manager resolution verification: confirmed before this completion claim (no
    unresolved findings; the 3 LOW findings are report-accuracy corrections applied in this
    body, not code defects requiring further code rounds).
• AC7 — falsification rule. Closed at round 1 — the first wave since wave 5 to
  reach a clean round from both reviewers on the first pass. Confirms the size premise at
  74 files / 168 declarations for pure rewording. New-authoring risk calibration
  caveat (wave 9 lesson, stated per AC7's requirement, not promoted further): this
  sub-wave carries 0 authoring files (MISSING_MODULE_DOC = 0), so the authoring-risk
  multiplier does not apply here — see the calibration note below for why this round-1
  result should not yet be read as confirming the broader "generative constraints
  prevent defects" methodology claim.
• AC8 — pre-review checklist over 100% before round 1. Predicate noun phrases
  resolved against repo defs (polymerFreeEnergy, mayerPartialSum,
  mayerExpansionTerm, vdCompatiblePolymerFamilies, allPolymers, evenSubgraphs,
  ursellCoefficient, clusterSeqActivity, highTempExpRate, inducedGraph,
  Exhaustion, freeEnergyAlongExhaustion, partitionFunctionAlongExhaustion,
  correlationAlongExhaustion). Binder-level hypothesis scoping by machine telescope for
  all 168 declarations. Bare-cardinality idiom sweep: measured (see AC1). Same-file
  /-- <-> /-! consistency: no new header contradicts a declaration doc comment in its
  own file (two pre-existing /-- defects found and filed as Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011 rather than fixed,
  since fixing them would be a deletion/rename AC4 forbids in a pure-rewording wave).
  Instance-binder census: all 168 declarations take
  [∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet] (0 exceptions), all 74 files
  carry variable {V : Type*} [DecidableEq V], the single omit [DecidableEq V] site is
  disclosed in that file's own header. Mixed-layer scope: the 8 along-exhaustion-vs-Λ
  correlation files are split explicitly (0 misattributions, independently confirmed by
  dev-review). PR-body raw-HTML self-check: performed on this body before submission (no
  literal angle brackets, including inside inline code, per the wave 9 CI-trap lesson).
  Exclusivity claims enumeration: 5 (not 4 — corrected from the implementer's
  report): HighTemperatureBounds ("takes only the stage index n, the site set A,
  and the hypothesis Odd A.card"); ...Deviation ("under 0 ≤ β * J alone");
  ...DeviationFerro ("under 0 ≤ J and 0 < β alone"); ...RatioLogFeNonemptyZ ("the
  Prop-valued hypotheses are exactly 0 < β * J and 0 < |E|" — this disclosure is what
  exposed errata Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011); and the 5th, found independently by dev-review and missing from
  the implementer's original count, HighTemperatureBoundsExpansion ("This module
  states nothing of its own" — verified: 0 comment-aware declarations, imports exactly
  the two named modules, 18 modules import it). AC5 evidence filled inline above with
  real numbers throughout, never left [PENDING].

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. 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 (recurred again this wave, see the scope-table correction above and Errata: #4984's per-wave "charges" figure counts the ratchet's non-authoritative TELEMETRY rows (wave 10a frozen at 132; the charged population was 90) #5012).
• Wave 9: new-authoring risk calibration is not transferable; the zero/nonzero
  characterization defect class (closed form -> admissible domain -> root set -> sign, in
  that order); no negative provenance claims.
• Wave 10a (this PR): a fourth lesson-class, disclosure-forcing vs. prohibition
  constraints. The one genuinely new defect surfaced this wave (Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011, a verbatim-duplicate
  declaration with a misleading name) was not caught by either wave-9 prohibition sweep. It
  fell out of the exclusivity-disclosure discipline (forcing enumeration of the full
  hypothesis telescope), not out of a "do not say X" rule. See the calibration note below.

Calibration note (do not promote to a confirmed methodology finding yet)

This wave applied wave 9's zero/nonzero and negative-provenance lessons proactively and
closed at round 1 with zero code findings from both independent reviewers — the first wave
since wave 5 to do so. dev-review explicitly cautions this should not yet be promoted to a
confirmed campaign methodology finding ("generative pre-push constraints prevent defects
better than reactive review-round corrections"), for two compounding reasons specific to this
wave:

1. 0 MISSING_MODULE_DOC. This wave contains no new-authoring activity at all — every
   one of the 74 files already had a header to rewrite. Waves 8/9's defects were generated
   specifically while authoring prose for modules that had none; that defect-generating
   activity is simply absent here, not prevented.
2. Maximally homogeneous content. All 168/168 declarations share one instance binder
   pattern, all 74/74 files share one variable line, and nearly every statement is a thin
   pass-through to a Λ-level lemma — the easiest possible case for "restate the pinned
   statement, do not derive."

Because content difficulty moved in the easy direction between wave 9 and wave 10a, "fewer
defects" is confounded with "easier content," not isolated as an effect of the generative
constraints alone. The true test of whether generative constraints prevent defects is a
future wave that does include MISSING_MODULE_DOC (new-authoring) content; this
determination is explicitly deferred until re-tested on such a wave.

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 (~40/74 files read in full depth by dev-review, 27 by
Codex) and the machine coverage sweeps over all 74 (hypothesis disclosure, identifier
existence, instance binder, layer partition, AC4).

Also filed (not fixed in this wave, by design)

• Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011 — partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_pow_two_lt_of_nonempty
  is a verbatim duplicate of ..._pow_two_lt (identical binder telescope, identical
  conclusion, body forwards every argument); its _of_nonempty suffix names a hypothesis it
  does not take. Confirmed independently by dev-review. Pre-existing, a deletion AC4 forbids
  in this wave.
• Errata: #4984's per-wave "charges" figure counts the ratchet's non-authoritative TELEMETRY rows (wave 10a frozen at 132; the charged population was 90) #5012 — the freeze-figure telemetry/charged conflation described above, filed to fix
  the freeze procedure rather than re-correcting the arithmetic by hand every wave.

Deliberate non-actions

• The 44 zero-charge in-family siblings under SpecialCases/ — outside the freeze.
• 18 surviving GJ §18.x mislabel markers in this family's /-- declaration doc comments
  (162 total occurrences across 115 lines existed on these 74 files before this wave; all
  header-side (/-!) occurrences are gone; the 18 remaining are all inside /-- declaration
  doc comments, outside this campaign's /-! scope — they belong to 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 ledger, not
  touched here).
• Errata Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011's duplicate declaration — a deletion, which AC4 forbids in this wave.
• Section markers /-! ### ... -/ inside module bodies were removed (matching wave 9):
  every one was written in the retired "along-ex wraps" inventory vocabulary, so leaving them
  would have left each file internally inconsistent with its own new header.