178 -- Follows from the smoothness of RG flow in the vicinity of the anchor. 179 -- REDUCTION: Perturbative unitarity ensures derivatives of anomalous dimensions are bounded. 180 intro A _hA hA_eq 181 -- The second derivative is bounded by 1 at muStar by hypothesis. 182 -- Since A.muStar = muStar, the bound transfers directly. 183 use 1 184 constructor 185 · norm_num 186 · intro f 187 rw [hA_eq] 188 exact h_bounded f 189 190/-- **DISPLAY IDENTITY THEOREM** 191 192 At μ⋆, the RG residue equals F(Z) = gap(Z). 193 194 **Proof Structure**: 195 1. The Display Function $F(Z) = \log_\phi (1 + Z/\phi)$ represents the geometric cost of a ledger state. 196 2. The Single Anchor Policy posits a one-to-one mapping between geometric charges $Z$ and residues $f$. 197 3. Specifically, the integrated anomalous dimension from $\mu_{\star}$ to the physical mass scale 198 is forced by RS to match the geometric gap $F(Z)$. 199 4. This matches the `RGTransport.anchorClaimHolds` predicate. 200 201 **STATUS**: HYPOTHESIS (RS-SM bridge) -/
depends on (39)
Lean names referenced from this declaration's body.