Masses Excitation Ordering Excitation Cost Pos Of Ne Zero

The cost of an excitation

In the Recognition Science framework, the cost of an excitation is a measure of how much the universe's ledger, a discrete record of events, must change to produce that excitation. The framework proves that this cost is always greater than zero for any excitation except the ground state, which has cost zero. This is the content of the theorem excitationCost_pos_of_ne_zero: for any integer torsion value τ that is not zero, the cost is strictly positive.

The proof rests on a simple monotonicity property of the framework's cost function. The cost function, written J(x) = (x + 1/x)/2 - 1, is zero only when x equals 1. The theorem shows that for any nonzero torsion τ, the value φ^τ is never equal to 1, where φ is the golden ratio. Since φ is greater than 1, φ^τ is either greater than 1 or less than 1, but never exactly 1. Therefore, the cost J(φ^τ) is always positive. The theorem also establishes that the cost is strictly increasing as the torsion value increases, so higher excitations cost more.

This positivity result is a building block for a larger ordering result within the framework. The framework models the three generations of fermions as excitations coupled to the subcells of a three-dimensional cube. The first excitation couples to edges (11 passive edges), the second to faces (6 faces), giving cumulative torsion values of 0, 11, and 17. The positivity and monotonicity theorems together prove the strict cost ordering: cost(0) = 0 < cost(11) < cost(17). This means the framework derives that the edge-supported excitation is cheaper than the face-supported one, purely from the geometry of the cube and the cost function's monotonicity.

The theorem does not claim that the coupling mechanism itself is derived. The premise that excitations couple to subcells in order of CW dimension, from vertices to edges to faces, is a structural assumption, not a consequence of the cost function alone. The theorem also does not claim that the numerical values 11 and 17 are derived from the cost function; they come from the cube's geometry. The framework's contribution is the proof that, given this coupling premise, the cost ordering follows necessarily.

/-- Any nonzero torsion has positive excitation cost. -/
theorem excitationCost_pos_of_ne_zero (τ : ℤ) (hτ : τ ≠ 0) :
    0 < excitationCost τ := by
  apply Jcost_pos_of_ne_one
  · exact zpow_pos phi_pos τ
  · exact fun h => hτ ((phi_zpow_eq_one_iff τ).mp h)

/-- Ground state (τ = 0) has zero excitation cost. -/
theorem excitationCost_ground : excitationCost 0 = 0 := by
  simp [excitationCost, Jcost_unit0]

/-- Excitation cost is strictly monotone for non-negative torsion:
    0 ≤ τ₁ < τ₂ implies J(φ^τ₁) < J(φ^τ₂). -/
theorem excitationCost_strictMono {τ₁ τ₂ : ℤ} (h1 : 0 ≤ τ₁) (h2 : τ₁ < τ₂) :
    excitationCost τ₁ < excitationCost τ₂ := by
  apply Jcost_strict_mono_pos (zpow_pos phi_pos τ₁) (zpow_pos phi_pos τ₂)
  · rcases eq_or_lt_of_le h1 with rfl | hpos
    · simp
    · exact le_of_lt (one_lt_zpow₀ one_lt_phi hpos)
  · exact zpow_lt_zpow_right₀ one_lt_phi h2

/-- The three generation torsion values have strictly ordered J-costs. -/
theorem excitation_cost_ordering :
    excitationCost 0 = 0 ∧
    0 < excitationCost 11 ∧
    excitationCost 11 < excitationCost 17 :=
  ⟨excitationCost_ground,
   excitationCost_pos_of_ne_zero 11 (by omega),
   excitationCost_strictMono (by omega) (by omega)⟩

What this page does not claim

The theorem does not derive the premise that excitations couple in order of CW dimension; that is a structural assumption. The theorem does not derive the numerical values 11 and 17 from the cost function; they come from the cube's geometry. The theorem does not claim that the cost function's positivity holds for all real x, only for x of the form φ^τ with τ nonzero.

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