module module moderate

`IndisputableMonolith.Verification.ZMapTopologicalDerivation`

Verification module proving that k=6 is the smallest positive even scale integerizing the three SM electric charges (as rationals). Mass-layer and Z-map authors cite it for the parity-constrained integerization closure. The argument defines the charge triple, checks small positive integers case-by-case, and identifies the winner with the cube's six faces.

claimLet $Q_{\mathrm{SM}}=\{Q_e,Q_u,Q_d\}\subset\mathbb{Q}$ be the three Standard Model electric charges. A positive integer $k$ integerizes them if $kQ\in\mathbb{Z}$ for every $Q\in Q_{\mathrm{SM}}$. Then $k=6$ is the smallest positive even integerizer, and $6$ equals the face count of the cube.

background

Recognition Science ties electromagnetic bookkeeping to the cubic ledger: spatial dimension $D=3$ (forcing step T8) gives a cube whose six faces supply a natural even combinatorial scale. The mass-layer Z-map needs a single positive even multiplier that clears denominators of the SM charge rationals so that rung arithmetic stays integral.

This module lives in Verification. It imports RS constants and the alpha-construction seed assembly (cubic-ledger combinatorics, $O(4\pi)$ recognition-scale content), but it does not re-derive $\alpha$. Its local objects are the charge triple as rationals, a predicate that a scale integerizes every charge, and comparison facts among small positive integers.

Downstream packaging treats the $k=6$ closure as an adopted parity-constrained fact for the mass layer.

proof idea

Definition block fixes the three SM charges as rationals and the integerization predicate. Separate lemmas show which small positive integers succeed or fail: $1,2,4,5$ fail; $3$ and $6$ succeed. A minimality lemma then states that $6$ is the smallest positive even integerizer. A parallel combinatorial lemma equates that scale to the cube face count. A summary bundle collects the case table and the minimality claim for import.

why it matters in Recognition Science

Feeds Masses.ZMapForcing, which "upstreams the partial O2/O3 closure into the canonical mass-layer namespace" and packages "$k=6$ is the smallest positive even scale that integerizes SM charges." That bridge is what lets mass-ladder and Z-map developments assume integral charge clearing under the parity constraint without re-proving the case analysis.

In the broader framework the result links T8 ($D=3$) and cubic-ledger geometry (six faces) to the charge sector used by the phi-ladder mass formula. It does not close the open infrared $\alpha^{-1}(0)$ boundary condition; it only supplies the integerization scale the mass layer adopts.

scope and limits

Does not derive the SM charge values from first principles; they are inputs as rationals.
Does not claim 6 is the unique integerizer; 3 also integerizes, but is odd.
Does not prove anything about continuous couplings or running alpha.
Does not discharge the open exact infrared alpha inverse boundary condition.
Does not treat non-SM or exotic fractional charges outside the fixed triple.

used by (1)

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

IndisputableMonolith.Masses.ZMapForcing module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (53)

def sm_charges L55
def integerizes_all L58
theorem six_integerizes L62
theorem one_fails L71
theorem two_fails L81
theorem three_integerizes L94
theorem four_fails L103
theorem five_fails L113
theorem face_count_eq_six L123
theorem integerization_results L126
theorem six_smallest_positive_even_integerizer L134
def Q_tilde_lepton L154
def Q_tilde_up L155
def Q_tilde_down L156
def Z_poly L160
def Z_quark_with_offset L163
theorem charge_conjugation_invariant L166
theorem neutral_vanishes L172
def Z_lepton L176
def Z_up L177
def Z_down L178
def Z_up_with_offset L181
def Z_down_with_offset L184
theorem bare_Z_values L187
theorem coefficients_forced_from_quark_bare_anchors L193
theorem full_anchor_tuple_forces_coefficients_and_offset L212
def families_separated L235
theorem canonical_separates L239
theorem quadratic_only_weak_hierarchy L249
theorem three_weak_hierarchy L256
theorem six_better_separation_than_three L261
def edge_direction_count L270
theorem edge_direction_eq_four L273
def Z_full L276
theorem full_Z_values L283
theorem matches_anchor_Z L292
structure ZMapDerivation L300
def derivation_complete L321
def ordered_hierarchy L335
theorem canonical_ordered L339
theorem quadratic_ordered L345
theorem quartic_only_separated L352
theorem minimal_nonzero_coefficients L359
theorem unique_minimal_complete L371
theorem one_one_achieves_minimum L377
theorem complete_ordered_min_budget_forces_unit_coeffs L382
def complete_ordered_minimizer L399
theorem one_one_is_complete_ordered_minimizer L404
theorem complete_ordered_minimizer_forces_unit_coeffs L412
theorem zmap_canonical_tuple_forced_from_first_principles L429
theorem zmap_canonical_tuple_satisfies_first_principles L451
def first_principles_zmap_tuple L462
theorem canonical_tuple_iff_first_principles L471