Masses Mass Genesis T10 Genesis Creation Terminal Additive Payable Accepts Nat M

The additive wall

The declaration ledger, a discrete record of events, concerns a simple question about creation rules: if a rule allows the universe to deposit a certain amount of energy, what else must it allow? The theorem additivePayable_accepts_nat_mul answers that if the rule is additive, meaning two allowed deposits can be combined into a third allowed deposit, then it must accept every positive integer multiple of any load it accepts. If it can deposit one unit, it can deposit two, three, four, and so on. This is a direct consequence of the additive property, not a separate assumption.

The proof is an induction. The base case, a multiple of one, is just the original allowed load. The inductive step uses the additive property to combine the load for n with the original load to get the load for n+1. The result is a theorem in the framework's machine-checked library of formal theorems, meaning its derivation is verified step by step. It holds for any additive rule, regardless of what the loads represent or what the target value is.

This theorem is the engine behind a larger negative result. The framework's admission gate for mass values requires accepting an intended load while rejecting a decoy at four times the amplitude. But the additive property forces acceptance of the decoy, because four times a payable load is itself payable. The theorem additiveGenesis_gate_impossible states this contradiction directly: an additive genesis law cannot both accept a load and reject its quadruple. The only escape is a rule that is not additive, such as one that pays only indivisible primitive points, but that path is closed by other theorems involving irrationality and the golden ratio.

In Recognition Science, this closes route A of a fork in the theory of mass genesis. The counting bridge, route B, was already closed. The remaining option is to treat the scale-anchoring law as a foundational model with an explicit origin story, and to name the missing structure that a future foundation must supply. The theorem does not claim that no creation rule can exist, only that no additive one can pass the gate. It does not determine what the intended load should be, and it does not prove that any particular mass value is correct.

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

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

This does not claim that no genesis creation rule of any kind can exist. This does not claim that the intended load phi^42 / 4 is the correct mass scale. This does not claim that a non-additive rule can pass the admission gate.

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: