Masses Zmap Forcing Complete Ordered Min Budget Forces Unit Coeffs

The coefficient budget

In the Recognition Science framework, the masses of known particles are represented by a ledger, a discrete record of events, through a map that assigns integer charge values to particle families. This map is built from a polynomial with two coefficients, a and b, that scale different powers of a charge variable. The question is which values these coefficients can take.

The theorem complete_ordered_min_budget_forces_unit_coeffs answers a narrow version of that question. It states that if a and b are positive integers, if they satisfy an ordering condition that arranges terms by hierarchy, and if their sum is exactly 2 (the minimal complete budget), then both must be 1. The proof is a short case analysis: the only positive integer pairs summing to 2 are (1,1) and (2,0), and the latter fails the positivity and ordering requirements.

This is a lemma in a larger forcing chain. The same library contains a theorem showing that a complete ordered minimizer, a stronger condition, also forces (1,1). Another theorem combines this with a separate result about integerization scale to force the full tuple (k, a, b, c) = (6, 1, 1, 4), where k is the smallest positive even scale that integerizes Standard Model charges and c is a color offset.

The theorem does not claim that the coefficients are derived from first principles. The ordering condition and the budget constraint are assumptions, not consequences. It also does not claim that the charge map itself is unique or that the polynomial form is forced. Those are separate, open questions. The theorem only shows that within the chosen family, the minimal budget pins down the coefficients.

/-- Topology-only selection-rule bridge:
if a topology-compatible complete polynomial family is ordered and satisfies the
minimal complete coefficient budget, then the coefficients are forced to
`(a,b) = (1,1)`. -/
theorem complete_ordered_min_budget_forces_unit_coeffs
    {a b : ℤ}
    (ha : a ≥ 1)
    (hb : b ≥ 1)
    (hord : ordered_hierarchy a b)
    (hmin : a + b = 2) :
    a = 1 ∧ b = 1 :=
  Verification.ZMapTopologicalDerivation.complete_ordered_min_budget_forces_unit_coeffs
    ha hb hord 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 coefficients are not derived from first principles; the ordering and budget conditions are assumed. The charge map polynomial form is not claimed to be unique or forced. The theorem does not state that the canonical tuple is physically realized, only that it is the unique solution within the stated constraints.

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: