pith. machine review for the scientific record. sign in
def definition def or abbrev high

gap

show as:
view Lean formalization →

The gap definition computes the logarithmic offset for a given sector and particle name by resolving the name to charge via chargeMap, applying the sector-specific Z integer map, and evaluating log(1 + Z/phi)/log(phi). Mass modelers in the Recognition Science framework cite it when placing fermions on the phi-ladder for predictions. The definition is a direct functional composition of chargeMap, Anchor.Z, and the closed-form gap expression.

claimFor sector $s$ and name $n$, define $gap(s,n) := (ln(1 + Z(s,Q(n))/phi))/ln(phi)$, where $Q(n)$ is the rational charge from the charge map and $Z(s,q)$ is the integer function that returns $q_6^2 + q_6^4$ for leptons and $4 + q_6^2 + q_6^4$ for quarks (with $q_6 = 6q$).

background

In the AnchorPolicy module the gap function supplies a name-based interface to the gap computation. chargeMap translates strings such as 'e' or 'u' into the corresponding rational charges. Anchor.Sector is the inductive type with constructors Lepton, UpQuark, DownQuark, Electroweak; each sector determines its own Z formula from the scaled charge. The upstream RSBridge.Anchor.gap records the closed form $gap(Z) = ln(1 + Z/phi)/ln(phi)$, which this policy instantiates after resolving name to charge to Z.

proof idea

The definition binds Q to chargeMap name and substitutes directly into the logarithmic expression using Anchor.Z sector Q. It is a one-line functional composition with no lemmas or tactics beyond the referenced definitions of chargeMap and Z.

why it matters in Recognition Science

This definition supplies the concrete gap values consumed by downstream certificates such as Jphi_numerical_band and visualBeautyCert in Aesthetics.VisualBeauty as well as adjacencyGap_eq and potterySerialCert in Archaeology.PotterySerialFromJCost. It implements the interface between the abstract anchor relation and the mass formula yardstick * phi^(rung - 8 + gap), thereby realizing the phi-ladder placement required by the T5 J-uniqueness and T6 self-similar fixed point. It touches the open alignment between the Gap45 derivation and observed particle spectra.

scope and limits

formal statement (Lean)

  24noncomputable def gap (sector : Anchor.Sector) (name : String) : ℝ :=

proof body

Definition body.

  25  let Q := chargeMap name
  26  (Real.log (1 + ((ChargeIndex.Z sector Q : ℝ) / Constants.phi))) / Real.log Constants.phi
  27

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.