display_identity_at_anchor
plain-language theorem explainer
The display identity theorem states that if the fermion residue function equals the geometric display F at every scale, then the equality holds at the anchor scale muStar for any AnchorSpec with equal weights. Mass-spectrum calculations in the Recognition Science framework cite this to substitute F(Z) directly into RG equations at the PMS scale. The proof is a one-line specialization of the universal hypothesis to the anchor point.
Claim. If $f(f,μ)=F(Z(f))$ holds for every fermion $f$ and scale $μ$, then for every anchor specification $A$ with equal weights, $f(f,A.μ_⋆)=F(Z(f))$ for every fermion $f$, where $F(Z)=log_φ(1+Z/φ)$ is the display function.
background
AnchorPolicy implements the Single-Anchor RG Policy. It aliases the display function as F(Z) := gap(Z) = log(1 + Z/φ)/log(φ) from RSBridge. AnchorSpec bundles the anchor scale muStar (set to 182.201 GeV), lambda = ln φ, kappa = φ, and the equalWeight predicate encoding unit motif weights at muStar. The module states the integrated residue as the hypothesis f_i(μ⋆) = (1/ln φ) ∫_{ln μ⋆}^{ln m_phys} γ_i d(ln μ), with the claim that this equals F(Z_i). Upstream, RGTransport supplies the residue integral definition while IntegrationGap.A fixes the active edge count per fundamental tick.
proof idea
One-line wrapper. After introducing the anchor A and fermion f, the proof applies the hypothesis h_exact directly at A.muStar, discarding the unused equalWeight predicate.
why it matters
The theorem supplies the RS-SM bridge for the display identity, feeding residueAtAnchor in RGTransport and canonicalAnchorSpec in ResidueData. It supports downstream results such as gap_down_pos in QuarkSchemeReconciliation. In the framework it instantiates the Single Anchor Policy at the phi-ladder step, where geometric charges Z map to residues via F(Z). It touches the open question of whether the identity survives explicit higher-order QCD kernels beyond the phenomenological hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.