Encyclopedia Masses Masses Mass Genesis T10 Genesis Creation Terminal Additive Genesis Rejects No Na
ARTICLE 2 claims 2 theorems
Masses Mass Genesis T10 Genesis Creation Terminal Additive Genesis Rejects No Na
A simple theorem about addition rules out a whole family of explanations for why particle masses take the values they do.
The additive genesis wall
A rule that says which amounts of energy a physical process is allowed to deposit. The rule might be strict, allowing only certain special amounts. But if the rule has one particular property, that it is closed under addition, then it has a fatal weakness. Closure under addition means that whenever two amounts are allowed, their sum is also allowed. The theorem additiveGenesis_rejects_no_nat_multiple states the consequence: if a rule is closed under addition and allows some load L, then it must allow every positive integer multiple of L, including 2L, 3L, 4L, and so on. The proof is a simple induction, a standard mathematical technique that builds up the result step by step from the base case of n equals 1.
This matters because of a specific problem in the Recognition Science framework, which studies how physical structure could be forced by the cost of recognition. The framework needs an absolute scale for particle masses, and one proposed route was a genesis law, a rule for which loads creation can deposit. The admission gate, the test this rule must pass, requires accepting the intended load while rejecting a decoy: a doubled-amplitude witness whose window energy is exactly four times larger. The theorem shows this is impossible for any additive genesis law. Since four times a payable load is payable, the gate cannot reject the decoy. This is not a claim about a specific target value; it holds for any load L whatsoever, in any units.
The only escape is a genesis law that is not additive, one that pays only primitive, indivisible lattice points. That escape also fails, but for different reasons: rational-generated lattices exclude the intended load because the golden ratio is irrational, and phi-generated lattices are blocked by a separate counting obstruction. The conclusion is that the entire class of additive creation laws is dead as a source of absolute scale. The framework's library of machine-checked theorems records this as a terminal result, meaning no additive genesis law can anchor the scale the framework needs.
What the theorem does not claim is equally important. It does not say that no genesis law of any kind can work, only that additive ones cannot. It does not prove that the intended load, phi to the 42 over 4, is actually the right scale; that value is an input, not a conclusion. And it does not establish that any non-additive law succeeds, only that the additive route is closed. The search for a scale-anchoring structure outside the present ledger remains open.
THEOREM additiveGenesis_rejects_no_nat_multiple · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- **A1: the additive genesis gate is impossible.** A genesis law whose
payable loads are closed under addition cannot accept a load while rejecting
its quadruple. Since the doubled-amplitude decoy quadruples the window
energy, no additive genesis law passes the admission gate, for any target,
in any units. -/
theorem additiveGenesis_rejects_no_nat_multiple {Payable : ℝ → Prop}
(hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y))
{L : ℝ} (hintended : Payable L) (n : ℕ) (hn : 1 ≤ n) :
Payable (n * L) := by
rcases n with _ | n
· omega
· exact additivePayable_accepts_nat_mul hadd hintended (n + 1) (Nat.succ_pos _)
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))
What this page does not claim
The theorem does not prove that the intended load phi^42 / 4 is the correct scale. The theorem does not rule out all genesis laws, only additive ones. The theorem does not establish that any non-additive genesis law succeeds.
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 non-additive genesis law could anchor the absolute scale the admission gate demands?
- What structure outside the present ledger could provide the missing scale anchoring?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM additiveGenesis_rejects_no_nat_multiple · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean
/-- **A1: the additive genesis gate is impossible.** A genesis law whose payable loads are closed under addition cannot accept a load while rejecting its quadruple. Since the doubled-amplitude decoy quadruples the window energy, no additive genesis law passes the admission gate, for any target, in any units. -/ theorem additiveGenesis_rejects_no_nat_multiple {Payable : ℝ → Prop} (hadd : ∀ {x y : ℝ}, Payable x → Payable y → Payable (x + y)) {L : ℝ} (hintended : Payable L) (n : ℕ) (hn : 1 ≤ n) : Payable (n * L) := by rcases n with _ | n · omega · exact additivePayable_accepts_nat_mul hadd hintended (n + 1) (Nat.succ_pos _)The theorem additiveGenesis_rejects_no_nat_multiple states the consequence: if a rule is closed under addition and allows some load L, then it must allow every positive integer multiple of L, including 2L, 3L, 4L, and so on. additiveGenesis_rejects_no_nat_multiple · 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 theorem shows this is impossible for any additive genesis law. additiveGenesis_gate_impossible · IndisputableMonolith/Masses/MassGenesis/T10GenesisCreationTerminal.lean