pith. sign in
module module moderate

IndisputableMonolith.RSBridge.GapFunctionForcing

show as:
view Lean formalization →

The module develops affine-log families on the reals as candidate forms for the gap function in the RS bridge to particle physics. Researchers deriving Z-to-mass mappings or fermion spectra would reference its forcing lemmas. The argument consists of sequential algebraic lemmas that impose normalization, step, and three-point conditions to collapse the family onto the canonical gap.

claimAn affine-log gap candidate takes the form $F(Z) = a \log(b + c Z)$ on the reals, with parameters $a, b, c$ fixed by zero normalization, unit-step scaling, and three-point closure to recover the canonical $F(Z) = \ln(1 + Z/\phi)/\ln\phi$.

background

The module sits inside the RSBridge domain and imports the time quantum $\tau_0 = 1$ tick from Constants together with the core bridge objects from Anchor. Anchor defines the 12 Standard Model fermions, the charge-indexed integer $Z_i = \tilde{q}^2 + \tilde{q}^4$ (+4 for quarks), the display function $F(Z) = \ln(1 + Z/\phi)/\ln\phi$, and the anchor-scale mass map. The present module examines the larger affine-log family that contains this canonical gap.

Sibling declarations introduce gapAffineLogR and gapAffineLog, then prove a chain of forcing statements (zero_normalization_forces_offset, unit_step_forces_log_scale, minus_one_step_forces_phi_shift, affine_log_parameters_forced, affine_log_collapses_to_gap) that terminate in three_point_forces_canonical_gap and the ThreePointClosure theorem.

proof idea

The module is organized as a sequence of lemmas rather than a single theorem. Each lemma applies an algebraic identity or normalization condition imported from Anchor and Constants: zero normalization fixes the offset, the unit step forces logarithmic scaling, the minus-one step forces the $\phi$ shift, and the three-point condition collapses the remaining parameters. The final ThreePointClosure packages these steps into a single statement that the canonical gap is the unique affine-log function satisfying the listed conditions.

why it matters in Recognition Science

The module supplies the explicit forcing argument that selects the canonical gap function used by massAtAnchor and the Z-map in Anchor. It therefore occupies the step that converts the abstract recognition composition law into a concrete functional form for fermion masses. Although no downstream declarations are yet recorded, the module directly supports any later theorem that invokes the gap function inside the RS forcing chain (T5–T8).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)