pith. machine review for the scientific record. sign in
def definition def or abbrev high

gap

show as:
view Lean formalization →

Gap supplies the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) that the integrated renormalization-group residue is claimed to match at the anchor scale for each fermion species. Mass-hierarchy modelers cite this when placing Standard Model fermions on the phi-ladder via the ZOf charge index. The implementation is a direct one-line transcription of the logarithmic ratio using the phi constant from the Constants bundle.

claim$F(Z) = (1/2) ln(1 + Z/φ) / ln(φ) for integer charge index Z, where φ is the golden ratio constant from the Constants bundle and Z is obtained from the ZOf map on fermions.

background

The RSBridge.Anchor module bridges recognition forcing to particle physics by defining the 12 Standard Model fermions, the ZOf charge index, and the gap display function. ZOf assigns to each fermion an integer Z = q̃² + q̃⁴ (plus 4 for quarks) from its tildeQ charge. Gap then gives the explicit closed form claimed to equal the integrated RG residue f_i(μ⋆) at the anchor scale, per the module statement: (1/ln φ) ∫ γ_i(μ) d(ln μ) ≈ gap(ZOf i) with tolerance ~1e-6.

proof idea

This is a one-line definition that directly transcribes the logarithmic ratio using Real.log applied to (1 + Z/φ) divided by Real.log of the phi constant imported from Constants. No lemmas or tactics are applied beyond the primitive real-arithmetic operations.

why it matters in Recognition Science

Gap completes the anchor identification required by Single Anchor Phenomenology in the RSBridge module and supplies the explicit residue for the phi-ladder mass formula. It is invoked downstream in visualBeautyCert, Jphi_numerical_band, and potterySerialCert for band and positivity checks. It operationalizes the T5 J-uniqueness and T6 phi fixed point by furnishing the concrete rung offset in the mass expression yardstick * φ^(rung - 8 + gap(Z)).

scope and limits

formal statement (Lean)

  73noncomputable def gap (Z : ℤ) : ℝ :=

proof body

Definition body.

  74  (Real.log (1 + (Z : ℝ) / (Constants.phi))) / (Real.log (Constants.phi))
  75
  76notation "𝓕(" Z ")" => gap Z
  77
  78/-- The residue at the anchor for a fermion species.
  79
  80    This is the **definitional** (closed-form) residue: `F(Z_i) = gap(ZOf f)`.
  81
  82    **Relation to the axiom `f_residue`**: The physics claim (stated as an axiom in
  83    `AnchorPolicy.lean`) is that the RG-transport residue equals this value:
  84      `f_residue f μ⋆ = residueAtAnchor f`
  85    This is verified numerically by external tools. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (24)

Lean names referenced from this declaration's body.