Pith. sign in
module module moderate

IndisputableMonolith.Masses.ZMapForcing

show as:
view Lean formalization →

Forces the canonical charge-to-band Z-map tuple from recognition topology and anchor outputs, with k=6 the smallest positive even integerization scale for SM charges. Mass-sector work cites it to pin gap(Z) in the phi-ladder formula without free coefficients. The argument equates ordered-minimizer uniqueness (unit coeffs) with the first-principles tuple from the 3-cube boundary derivation.

claimThe smallest positive even integerization scale for Standard Model charges is $k=6$. The canonical Z-map tuple is uniquely forced by first-principles recognition topology (charge-to-band map from 3-cube boundaries) together with anchor charge-map values; it is the unique complete ordered budget minimizer and carries unit coefficients.

background

Recognition Science places masses on a $\varphi$-ladder: yardstick times $\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. The gap term is read from a charge-to-band map $Z$ on integerized charges $\tilde Q$. Integerization needs a positive even scale $k$ so that SM charges land on a discrete lattice compatible with the eight-tick / 3-cube structure (T7–T8).

Upstream, Anchor centralises parameter-free mass constants in the Model layer and does not claim experimental agreement. ZMapTopologicalDerivation derives the polynomial $Z(\tilde Q)$ from structural properties of recognition boundaries on the 3-cube, without anchor constraints or empirical masses.

This module sits between those layers: it fixes which discrete scale and coefficient tuple are the unique first-principles choice once anchor outputs and ordered-minimizer constraints are imposed.

proof idea

Not a single theorem; a forcing chain of lemmas. First identify $k=6$ as the smallest positive even integerization scale for SM charges, and record the canonical color offset and anchor charge-map values. Next show that any complete ordered minimum-budget solution is forced to unit coefficients (two parallel statements: min-budget and minimizer forms). Then prove the canonical tuple is forced from anchor outputs and, separately, from first principles; establish that the first-principles Z-map tuple satisfies those principles; and close with an iff equating the canonical tuple to the first-principles tuple.

why it matters in Recognition Science

Supplies the discrete Z-map choice consumed by QuarkForwardPipeline, the unified forward-prediction path for all six quark masses under Convention A: sector yardsticks from cube geometry, integer rungs from generation torsion, and $\mathrm{gap}(Z)$ from the charge-band map, with no PDG targeting. Without a forced canonical tuple, gap(Z) would remain a free discrete parameter. The module therefore closes the charge-band step of the mass formula between topological derivation of $Z$ and numerical quark forward prediction, keeping the Model-layer constants parameter-free at that interface.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)