Masses Mass Genesis T10 Rung Tower Modular Flow

The rung tower's verdict

The golden ratio φ appears throughout mathematics, from pentagon geometry to the Fibonacci sequence. In Recognition Science, it also appears in a tower model for how mass might be generated. The tower is a ladder of rungs, and each rung can hold a quantum of mass. The framework's central claim is that a mass at rung n carries a weight proportional to φ raised to the power n. This is a definitional choice, a model, not a derived fact.

The model also includes a single deposit event: one extra quantum of mass is placed at a chosen rung. The question is whether the tower's internal structure, its modular spectrum, can reveal which rung received the deposit. The spectrum is a list of ratios that arises from comparing the tower before and after the deposit. The result proves that this spectrum is completely determined by the deposit's location, but it also proves something more subtle.

The key result is an absorption phenomenon. The golden identity 1 + φ = φ² means that a deposit at rung 1 lands exactly on the tower's own scale: the spectrum stays entirely within the set of powers of φ. At any other rung, the deposit introduces a ratio that is not a power of φ, a non-phi trace. The theorem states that the spectrum is generated by φ alone if and only if the deposit sits at rung 1. This is a proved fact, not a conjecture.

However, this unique selection is exactly the wrong answer for the campaign. The campaign's target is the electroweak rung 55, a viable rung. The result proves that no sector-invariant principle, one that depends only on the spectrum as a set of numbers, can select a viable rung. The spectrum faithfully records which rung received the deposit, but it cannot derive why that rung was chosen. The deposit's location must be an input, not an output.

This is a negative result with scope. The tower's modular data is a faithful ledger of the deposit event, but it is not a principle that generates the deposit's location. The next step is to find a mechanism that derives where the posting lands. This framework provides the machinery to make that question statable.

/-- The sector space of the tower algebra: rung `n : Fin N`, phase `Fin 2`
(`commit = 0`, `clear = 1`). -/
abbrev SectorN (N : ℕ) := Fin N × Fin 2

/-- **The absorption dichotomy, pointwise.** `1 + phi^k` is an integer power
of `phi` if and only if `k = 1`: the golden identity at rung 1, the banked
`two_not_zpow_phi` at rung 0, and the strict between-powers bound above. -/
theorem one_add_phi_pow_zpow_iff {N : ℕ} (hN : 2 ≤ N) (k : Fin N) :
    (∃ j : ℤ, phi ^ j = 1 + phi ^ k.val) ↔ k = rungOne hN := by
  constructor
  · rintro ⟨j, hj⟩
    by_cases hk0 : k.val = 0
    · exfalso
      rw [hk0, pow_zero] at hj
      have h2 : phi ^ j = 2 := by
        rw [hj]
        norm_num
      exact two_not_zpow_phi ⟨j, h2⟩
    · by_cases hk1 : k.val = 1
      · exact Fin.ext hk1
      · exfalso
        exact one_add_phi_pow_not_zpow_of_ge_two (by omega) ⟨j, hj⟩
  · intro hk
    rw [hk]
    refine ⟨((2 : ℕ) : ℤ), ?_⟩
    rw [zpow_natCast, rungOne_val, pow_one]
    exact one_add_phi_one.symm

/-- **C1 regression.** At `N = 2, k = 0` the tower spectrum is exactly the C1
spectrum `{1, 2, phi, 2/phi}`. -/
theorem c1_spectrum_shape :
    modularSpectrum (⟨0, by omega⟩ : Fin 2) = ({1, 2, phi, 2 / phi} : Set ℝ) := by
  ext x
  constructor
  · rintro (⟨n, m, hnk, rfl⟩ | ⟨m, rfl⟩)
    · have hn1 : n.val = 1 := by
        have hlt := n.isLt
        by_contra hnv
        have hv0 : n.val = 0 := by omega
        exact hnk (Fin.ext hv0)
      have hm : m.val = 0 ∨ m.val = 1 := by have hlt := m.isLt; omega
      rcases hm with hm0 | hm1
      · rw [hn1, hm0, pow_one, pow_zero, div_one]
        simp
      · rw [hn1, hm1, pow_one, div_self (ne_of_gt phi_pos)]
        simp
    · have hm : m.val = 0 ∨ m.val = 1 := by have hlt := m.isLt; omega
      rcases hm with hm0 | hm1
      · rw [hm0]
        show (1 + phi ^ (0 : ℕ)) / phi ^ (0 : ℕ) ∈ ({1, 2, phi, 2 / phi} : Set ℝ)
        rw [pow_zero, div_one, show (1 : ℝ) + 1 = 2 by norm_num]
        simp
      · rw [hm1]
        show (1 + phi ^ (0 : ℕ)) / phi ^ (1 : ℕ) ∈ ({1, 2, phi, 2 / phi} : Set ℝ)
        rw [pow_zero, pow_one, show (1 : ℝ) + 1 = 2 by norm_num]
        simp
  · intro hx
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hx
    rcases hx with rfl | rfl | rfl | rfl
    · refine Or.inl ⟨⟨1, by omega⟩, ⟨1, by omega⟩, by decide, ?_⟩
      show (1 : ℝ) = phi ^ (1 : ℕ) / phi ^ (1 : ℕ)
      rw [pow_one, div_self (ne_of_gt phi_pos)]
    · refine Or.inr ⟨⟨0, by omega⟩, ?_⟩
      show (2 : ℝ) = (1 + phi ^ (0 : ℕ)) / phi ^ (0 : ℕ)
      rw [pow_zero, div_one]
      norm_num
    · refine Or.inl ⟨⟨1, by omega⟩, ⟨0, by omega⟩, by decide, ?_⟩
      show (phi : ℝ) = phi ^ (1 : ℕ) / phi ^ (0 : ℕ)
      rw [pow_one, pow_zero, div_one]
    · refine Or.inr ⟨⟨1, by omega⟩, ?_⟩
      show (2 / phi : ℝ) = (1 + phi ^ (0 : ℕ)) / phi ^ (1 : ℕ)
      rw [pow_zero, pow_one]
      norm_num

What this page does not claim

No sector-invariant principle selects a viable rung; the deposit location is an input, not a derived output. The tower model does not predict the electroweak rung 55; it only provides a framework where the question can be asked. The result does not apply to infinite towers or to type III1 von Neumann algebra classifications.

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