SelfSimilarDressing
plain-language theorem explainer
A self-similar dressing is a survival-fraction map under gap load constrained only by multiplicative factorization on independent nonnegative loads, antitonicity on the nonnegative ray, and the fixed-point balance g(1)=1/(1+g(1)). It is the input type for M5 calibration forcing: no unit-linear-response or derivative normalization is present. Downstream theorems force g=φ^{-t} and recover the forward α object from every such dressing. The declaration is a pure structure; existence is witnessed later by the forced continuum weight.
Claim. A self-similar dressing is a real map $g:\mathbb{R}\to\mathbb{R}$ such that (i) $g(a+b)=g(a)g(b)$ whenever $a,b\ge 0$ (factorization over independent nonnegative loads), (ii) $g$ is antitone on $[0,\infty)$ (more load never raises survival), and (iii) $g(1)=1/(1+g(1))$ (self-similar single-step balance).
background
Module M5 (Calibration Forcing) eliminates the unit-linear-response axiom (D2) that earlier dressing responses carried. The residual worry was that α genesis still hid a normalization choice. The cure is to package only ledger-native premises.
Factorizes g (from MeasureForcing) means $g(a+b)=g(a)g(b)$ for nonnegative $a,b$: independent gap loads multiply survival fractions. Antitonicity on $[0,\infty)$ says more load never helps. The third field is the same fixed-point equation (W2) that forces the T9 recognition-measure step: $g(1)=1/(1+g(1))$. No derivative condition and no CODATA scale appear.
Spatial dimension $D=3$ (T8/T9) sits upstream in the α pipeline but is not a field of this structure; the structure only records the response under gap load.
proof idea
No proof body: this is a structure definition. It bundles three Prop fields on a map $g:\mathbb{R}\to\mathbb{R}$. Downstream lemmas (e.g. step_eq_sq, step_forced, response_forced) discharge consequences from those fields; non-vacuity is the separate canonical construction that installs the forced continuum weight as an instance.
why it matters
This is the M5 carrier that discharges the residual calibration worry for α genesis. Module doc: form, rate, and step of the dressing are forced by the same two structural facts (factorization and self-similar balance) that force the recognition measure itself.
Parents: alphaInvGenesis_from_selfSimilar obtains the forward α object from every instance via $α^{-1}_{\mathrm{genesis}}=S\cdot g(w_8/S)$; natural_display shows every M1 calibrated (D1)+(D2) response is this object read in natural log-φ units; CalibrationForcingCert bundles step $g(1)=φ^{-1}$, full forcing $g=φ^{-t}$, natural-units display, and α recovery; canonical witnesses non-vacuity with the forced continuum weight.
Landmark link: the balance field is the W2 equation of the T9 measure step, so the dressing inherits the φ-ladder rate without a separate calibration input. Status target: theorem file, zero sorry, no CODATA.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.