Masses Mass Genesis T10 Creation Deposit Forcing

The creation deposit

The creation deposit is a formal object in the framework's account of how particle masses arise. It models a minimal event: one posting on each of three spatial axes, the smallest action that flips every parity bit of a three-dimensional lattice. The central result is a proof, checked by a machine, that this deposit carries a normalization of exactly one quarter. The number is not chosen; it is forced by the requirement that each posting be a unit quaternion, a rotation-like object with squared length one.

That requirement fixes the per-posting factor. The unnormalized quarter turn has squared norm two, so the unique positive number making it a unit quaternion is one over the square root of two. The theorem postingNorm_unique proves this. Because transport composes by multiplication, a deposit with one posting on each of the three axes carries the product of three such factors, which is (1/√2)³, exactly √2/4, or one quarter. The proof that the exponent is the lattice dimension appears as creationDepositNorm_eq_pow, and the identity to one quarter as creationDepositNorm_eq_sqrt2_div_four.

The result matters because it explains a previously unexplained prefactor. A candidate amplitude for a particle mass was known to be φ²¹ times √2/4, where φ is the golden ratio. The creation deposit theorem shows the √2/4 is not an arbitrary constant: it is the product of the three per-axis transport normalizations. The amplitude becomes φ²¹ times the deposit normalization. The squared deposit normalization is one eighth, which matches the banked per-tick share of the eight-tick recognition cycle, a separate result in the framework.

In Recognition Science, the framework models this as a gate on what amplitudes are payable. The law accepts the intended amplitude, with the exponent 21, and rejects its double, which would require the golden ratio raised to a power to equal two, a known impossibility. The theorem two_mul_intended_ne_phi_pow_mul_creationDepositNorm records this rejection. An additive composition law, where amplitudes simply sum, is also killed: it would accept the quadruple of the intended value, a decoy that the multiplicative law excludes.

What the framework does not do is explain the φ²¹ remainder. That exponent carries the taint of an electroweak rung, and the framework does not lift it. Whether the tainted candidate is the true absolute mass scale remains undecided. The selection principle that a genesis deposit posts every axis once is proved minimal, but its mechanistic identification as the genesis dynamics remains a conjecture, not a theorem.

/-- **Unitarity forces the normalization (THEOREM).** The unnormalized
quarter factor `1 + a` has squared norm `2`, so `c * (1 + a)` is a unit
quaternion iff `c^2 * 2 = 1`; the unique positive solution is
`c = 1 / sqrt2`. -/
theorem postingNorm_unique {c : ℝ} (hc : 0 < c) (hunit : c ^ 2 * 2 = 1) :
    c = postingNorm := by
  have hc2 : c ^ 2 = 1 / 2 := by linarith
  have h : c = Real.sqrt (1 / 2) := by
    have h1 : c = Real.sqrt (c ^ 2) := (Real.sqrt_sq hc.le).symm
    rw [hc2] at h1
    exact h1
  calc c = Real.sqrt (1 / 2) := h
    _ = Real.sqrt 1 / Real.sqrt 2 := by
        rw [Real.sqrt_div (by norm_num : (0 : ℝ) ≤ 1)]
    _ = 1 / Real.sqrt 2 := by rw [Real.sqrt_one]
    _ = postingNorm := rfl

/-- The exponent is the lattice dimension: the product over `Axis = Fin 3`
of the constant per-posting normalization is its third power. -/
theorem creationDepositNorm_eq_pow : creationDepositNorm = postingNorm ^ 3 := by
  show (∏ _a : Axis, postingNorm) = postingNorm ^ 3
  rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin]

/-- The full-dimension deposit normalization is exactly the off-field factor
`sqrt2 / 4`. -/
theorem creationDepositNorm_eq_sqrt2_div_four :
    creationDepositNorm = Real.sqrt 2 / 4 := by
  rw [creationDepositNorm_eq_pow]
  exact inv_sqrt_two_pow_three

/-- The squared deposit normalization is the banked eight-tick per-tick
share `1/8`: the same `1/8` that enters `f^2 = phi^42/8` through the banked
`f^2 = predictedMass/16` (the two-phase factor `2` cancels the mass law's
two-occupied-phases factor, leaving the per-tick share `8 = 2^3`). -/
theorem creationDepositNorm_sq_eq_one_div_eight :
    creationDepositNorm ^ 2 = 1 / 8 := by
  have h : creationDepositNorm ^ 2 = (postingNorm ^ 2) ^ 3 := by
    rw [creationDepositNorm_eq_pow]; ring
  rw [h, postingNorm_sq]
  norm_num

/-- **Gate discrimination (THEOREM).** The rung-quantum law rejects the
doubled decoy: `2 f = phi^m * creationDepositNorm` would force
`phi^(m-21) = 2`, excluded by the banked `two_not_zpow_phi` (the diagonal
ratio `2` is no integer power of `phi`). -/
theorem two_mul_intended_ne_phi_pow_mul_creationDepositNorm :
    ¬ ∃ k : ℕ, 2 * intendedGapOneFactorAmplitude =
      Constants.phi ^ k * creationDepositNorm := by
  rintro ⟨k, hk⟩
  rw [intended_eq_phi21_mul_creationDepositNorm, creationDepositNorm_eq_pow] at hk
  have hpn : postingNorm ≠ 0 := ne_of_gt postingNorm_pos
  have hk2 : (2 * Constants.phi ^ 21) * postingNorm ^ 3 =
      Constants.phi ^ k * postingNorm ^ 3 := by
    linear_combination hk
  have h1 : 2 * Constants.phi ^ 21 = Constants.phi ^ k :=
    mul_right_cancel₀ (pow_ne_zero 3 hpn) hk2
  have hφ : Constants.phi ≠ 0 := Constants.phi_ne_zero
  have hz : Constants.phi ^ ((k : ℤ) - (21 : ℕ)) = 2 := by
    rw [zpow_sub₀ hφ, zpow_natCast, zpow_natCast, ← h1]
    rw [div_eq_iff (pow_ne_zero 21 hφ)]
  exact two_not_zpow_phi ⟨(k : ℤ) - (21 : ℕ), hz⟩

/-- **The additive-over-axes composition is gate-killed (banked).** Any
deposit law whose payable loads compose additively accepts the quadruple of
every accepted load, hence cannot accept the gap-one load while rejecting
the doubled-scale decoy. This instantiates the banked
`additiveGenesis_accepts_gapOne_decoy`; it is not re-proved here. -/
theorem additive_composition_gate_killed {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_accepts_gapOne_decoy hadd hintended

What this page does not claim

The φ²¹ remainder is not explained by this framework. The mechanistic identification of the genesis deposit with a genesis dynamics is not proved here. The tainted candidate is not established as the true absolute mass scale.

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/T10CreationDepositForcing.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: