CalibrationForcingCert
plain-language theorem explainer
Certificate packaging the M5 closure of alpha genesis: calibration is not an input. It asserts four forced facts: the dressing step equals φ⁻¹ from balance alone; every self-similar dressing is the forced continuous measure on loads; the M1 calibrated response is only the natural-units display of that object; and the forward α⁻¹ seed follows from every such dressing. Cite when closing the fine-structure derivation without CODATA. The inhabiting proof is a four-way conjunction of existing forcing lemmas.
Claim. A calibration-forcing certificate is verified when all four hold: (1) every self-similar dressing $D$ satisfies $D.g(1)=\varphi^{-1}$; (2) for every such $D$ and every $t\ge 0$, $D.g(t)$ equals the forced continuous weight $\varphi^{-t}$; (3) every M1 dressing response $R$ and self-similar dressing $D$ obey $R.g((\ln\varphi)\,t)=D.g(t)$ for $t\ge 0$; (4) for every self-similar $D$, the forward inverse-fine-structure object equals channel budget times $D.g$ at spectral load. Any certificate is verified.
background
Alpha Genesis M5 eliminates the unit-linear-response calibration (D2) that M1 still carried. A self-similar dressing is a survival fraction $g$ on gap load with three premises only: factorization over independent nonnegative loads (ledger inheritance), antitonicity (more load never helps survival), and the self-similar balance $g(1)=1/(1+g(1))$ on the single step — the same balance that forces the T9 measure step. No normalization field is present.
From those premises alone one obtains $g(t)=\varphi^{-t}$ on all $t\ge 0$, with step $g(1)=\varphi^{-1}$ derived rather than fitted: positivity of the step follows from factorization ($g(1)=g(1/2)^2>0$), and the balance equation then has a unique admissible root. The continuous forced weight is the object already named in MeasureForcing (contWeight).
Upstream, step_forced and response_forced establish the step and the full measure identity; natural_display identifies every differentiable M1 DressingResponse as the same object read in natural log units; alphaInvGenesis_from_selfSimilar recovers the forward $\alpha$ seed as channel budget times the dressing at spectral load. Spatial dimension $D=3$ is the T8/T9 constant used elsewhere in the alpha ladder, not an input here.
proof idea
The structure is empty (deriving Inhabited); content lives in the verified predicate, a four-conjunct Prop. The companion theorem verified_any proves every certificate satisfies it by refine ⟨?_, ?_, ?_, ?_⟩ and discharging each goal with one existing lemma:
D.step_forced— step equals $\varphi^{-1}$;D.response_forced t ht— self-similar dressing equalscontWeighton $t\ge 0$;SelfSimilarDressing.natural_display R D t ht— M1 response is the natural-units display;SelfSimilarDressing.alphaInvGenesis_from_selfSimilar D— forward $\alpha^{-1}$ object from every self-similar dressing.
No new algebra; pure packaging of the M5 forcing chain.
why it matters
This is the M5 closure certificate for Alpha Genesis: it records that the dressing of the $\alpha$ seed carries zero calibration input. Form, rate, and step are forced by the same two structural facts (factorization and self-similar balance) that force the recognition measure itself (T5–T9 lineage, eight-tick / $D=3$ setting upstream).
Downstream use is currently empty in the graph, so the certificate is a terminal audit object: a single verified flag that the residual normalization worry is discharged and that no CODATA constant enters the file. It sits at the end of the CalibrationForcing module after step_forced, response_forced, natural_display, and alphaInvGenesis_from_selfSimilar, and is the natural place a parent alpha-band or constants-assembly theorem would cite when claiming the inverse-fine-structure construction is calibration-free. Status target is theorem with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.