pith. sign in
module module high

IndisputableMonolith.RSBridge.ResidueData

show as:
view Lean formalization →

ResidueData supplies gap theories and certification constants for Standard Model fermions via the F(Z) residue function. Mass-spectrum calculations in the Recognition framework cite these values to fix rung positions on the phi-ladder. The module consists of separate theory lemmas for leptons (Z=1332), up quarks (Z=276), and down quarks (Z=24), each importing the Z-mapping and gap definition from the Anchor layer.

claimgap_lepton_theory asserts $F(1332) = 13.954$ where $F(Z) = ln(1 + Z/φ)/ln(φ)$; gap_up_theory and gap_down_theory give the corresponding values for Z=276 and Z=24; cert_e, cert_mu, cert_tau, cert_u, cert_c, cert_t are the associated certification constants at the anchor scale.

background

The module resides in the RSBridge layer and imports AnchorPolicy (single-anchor RG policy and stability scaffolding) together with Anchor (Fermion species, ZOf charge index, and gap function). Anchor defines $F(Z) = ln(1 + Z/φ)/ln(φ)$ with Z_i = q̃² + q̃⁴ (+4 for quarks) and massAtAnchor at scale μ⋆. AnchorPolicy isolates assumptions on anchor scale and flavor compatibility so that residue data can be audited cleanly. The supplied DOC_COMMENT records the lepton case F(1332) ≈ 13.954.

proof idea

This is a definition module, no proofs. It organizes sibling declarations gap_lepton_theory, gap_up_theory, gap_down_theory as direct applications of the gap function to the respective Z values, followed by certification constants cert_e through cert_t that bind the numerical residues to the anchor-scale mass formula.

why it matters in Recognition Science

ResidueData closes the numerical bridge from the abstract Z-mapping to concrete particle data required by the mass formula yardstick · φ^(rung-8 + gap(Z)). It feeds mass-spectrum constructions that rely on AnchorPolicy's single-anchor interface and supports the T5 J-uniqueness and phi-ladder steps of the forcing chain. No direct downstream theorems are listed yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)