pith. sign in
module module high

IndisputableMonolith.RSBridge.GapFunctionForcing

show as:
view Lean formalization →

The GapFunctionForcing module introduces the affine-log family as candidate forms for the gap function on the reals and derives the parameter constraints that force its canonical shape. Mass-spectrum modelers in the Recognition framework would cite the three-point closure result to justify the explicit gap expression. The argument consists of a chain of algebraic identities on the golden ratio together with normalization conditions at zero and unit steps.

claimThe affine-log candidate family comprises functions $f(r) = a + b log r$ on $r > 0$, with coefficients $a, b$ fixed by the relations $phi = 1 + phi^{-1}$, zero normalization, unit-step scaling, and three-point closure so that $f$ coincides with $ln(1 + Z/phi)/ln(phi)$.

background

The module sits inside the RSBridge layer that converts the recognition framework into Standard Model quantities. It imports the time quantum $tau_0 = 1$ tick from Constants and the core objects from Anchor: the 12 fermions, the charge-derived index $Z_i = qtilde^2 + qtilde^4$ (+4 for quarks), the gap display function $F(Z) = ln(1 + Z/phi)/ln(phi)$, and the anchor-scale mass. The local setting is therefore the real-line extension of this gap function, treated as an affine-log family whose parameters must be forced by phi self-similarity.

proof idea

The module first records the elementary phi identities, then applies zero normalization to fix the additive offset, unit-step scaling to fix the multiplicative coefficient, and the minus-one step to enforce the phi shift. These steps collapse the general affine-log form onto the canonical gap expression; the final three-point closure lemma assembles the constraints into a unique solution on the reals.

why it matters in Recognition Science

The module supplies the explicit justification for the gap function that appears in massAtAnchor and therefore underpins all subsequent fermion-mass calculations. It realizes the forcing step that converts the abstract phi-ladder (T6) into a concrete display function on integer Z values. No downstream theorems are yet recorded, so the module functions as a self-contained bridge lemma.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)