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

IndisputableMonolith.RSBridge.GapFunctionForcing

show as:
view Lean formalization →

This module defines the affine-logarithmic candidate family for the gap function on the reals and derives the forcing conditions that select the canonical phi-based form. Researchers deriving fermion masses from the recognition ladder would cite the gapAffineLog construction when mapping Z indices to display scales. The module consists of auxiliary definitions followed by algebraic lemmas that close the three-point parameter system.

claimThe gap function family on the reals is given by the affine-log form $F(Z) = a + b^{-1} (1 + c Z)$ with the canonical instance $F(Z) = ln(1 + Z phi^{-1}) / ln phi$ forced by three-point closure.

background

The module operates inside the RSBridge layer that connects Recognition Science to Standard Model fermions. Upstream, the Anchor module supplies the gap display function F(Z) = ln(1 + Z/phi)/ln(phi) together with the ZOf charge index for each fermion species, while Constants fixes the base time quantum tau_0 = 1 tick. The present module explores affine-log candidates on the reals as candidate realizations of this display function.

proof idea

This is a definition module, no proofs. It introduces gapAffineLogR and gapAffineLog as the real-valued affine-log candidates, then supplies the supporting algebraic identities (phi_eq_one_add_inv_phi, log_one_add_inv_phi_eq_log_phi, zero_normalization_forces_offset, unit_step_forces_log_scale) that prepare the three-point closure argument.

why it matters in Recognition Science

The module supplies the explicit affine-log realization of the gap function used in massAtAnchor calculations. It feeds the fermion species and Z-map machinery in the Anchor module by showing that three-point conditions force the canonical phi form, thereby closing the parameter space for the phi-ladder mass formula.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)