display_identity_at_anchor_hypothesis
plain-language theorem explainer
Recognition Science sets the RG residue of a fermion equal to the display function at its Z value. This hypothesis supports derivations of mass ratios at the anchor as pure powers of phi. The declaration introduces it directly as the proposition that the residue equals the display function evaluated at the fermion Z for every fermion and scale.
Claim. Let $f_ {residue} : Fermion to mathbb{R} to mathbb{R}$. The hypothesis asserts that $f_{residue}(f, mu) = F(Z(f))$ for all fermions $f$ and scales $mu$, where $F(Z) = log(1 + Z/phi)/log(phi)$ is the display function.
background
The module supplies a Lean interface for single-anchor phenomenology in the mass framework. It reuses the gap function from RSBridge as the display F(Z), given by log(1 + Z/phi) over log(phi). The hypothesis isolates the claim that the integrated RG residue equals this display at the fermion Z value.
proof idea
The declaration is a definition that introduces the hypothesis as a Prop. The body equates the residue function for any fermion at any scale to the display function evaluated at the fermion Z value. No lemmas or tactics are applied.
why it matters
This hypothesis is required by family_ratio_from_display to show that mass ratios at the anchor reduce to phi raised to the difference in rungs for equal-Z fermions. It likewise supports the muon-electron ratio theorem. The declaration closes the interface for the single-anchor assumption in the Recognition Science mass framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.