F_eq_gap
The theorem confirms that the anchor display function F(Z) equals the gap function from RSBridge. Researchers modeling fermion masses on the phi-ladder or substituting closed-form residues at the anchor scale would cite this identity to interchange notations without further justification. The proof is a one-line reflexivity that follows immediately from the alias definition of F.
claim$F(Z) = g(Z)$ where $F(Z) = g(Z) = {ln(1 + Z/φ)} / {ln φ}$ and $g$ denotes the closed-form residue function at the anchor scale μ⋆.
background
The module supplies a Lean surface for single-anchor RG policy in the mass framework, wiring Constants.phi to the RSBridge infrastructure so that downstream lemmas can reference a clean predicate for stationarity at μ⋆ = 182.201 GeV. F is introduced as the display function F(Z) := gap Z, where gap is the noncomputable definition gap(Z) = ln(1 + Z/φ) / ln(φ) that represents the integrated mass anomalous dimension residue f_i(μ⋆). Upstream results include the gap definition in RSBridge.Anchor, whose doc-comment states that this closed form is claimed to equal the RG integral at the anchor, and the Z map in Masses.Anchor that supplies the integer input for each sector.
proof idea
The proof is a one-line wrapper that applies reflexivity on the definition of F as gap Z.
why it matters in Recognition Science
This identity makes the phenomenological claim f_i(μ⋆) = gap(ZOf i) auditable inside the Recognition framework, supporting the single-anchor phenomenology that links to the phi-ladder mass formula and the eight-tick octave structure. It fills the interface role described in the module doc-comment for connecting RGTransport hypotheses to the closed-form expression without embedding the full integral computation.
scope and limits
- Does not compute numerical values of F(Z) for concrete Z.
- Does not prove equality between the RG integral and the closed form.
- Does not address radiative stability bounds or flavor compatibility.
- Does not implement QCD or QED anomalous-dimension kernels.
formal statement (Lean)
62theorem F_eq_gap (Z : ℤ) : F Z = gap Z := rfl
proof body
Term-mode proof.
63
64/-! ## Anchor Specification -/
65
66/-- Universal anchor scale and equal‑weight condition.
67 This abstracts "PMS/BLM mass‑free stationarity + motif equal weights at μ⋆"
68 into a single predicate that downstream lemmas can reference.
69
70 From Source-Super: μ⋆ = 182.201 GeV, λ = ln φ, κ = φ. -/