The Pearl and the Toll: a Witnessed-Scale Chowla Regime and the Width Law of the Entropy Decrement

Every theorem in this paper is verified by the Lean 4 kernel over mathlib, with axiom base exactly {propext, Classical.choice, Quot.sound}; nothing rests on informal argument. The mathematics — the designs, the proofs, and their formalization — is joint work of the author and Claude (Anthropic's Fable 5 and Opus models), carried out under the author's direction and ratification; the commit ledger records the collaboration line by line. We prove two theorems about the entropy-decrement route to the logarithmically averaged two-point Chowla statement. The first, the toll, is unconditional: along the flat tower of scales H_{j+1} = H_j ⌊2A log H_j⌋ at design constant A ≥ 1, the telescoped entropy decrement equals a potential difference to within 5%, and consequently a tower long enough to exhaust the one-bit entropy budget log 2 must multiply the doubly-logarithmic width log 2A + log log H by a factor in the bracket [4^{(20/21)A}, (21/20) 4^A] — exponent pinned within 4.8%, constant within 5%, with the continuum value 4^A inside. Crossing the entropy budget is thus a conservation law rather than an optimization: the price is fixed, and a design chooses only the coordinate in which to pay it. The second theorem, the pearl, is conditional and we name its conditionality at the statement: at every design constant A above an explicit floor there is a Chowla regime whose window base is pinned at ⌈e^{e^{3.2A}}⌉, and for that regime the logarithmically averaged two-point Chowla correlation does not fail at the witnessed scale, on a list of hypotheses given in full in the paper: one analytic constant of the band lane, eight numeric riders on constants the theorem itself produces, and two carried predicates. Of that list, one rider was found unreachable along the proof and one predicate false at the regime the theorem itself produces — the second refuted by the first theorem's own lower bound — and both were repaired at the level of the statement, which is the episode the paper is written around. A chain of six corollaries then removes, in order, the two Siegel-genre riders by the classical limit, the band-lane constant by its own window, three numerals at their leaves, the base-scale cap at a raised lever, the outer-scale ceiling by threading, and the co-factor supply by repairing its register; the last of them has no outer hypothesis and no conclusion-side predicate, and of its five surviving hypotheses three are met by objects the development exhibits and two are the Siegel obstruction. Making the classical limit available required a quantifier hoist that the formal statement, and only the formal statement, made visible. The Lean sources for every declaration cited are archived at Zenodo, DOI 10.5281/zenodo.21828638 (a curated, self-contained snapshot; Lean 4 v4.32.0-rc1, mathlib at the same tag; builds with `lake exe cache get; lake build`).