Masses Zmap Forcing Complete Ordered Minimizer Forces Unit Coeffs

The coefficient forcing

The declaration complete_ordered_minimizer_forces_unit_coeffs is a machine-checked theorem in the framework's library of formal theorems. It states a plain fact about two whole numbers, a and b, that appear as coefficients in a polynomial family used to model particle masses. If the family is complete, meaning it contains all terms the topology allows; ordered, meaning the two coefficients respect a fixed hierarchy; and minimal, meaning their sum is exactly 2; then the only possible values are a = 1 and b = 1. The proof is a short argument in the arithmetic of integers, and the library records it as a theorem with no unproved assumptions.

The classical surface here is the idea of a minimizer: a choice that uses the smallest permitted budget. Given a budget of 2 and two positive whole-number coefficients, the minimal choices are either (1,1) or (2,0), but the ordering condition rules out the second. The theorem's content is that the ordering condition is exactly what selects the unit pair. This is a small piece of a larger forcing chain in the framework, where the same style of argument appears at several levels: a minimal complete choice turns out to be unique.

In Recognition Science, this theorem is one step toward a larger target. The framework models particle masses through a charge map, and a separate theorem shows that if a topology-compatible family matches certain anchor values, then the coefficients are forced to (1,1,4). The minimizer theorem supplies the (1,1) part from pure ordering and budget considerations, without needing the anchor values. The framework's library also bundles a joint result: if the integerization scale k is the smallest positive even integer that makes standard-model charges integral, the coefficients are minimal and ordered, and the color offset is 4, then the whole tuple is (6,1,1,4).

What the declaration does not claim is just as important. It does not claim that the polynomial family is the only possible model, nor that the ordering condition is forced by physics. It establishes a conditional uniqueness: if the family is complete, ordered, and minimal, then the coefficients are 1 and 1. The theorem says nothing about why the budget is 2 or why the ordering holds. Those are separate premises, and the framework's own documentation describes the overall closure as partial, not yet first-principles. The minimizer theorem is a clean logical step, but it is not the whole story of particle masses.

/-- 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

/-- 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

What this page does not claim

The theorem does not claim the polynomial family is the only possible model for particle masses. It does not claim the ordering condition is forced by physics. It does not claim the overall mass closure is complete.

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: