Pith. sign in
module module high

IndisputableMonolith.Masses.ZMapForcing

show as:
view Lean formalization →

Forces the Standard Model charge-to-band Z-map to a unique canonical integer tuple from first principles, with integerization scale k=6 as the smallest positive even scale compatible with SM charges. Mass and quark-pipeline authors cite it to replace anchor-fitted charge maps by a forced discrete object. The argument combines the topological Z-derivation on the 3-cube with anchor charge outputs and ordered min-budget uniqueness for unit coefficients.

claimThe charge-to-band map is forced to a unique canonical integer tuple $(z_u,z_d,z_s,\ldots)$ once SM charges are integerized at the smallest positive even scale $k=6$. That tuple is the unique complete ordered minimizer of the recognition budget with unit coefficients, and it coincides with the first-principles Z-map obtained from recognition topology on the 3-cube.

background

Recognition Science places quark and lepton masses on a $\varphi$-ladder: mass $\propto$ yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, where the gap is read from a charge-to-band polynomial $Z(\tilde Q)$. The topological derivation module builds $Z$ from recognition boundaries on the 3-cube without fitting masses. The Anchor module centralises the parameter-free mass constants in the Model layer and does not claim experimental agreement.

This module sits between those two sources. It integerizes SM charges at scale $k$ and isolates $k=6$ as the smallest positive even integerization scale. From the resulting anchor charge-map values it extracts a canonical color offset and a canonical tuple, then proves that complete ordered min-budget uniqueness forces the coefficients to be units. The same tuple is shown to be exactly the first-principles Z-map tuple, so anchor outputs and topology agree on one discrete object.

proof idea

The module is a short forcing chain, not a definition dump. It first records $k=6$ as smallest positive even integerization scale and the canonical color offset. Anchor charge-map values are then shown to determine a unique candidate tuple. Completeness and ordered min-budget hypotheses force all free coefficients to $\pm 1$ (unit coefficients). Separately, the topological first-principles Z-map tuple is named and proved to satisfy the same constraints. The two characterizations are glued by an iff: a tuple is the canonical one exactly when it is the first-principles Z-map tuple. Downstream code therefore imports a single forced object rather than a fitted polynomial.

why it matters in Recognition Science

Quark masses in RS need a charge-band gap with no PDG targeting. The downstream QuarkForwardPipeline implements one forward pipeline for all six quarks under Convention A: cube-geometry yardsticks, generation-torsion rungs, and $\mathrm{gap}(Z)$ from the charge-band map, with the explicit property of no PDG input. This module supplies the forced canonical Z-tuple that pipeline consumes, closing the gap between the topological Z-derivation and the anchor constants. In the broader chain it stabilizes the mass formula's $Z$-dependent rung correction so that sector predictions remain parameter-free once $\varphi$ and the eight-tick / $D=3$ geometry are fixed.

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)