cross_sector_shift
The definition returns the integer 12 for the down-quark sector and zero otherwise, supplying the additive correction to the exponent in the phi-ladder mass formula that accounts for edge-layer traversal cost in the three-dimensional cube partition. Mass-prediction calculations in the Recognition Science framework reference this term when adjusting down-quark entries on the SDGT rung. It is realized by a direct case split on the sector that inserts the precomputed edge count from the cube geometry.
claimDefine the integer-valued shift function on sectors by $s(DownQuark)=12$ and $s(s)=0$ for every other sector $s$. The constant 12 equals the number of edges in the three-dimensional cube, $D=3$.
background
Sectors are the four labels Lepton, UpQuark, DownQuark and Electroweak. The mass formula in this module is yardstick times phi raised to the power (rung minus 8 plus gap of Z plus the shift). The auxiliary gap function takes a sector and particle name, extracts the charge via chargeMap, forms Z as the sum of quadratic and quartic terms in the scaled charge Q6, then converts the result to a real exponent via logarithms base phi. Upstream, cube_edges(d) is defined as d times 2 to the power (d minus 1), and the spectral-emergence constant E(D) is identical; both evaluate to 12 when D equals 3. The gap constant from the Gap45 derivation is the product of closure and Fibonacci factors and equals 45 by the main theorem of that module.
proof idea
The definition is realized by pattern matching on the sector argument. The DownQuark branch returns the literal 12, which is the value of cube_edges(3). Every other branch returns the literal 0. No further lemmas or tactics are invoked; the numeric constant is taken directly from the cube-edge count already established in the AlphaDerivation and SpectralEmergence modules.
why it matters in Recognition Science
The definition supplies the shift that appears inside predict_mass_sdgt, which computes the SDGT mass as yardstick times phi to the power (rung_sdgt minus 8 plus gap plus shift). It encodes the cross-sector correction required by the cube-partition geometry that underlies the Recognition Science mass ladder, where D equals 3 and the eight-tick octave fixes the phi spacing. Without the shift the down-quark predictions would omit the edge-layer cost assigned to the lepton sector in the partition.
scope and limits
- Does not compute any mass value, only the integer exponent correction.
- Does not apply to leptons, up quarks or electroweak entries.
- Does not incorporate charge values, particle names or the gap function.
- Does not alter the yardstick or the base rung calculation.
Lean usage
noncomputable def predict_mass_sdgt (sector : Anchor.Sector) (name : String) : ℝ := Anchor.yardstick sector * Constants.phi ^ (rung_sdgt sector name + gap sector name - 8 + cross_sector_shift sector)formal statement (Lean)
66noncomputable def cross_sector_shift (sector : Anchor.Sector) : ℤ :=
proof body
Definition body.
67 match sector with
68 | .DownQuark => 12 -- E = cube_edges(3) = 12
69 | _ => 0
70
71/-- SDGT mass prediction: m = A_s × φ^(r_sdgt - 8 + gap(Z) + shift). -/