Masses Zmap Forcing Zmap Canonical Tuple Forced From First Principles

The forced tuple

The declaration zmap_canonical_tuple_forced_from_first_principles is a theorem in the framework's machine-checked library of formal theorems. It states that if a tuple of four integers, written (k, a, b, c), meets five stated conditions, then that tuple must be exactly (6, 1, 1, 4). The conditions are: k is a positive even integer that makes all Standard Model charges integer-valued; k is the smallest such integer; the coefficients a and b form a complete ordered minimizer; and c equals the number of edge directions of a cube, which is 4. The theorem proves that no other tuple can satisfy all these constraints at once.

In plainer language, the theorem pins down a specific set of numbers that appear in the framework's model of particle masses. The number k = 6 is the smallest positive even scale that turns the fractional charges of quarks and leptons into whole numbers. The coefficients a = 1, b = 1, and c = 4 come from a separate argument about the structure of a polynomial family. The theorem's converse is also proved: the tuple (6, 1, 1, 4) does satisfy all the conditions, so the characterization is exact, not merely one-way.

In Recognition Science, this result is a step toward deriving particle properties from the framework's starting point, where reality keeps a discrete record of recognition events. The framework models the mass-layer charge map as a polynomial in the charge Q, with the form Z = aQ² + bQ⁴ for leptons and Z = c + aQ² + bQ⁴ for quarks. The theorem shows that if this polynomial family is constrained by topology and a minimal coefficient budget, the coefficients are forced to (1, 1, 4). The scale k = 6 is forced separately by the integerization condition.

What the theorem does not claim is just as important. It does not claim that the tuple (6, 1, 1, 4) has been derived from the framework's most basic axioms alone; the docstring says this is not full first-principles closure yet. It does not claim that these numbers predict any measured particle mass. It does not claim that the polynomial form itself is forced; that form is a modeling choice. The theorem only says that within the chosen family and under the stated conditions, the tuple is unique.

/-- Upstreamed joint first-principles Z-map tuple forcing:
if `(k, a, b, c)` satisfies smallest-positive-even integerization + minimal-complete-ordered
coefficients + edge-direction color offset, then `(k, a, b, c) = (6, 1, 1, 4)`. -/
theorem zmap_canonical_tuple_forced_from_first_principles
    {k : ℕ} {a b c : ℤ}
    (hk_pos : 0 < k) (hk_even : Even k)
    (hint : integerizes_all k)
    (hmin_k : ∀ k' : ℕ, 0 < k' → Even k' → integerizes_all k' → k ≤ k')
    (hminab : complete_ordered_minimizer a b)
    (hc : c = (edge_direction_count : ℤ)) :
    k = 6 ∧ a = 1 ∧ b = 1 ∧ c = 4 :=
  Verification.ZMapTopologicalDerivation.zmap_canonical_tuple_forced_from_first_principles
    hk_pos hk_even hint hmin_k hminab hc

/-- Upstreamed converse: canonical `(6, 1, 1, 4)` satisfies all first-principles
characterization conditions. -/
theorem zmap_canonical_tuple_satisfies_first_principles :
    integerizes_all 6 ∧
    (∀ k' : ℕ, 0 < k' → Even k' → integerizes_all k' → 6 ≤ k') ∧
    complete_ordered_minimizer 1 1 ∧
    (4 : ℤ) = (edge_direction_count : ℤ) :=
  Verification.ZMapTopologicalDerivation.zmap_canonical_tuple_satisfies_first_principles

/-- Upstreamed iff characterization:
`(k, a, b, c)` is canonical iff it satisfies the bundled first-principles
tuple constraints. -/
theorem canonical_tuple_iff_first_principles (k : ℕ) (a b c : ℤ) :
    first_principles_zmap_tuple k a b c ↔ (k = 6 ∧ a = 1 ∧ b = 1 ∧ c = 4) :=
  Verification.ZMapTopologicalDerivation.canonical_tuple_iff_first_principles k a b c

/-- `k = 6` is the smallest positive even integerization scale for SM charges. -/
theorem smallest_positive_even_integerization_scale :
    integerizes_all 6 ∧
      (∀ k : ℕ, 0 < k → Even k → integerizes_all k → 6 ≤ k) :=
  six_smallest_positive_even_integerizer

/-- Upstreamed minimizer-form selection rule bridge for O2':
any complete ordered minimizer in the topology family is forced to `(a,b)=(1,1)`. -/
theorem complete_ordered_minimizer_forces_unit_coeffs
    {a b : ℤ}
    (hmin : complete_ordered_minimizer a b) :
    a = 1 ∧ b = 1 :=
  Verification.ZMapTopologicalDerivation.complete_ordered_minimizer_forces_unit_coeffs hmin

What this page does not claim

The theorem does not claim that the tuple (6, 1, 1, 4) is derived from the framework's most basic axioms alone. The theorem does not claim that the polynomial form Z = aQ² + bQ⁴ is itself forced; that form is a modeling choice. The theorem does not claim any prediction of a measured particle mass.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/ZMapForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: