module module high

`IndisputableMonolith.RSBridge.ResidueData`

ResidueData module encodes the theoretical gaps for leptons at Z=1332, up quarks at Z=276 and down quarks at Z=24 using the F function. It includes certification data for the electron, muon, tau, up, charm and top. Researchers applying the Recognition Science mass formula to Standard Model fermions cite these gap values. The module is purely declarative, importing anchor and policy modules to organize the residue data.

claimThe module declares the lepton gap $F(1332) = \frac{\ln(1 + 1332/\phi)}{\ln\phi} ≈ 13.954$, the up gap $F(276)$, the down gap $F(24)$, and particle certifications for $e, \mu, \tau, u, c, t$.

background

The RSBridge.ResidueData module operates within the single-anchor phenomenology defined in AnchorPolicy. It relies on the core definitions from RSBridge.Anchor: the Fermion type for the twelve Standard Model particles, the ZOf map giving charge-indexed integers, and the gap function F(Z) = ln(1 + Z/φ)/ln(φ).

The module supplies species-specific residue data by instantiating gap theories for leptons (Z=1332), up-type (Z=276) and down-type (Z=24) quarks. These Z values arise from the charge formula Z_i = q̃² + q̃⁴ with an additive offset for quarks.

AnchorPolicy isolates assumptions about the anchor scale μ⋆ and radiative stability so that the gap data can be used cleanly in mass calculations.

proof idea

This is a definition module, no proofs. It organizes its content into separate declarations for each gap theory and certification constant, drawing the F function and Z map directly from the imported Anchor module.

why it matters in Recognition Science

This module supplies the fermion-specific gap data required by the massAtAnchor construction in the Anchor module. It fills the concrete rung assignments on the phi-ladder for the lepton and quark sectors. The data supports the eight-tick octave and D=3 framework by fixing the gap(Z) term in the mass formula.

scope and limits

Does not derive the Z values from the J-uniqueness or RCL.
Does not include neutrino residue data.
Does not perform numerical integration or renormalization group flow.
Does not claim dynamical stability beyond the policy hypotheses.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.AnchorPolicy module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (22)

def gap_lepton_theory L37
def gap_up_theory L41
def gap_down_theory L45
theorem lepton_Z_is_1332 L49
theorem up_Z_is_276 L50
theorem down_Z_is_24 L51
def cert_e L62
def cert_mu L69
def cert_tau L76
def cert_u L88
def cert_c L95
def cert_t L104
def cert_d L111
def cert_s L118
def cert_b L125
structure StabilityCert L136
def canonicalAnchorSpec L144
theorem display_identity_uses_gap L151
def certificateWithinTolerance L158
def leptonCerts L166
def quarkCerts L169
def allCerts L172