display_identity_uses_gap
plain-language theorem explainer
The theorem states that for any fermion the residue function F applied to its Z-value equals the gap function at the same Z-value. Researchers auditing fermion mass residues against Recognition Science predictions cite it to confirm definitional consistency at the anchor scale. The proof is a one-line reflexivity establishing the equality by definition from the AnchorPolicy setup.
Claim. For any fermion $f$, $F(Z(f)) = g(Z(f))$, where $Z(f)$ is the integer rung of the fermion, $F$ is the display residue function, and $g$ is the gap given by the product of closure and Fibonacci factors.
background
The module supplies residue certificates as numerical audit data for experimental fermion masses transported to the anchor scale. These bounds are constructed to verify the axiom display_identity_at_anchor from AnchorPolicy, which equates the residue to both $F(Z)$ and $g(Z)$ at the canonical point. Upstream, Gap45.Derivation defines $g$ as the product of closure_factor and fibonacci_factor with the main theorem that this product equals 45; PhiForcingDerived supplies the J-cost structure $J(x) = (x + x^{-1})/2 - 1$ whose convexity underpins the phi-ladder used to assign rungs.
proof idea
The proof is a one-line reflexivity that unfolds the definitions of $F$ and $g$ from AnchorPolicy, confirming they coincide on $Z(f)$ without invoking further lemmas.
why it matters
The result anchors the residue certificates (cert_e, cert_mu, cert_tau, cert_u, cert_c, cert_t) to the display_identity_at_anchor axiom. It closes the link between the audit payload and the theoretical gap derived in Gap45, ensuring consistency with the phi-ladder mass formula and the eight-tick octave structure. The declaration touches the open tension between integer-rung predictions and observed quark residues, particularly the charm anomaly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.