Masses Mass Genesis T10 Posting Cascade Cascade Eigenvalue Amplitude Blind

The amplitude-blind eigenvalue

The declaration cascadeEigenvalue_amplitude_blind proves a precise fact about the posting cascade, a model of how repeated deposits accumulate in a discrete record of events. The theorem states that the cascade's eigenvalue, a number describing how the system responds to a deposit, does not depend on the amplitude parameter a. Two different nonzero amplitudes produce exactly the same eigenvalue for any deposit sequence. The result holds for all sector pairs and all finite deposit lists, and it is proved in the machine-checked library of formal theorems.

What this means in plain terms: the cascade's response to a deposit is blind to the strength of the underlying event. Whether the posting event carries a small or large load, the eigenvalue that records where the deposit lands is identical. The theorem is a direct consequence of the definition of the cascade eigenvalue, which divides the post-deposit weight by the pre-deposit weight. The amplitude cancels in that ratio, leaving only the deposit counts and the golden-ratio powers.

The theorem does not claim that the amplitude is irrelevant to the cascade's behavior overall. It says only that the eigenvalue, the specific quantity defined as the ratio of post- to pre-deposit weights, is amplitude-blind. Other aspects of the cascade, such as the total load or the positivity of weights, do depend on the amplitude. The theorem also does not claim that the eigenvalue determines where deposits land; that question is addressed by other results in the cascade, which show that no principle among the four examined shapes forces a viable deposit location.

theorem cascadeEigenvalue_amplitude_blind {N : ℕ} {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0)
    (ks : List (Fin N)) (i j : SectorN N) :
    cascadeEigenvalue a ks i j = cascadeEigenvalue b ks i j := by
  obtain ⟨n, p⟩ := i
  obtain ⟨m, q⟩ := j
  rw [cascadeEigenvalue_eq ha, cascadeEigenvalue_eq hb]

theorem cascadeEigenvalue_amplitude_blind {N : ℕ} {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0)
    (ks : List (Fin N)) (i j : SectorN N) :
    cascadeEigenvalue a ks i j = cascadeEigenvalue b ks i j := by
  obtain ⟨n, p⟩ := i
  obtain ⟨m, q⟩ := j
  rw [cascadeEigenvalue_eq ha, cascadeEigenvalue_eq hb]

theorem cascadeEigenvalue_eq {N : ℕ} {a : ℝ} (ha : a ≠ 0) (ks : List (Fin N))
    (n m : Fin N) (p q : Fin 2) :
    cascadeEigenvalue a ks (n, p) (m, q) =
      (phi ^ n.val + (depositCount ks n : ℝ)) / phi ^ m.val := by
  have ha2 : a ^ 2 ≠ 0 := pow_ne_zero 2 ha
  have hnum : omegaCascade a ks (n, p) =
      a ^ 2 * (phi ^ n.val + (depositCount ks n : ℝ)) := by
    show postingEventLoad a * phi ^ n.val +
        (depositCount ks n : ℝ) * postingEventLoad a =
      a ^ 2 * (phi ^ n.val + (depositCount ks n : ℝ))
    unfold postingEventLoad
    ring
  have hden : omegaPreN a (m, q) = a ^ 2 * phi ^ m.val := rfl
  unfold cascadeEigenvalue
  rw [hnum, hden, mul_div_mul_left _ _ ha2]

What this page does not claim

The amplitude is irrelevant to all aspects of the cascade's behavior. The eigenvalue determines where deposits land in the cascade. The theorem applies to amplitudes outside the real numbers or to zero amplitude.

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