Encyclopedia Masses Masses Mass Genesis T10 Genesis Creation Terminal
ARTICLE 3 claims 3 theorems
Masses Mass Genesis T10 Genesis Creation Terminal
A theorem closes the last route to deriving particle masses from first principles, leaving one open target.
The genesis wall
In the Recognition Science framework, the question of where particle masses come from splits into two routes. One route tried to count something discrete; that path is permanently blocked. The other route, called genesis creation, asked whether a law of how the universe creates patterns could force the absolute scale of masses. The module ledger, a discrete record of events, that would anchor the scale. The terminal theorem shows this route is also closed: no such creation law can work.
The argument is a single line of group theory. A genesis law names which loads creation can deposit, a set of real numbers. If creations compose, meaning depositing one load and then another deposits their sum, then the payable set is closed under addition. The theorem additive payable set that accepts a load must accept every positive integer multiple of it. The admission gate demands that a law accept the intended load but reject a decoy at four times the energy. Since doubling an amplitude quadruples its window energy, the decoy is four times the payable load, so it must be accepted. The gate is impossible for any additive law, for any target, in any units.
The only escape is a creation law that is not additive, one that pays only primitive, indivisible points. That escape dies on the admission gate's own rules. A lattice generated by rational numbers excludes the intended load because the golden ratio is irrational. A lattice generated by the golden ratio itself is blocked by the permanent counting obstruction. A lattice generated by the intended load is circular, since the gate forbids reading the selector's constant off the target it selects. Every remaining class of creation-side conditions was already banked as impossible in earlier rounds.
Both routes are now closed by theorem. The framework's only surviving option is to treat the absolute mass scale as a foundational model law with an explicit origin story, not as a derived consequence. The module names the missing piece: a scale-anchoring structure outside the present ledger, since no additive or lattice creation condition inside it can anchor scale. This is an open target, not an impossibility, and the module states exactly what a future foundation must supply.
THEOREM additivePayable_accepts_nat_mul · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- **An additive payable set accepts every positive integer multiple.**
If creation can deposit `L`, and creations compose, then creation can
deposit `n * L`. -/
theorem additivePayable_accepts_nat_mul {Payable : ℝ → Prop}
(hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y))
{L : ℝ} (hL : Payable L) :
∀ n : ℕ, 0 < n → Payable (n * L)
| 1, _ => by simpa using hL
| n + 2, _ => by
have hn := additivePayable_accepts_nat_mul hadd hL (n + 1) (Nat.succ_pos _)
have h := hadd hn hL
have heq : ((n + 2 : ℕ) : ℝ) * L = ((n + 1 : ℕ) : ℝ) * L + L := by
push_cast
ring
rw [heq]
exact h
THEOREM additiveGenesis_gate_impossible · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- The gate incompatibility, stated against the admission gate itself:
acceptance of the intended witness and rejection of the doubled-scale decoy
cannot coexist in an additive genesis law. -/
theorem additiveGenesis_gate_impossible {Payable : ℝ → Prop}
(hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y))
{L : ℝ} (hintended : Payable L)
(hrejects : ¬ Payable (4 * L)) : False :=
hrejects (additiveGenesis_rejects_no_nat_multiple hadd hintended 4 (by norm_num))
THEOREM additiveGenesis_accepts_gapOne_decoy · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- Instantiation at the gap-one anchor load. The doubled-amplitude witness
has window energy `4 * (phi^42 / 4) = phi^42`
(`doubledAmplitude_windowEnergy_eq_four_mul`), so any additive genesis law
that accepts the anchor load accepts the decoy. -/
theorem additiveGenesis_accepts_gapOne_decoy {Payable : ℝ → Prop}
(hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y))
(hintended : Payable ((Constants.phi : ℝ) ^ 42 / 4)) :
Payable (4 * ((Constants.phi : ℝ) ^ 42 / 4)) :=
additiveGenesis_rejects_no_nat_multiple hadd hintended 4 (by norm_num)
What this page does not claim
This does not claim that no genesis law of any kind can exist, only that the additive and lattice classes are closed. This does not claim that the mass scale is unattainable, only that it is not derivable from within the ledger. This does not claim that the golden ratio is irrational as a new result; it cites that as a known theorem.
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/MassGenesis/T10GenesisCreationTerminal.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:
- What external scale-anchoring structure could a future foundation supply without being circular?
- Does the failure of additive genesis laws rule out all possible creation dynamics, or only those that compose?
- What would it mean for the mass scale to be a foundational model law rather than a derived consequence?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM additivePayable_accepts_nat_mul · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- **An additive payable set accepts every positive integer multiple.** If creation can deposit `L`, and creations compose, then creation can deposit `n * L`. -/ theorem additivePayable_accepts_nat_mul {Payable : ℝ → Prop} (hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y)) {L : ℝ} (hL : Payable L) : ∀ n : ℕ, 0 < n → Payable (n * L) | 1, _ => by simpa using hL | n + 2, _ => by have hn := additivePayable_accepts_nat_mul hadd hL (n + 1) (Nat.succ_pos _) have h := hadd hn hL have heq : ((n + 2 : ℕ) : ℝ) * L = ((n + 1 : ℕ) : ℝ) * L + L := by push_cast ring rw [heq] exact hAn additive payable set that accepts a load must accept every positive integer multiple of it. additivePayable_accepts_nat_mul · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.leanTHEOREM additiveGenesis_gate_impossible · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- The gate incompatibility, stated against the admission gate itself: acceptance of the intended witness and rejection of the doubled-scale decoy cannot coexist in an additive genesis law. -/ theorem additiveGenesis_gate_impossible {Payable : ℝ → Prop} (hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y)) {L : ℝ} (hintended : Payable L) (hrejects : ¬ Payable (4 * L)) : False := hrejects (additiveGenesis_rejects_no_nat_multiple hadd hintended 4 (by norm_num))The admission gate is impossible for any additive genesis law, for any target, in any units. additiveGenesis_gate_impossible · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.leanTHEOREM additiveGenesis_accepts_gapOne_decoy · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- Instantiation at the gap-one anchor load. The doubled-amplitude witness has window energy `4 * (phi^42 / 4) = phi^42` (`doubledAmplitude_windowEnergy_eq_four_mul`), so any additive genesis law that accepts the anchor load accepts the decoy. -/ theorem additiveGenesis_accepts_gapOne_decoy {Payable : ℝ → Prop} (hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y)) (hintended : Payable ((Constants.phi : ℝ) ^ 42 / 4)) : Payable (4 * ((Constants.phi : ℝ) ^ 42 / 4)) := additiveGenesis_rejects_no_nat_multiple hadd hintended 4 (by norm_num)A lattice generated by rational numbers excludes the intended load because the golden ratio is irrational. additiveGenesis_accepts_gapOne_decoy · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean