gap
plain-language theorem explainer
This definition computes the gap for a sector and particle name by first mapping the name to charge Q then evaluating the logarithmic display function on the integer Z from the anchor map. Mass ladder calculations and serial predictions in archaeology cite it to fix the exponent offset on the phi-ladder. The body is a direct term that composes chargeMap with the Z function and the closed-form ratio of logs.
Claim. For sector $s$ and name $n$, define $gap(s,n) := (Real.log(1 + (Z(s,Q(n)) : ℝ)/φ)) / Real.log φ$, where $Q(n)$ is the rational charge from the charge map and $Z(s,q)$ is the integer anchor function.
background
The AnchorPolicy module supplies policy functions that select anchors for mass predictions on the phi-ladder. Sector is the inductive type with cases Lepton, UpQuark, DownQuark, Electroweak. The Z function computes an integer from sector and rational charge Q via Q6 = 6*Q, then applies sector-specific powers: for Lepton it is Q6 squared plus Q6 to the fourth, with additive offsets for the quark sectors.
proof idea
The definition is a direct term. It lets Q be chargeMap name, then returns the ratio of Real.log on (1 + (Z sector Q cast to ℝ) over Constants.phi) divided by Real.log of Constants.phi. It applies the Z definition from Anchor and the gap expression from RSBridge.Anchor.
why it matters
This definition supplies the gap offset used by the mass formula yardstick * phi^(rung - 8 + gap(Z)). It feeds visualBeautyCert for the Jphi numerical band and potterySerialCert for adjacency gap positivity in archaeology. The expression realizes the closed-form residue at the anchor scale from RSBridge.Anchor, supporting the phi-ladder and T7 eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.