pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.RSBridge.GapFunctionForcing

show as:
view Lean formalization →

The module defines an affine-log family of candidate gap functions on the reals and derives normalization conditions that force the parameters to match the canonical RS gap function. Researchers building mass ladders from the Z-map would cite the ThreePointClosure result. The structure consists of successive lemmas that fix the affine coefficients via the golden ratio identity and three-point interpolation.

claim$F(Z) = a · log(Z + b) + c$ on the reals, with parameters forced by the conditions $φ = 1 + φ^{-1}$, zero normalization, unit step scaling, and three-point closure to recover the canonical form $F(Z) = ln(1 + Z/φ)/ln(φ)$.

background

The module sits in the RSBridge domain and imports the base time quantum τ₀ = 1 tick from Constants together with the fermion Z-map and gap function from Anchor. Anchor supplies the core display function F(Z) = ln(1 + Z/φ)/ln(φ) and the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks). The module introduces the affine-log candidates gapAffineLogR and gapAffineLog as a parameterized family on the reals.

proof idea

The module first states the affine-log definitions gapAffineLogR and gapAffineLog. It then proves the golden-ratio identities phi_eq_one_add_inv_phi and log_one_add_inv_phi_eq_log_phi, followed by the normalization lemmas zero_normalization_forces_offset, unit_step_forces_log_scale, and minus_one_step_forces_phi_shift. These combine algebraically in affine_log_parameters_forced and affine_log_collapses_to_gap, closing with three_point_forces_canonical_gap and ThreePointClosure.

why it matters in Recognition Science

The module supplies the uniqueness argument for the gap function under affine-log assumptions, supporting the massAtAnchor construction in Anchor and the phi-ladder mass formula. It closes the three-point determination step that aligns with the self-similar fixed point for phi in the forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)