Masses Mass Genesis T10 Posting Cascade Cascade Diagonal Determines Counts

The diagonal verdict

The declaration cascade_diagonal_gt_one_iff belongs to the framework's study of how deposits accumulate in a discrete ledger, a record of events where each posting adds a fixed quantum to one of a finite set of rungs. The theorem states a precise equivalence: for any nonempty deposit sequence, the diagonal entry of the cascade eigenvalue exceeds 1 at a given rung if and only if that rung has received at least one deposit. In plain terms, the diagonal response of the system acts as a perfect detector of where deposits have landed; it does not merely correlate with the deposit counts, it determines them exactly.

The proof rests on the explicit formula for the cascade eigenvalue, which is (φ^n + count(n)) / φ^m, where count(n) is the number of deposits at rung n. Because the diagonal sets m = n, the expression becomes 1 + count(n) / φ^n, which is greater than 1 precisely when count(n) is positive. The theorem is amplitude-blind: it holds for any nonzero amplitude parameter, because the eigenvalue formula does not depend on it. The diagonal profile therefore encodes the full deposit count vector, and no two distinct deposit sequences can produce the same diagonal signature.

This result is a theorem in the machine-checked library of formal theorems, with no unproved assumptions. It is a structural fact about the cascade construction, not a physical claim about actual particle masses. The framework's own verdict, also proved, states that no principle among the four examined shapes forces a viable nonempty deposit location from the accumulated modular data and the append-only structure. The diagonal theorem tells you what the data says; it does not tell you where the next deposit must go.

theorem cascade_diagonal_gt_one_iff {N : ℕ} {a : ℝ} (ha : a ≠ 0)
    (ks : List (Fin N)) (n : Fin N) (p : Fin 2) :
    1 < cascadeEigenvalue a ks (n, p) (n, p) ↔ 0 < depositCount ks n := by
  rw [cascadeEigenvalue_diag ha]
  constructor
  · intro h
    have h' : (1 : ℝ) * phi ^ n.val < phi ^ n.val + (depositCount ks n : ℝ) :=
      (lt_div_iff₀ (pow_pos phi_pos _)).mp h
    have : (0 : ℝ) < (depositCount ks n : ℝ) := by linarith
    exact Nat.cast_pos.mp this
  · intro h
    rw [lt_div_iff₀ (pow_pos phi_pos _)]
    have : (0 : ℝ) < (depositCount ks n : ℝ) := Nat.cast_pos.mpr h
    linarith [pow_pos phi_pos n.val]

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]

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 conditioning_collapses_to_killed_shape {N : ℕ} (hN : 2 ≤ N)
    (ks : List (Fin N)) (k : Fin N)
    (_hm : MatchesSinglePosting ks k)
    (hdist : SpectrallyDistinguished k) :
    k = rungOne hN :=
  (spectrum_phi_generated_iff hN k).mp hdist

What this page does not claim

The theorem does not claim that any deposit location is physically selected. The theorem does not claim that the diagonal response is the only data that determines deposit counts. The theorem does not claim that the cascade construction applies to any physical system without further modeling assumptions.

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: