Encyclopedia Masses Masses Mass Genesis T10 Rung Tower Modular Flow Modular Eigenvalue N Amplitude B

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Rung Tower Modular Flow Modular Eigenvalue N Amplitude B

A tower of rungs records a single deposit; the record's shape turns out not to depend on how heavy the deposit is.

Verify this page

The amplitude-blind spectrum

In the Recognition Science framework, a ledger (a discrete record of events) can be built as a ladder of rungs, each rung holding a weight that grows by the golden ratio phi as you climb. A single irreversible event, a posting, adds one extra quantum at one chosen rung. The question is whether the modular spectrum, a set of ratios derived from the weights before and after the posting, can reveal which rung received the deposit.

The declaration modularEigenvalueN proves a striking fact: the spectrum does not depend on the overall amplitude a of the weights. Every ratio that forms the spectrum divides one post-posting weight by one pre-posting weight, and the common factor a^2 cancels in every such division. The spectrum is exactly the set { phi^n / phi^m : n ≠ k } ∪ { (1 + phi^k) / phi^m }, where k is the deposit rung. No amplitude numeral appears anywhere in this description.

This amplitude blindness is a theorem, proved in the framework's machine-checked library of formal theorems. It holds for any number of rungs N and any deposit rung k. At N = 2 and k = 0, the spectrum reduces to the four values {1, 2, phi, 2/phi}, matching the earlier two-rung case. The result matters because it shows the spectrum is a pure shape, a fingerprint of the tower's structure and the deposit's location, not a number that depends on how strong the deposit is.

What the theorem does not claim is equally important. It does not say the spectrum identifies the deposit rung; in fact, the spectrum alone does determine k, but that is a separate result. The amplitude-blind statement only says the spectrum is independent of a. It also does not claim that the spectrum is generated by phi alone; that is a different property, one that holds only when the deposit sits at rung 1. The theorem is a precise, narrow fact about cancellation, not a claim about which rung is special.

In the framework's campaign to derive particle masses, this result is a tool. It isolates the modular spectrum as a structural invariant, one that can be studied without tracking the amplitude. The next step, deriving where the posting lands, remains open; this theorem makes that question statable by clearing away the amplitude dependence.

THEOREM modularEigenvalueN · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean
modularEigenvalueN · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean:227 
/-- The modular eigenvalue on the matrix unit `E_{ij}`: the ratio
`omegaPost(i) / omegaPre(j)`. -/
def modularEigenvalueN (a : ℝ) {N : ℕ} (k : Fin N) (i j : SectorN N) : ℝ :=
  omegaPostN a k i / omegaPreN a j
THEOREM c1_spectrum_shape · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean
c1_spectrum_shape · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean:398 
/-- **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
THEOREM c1_spectrum_shape · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean
c1_spectrum_shape · IndisputableMonolith/Masses/MassGenesis/T10RungTowerModularFlow.lean:398 
/-- **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

The spectrum identifies the deposit rung. The spectrum is generated by phi alone. The amplitude a is zero or has any particular value.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND