Encyclopedia Masses Masses Mass Genesis T10 Directed Posting Modular Seed Settled Window Sqnorm Eq T

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Directed Posting Modular Seed Settled Window Sqnorm Eq T

A small algebraic model shows that a two-phase posting carries exactly twice the squared content of a single phase, and that this ratio is independent of the posting's amplitude.

Verify this page

The settled window's squared norm

The declaration settled_window_sqnorm_eq_two_quanta establishes a precise fact about a ledger, a discrete record of events. In the framework's model, a settled two-phase posting at amplitude a assigns each of its two phases a load of ±a, so the squared content of each phase is a². The declaration proves that the window's total squared norm is exactly 2a², the sum of the two phase quanta. This is a theorem about the definitional choice of the model: the algebra, the weight profile, and the matrix-unit encoding are all MODEL choices, but the squared-norm identity itself is kernel-proved.

The identity matters because it feeds a larger construction. The pre-posting weight is the settled ladder's per-phase content, a² times φⁿ at rung n, where φ is the golden ratio. The post-posting weight appends one new deposit of a² per phase at the base rung. The ratio of the post weight to the pre weight is 2 at the posted rung and 1 at the other rung, so the two weights are not proportional. That non-proportionality is what makes the relative modular operator non-scalar, a fact proved separately as relativeModular_not_scalar. The squared-norm identity is the seed of that ratio.

What the declaration does not claim is broader. It does not claim that the ratio 2 is generated by φ alone; in fact, the theorem two_not_zpow_phi proves that 2 is no integer power of φ. It does not claim that √2 lies in the rational-φ field; the theorem sqrt_two_not_inQPhi proves it does not. The declaration does not attempt a type III1 classification, and it does not establish the Krieger ratio set of any infinite factor completion. It proves only the finite point spectrum of the seed's modular operator and its two escape clauses. The amplitude a cancels in every ratio, so the result is measurement-freedom: no anchor numeral appears anywhere in the module.

In plain terms, the declaration pins down one number: the squared norm of a settled two-phase posting is twice the squared content of a single phase, regardless of the posting's size. That fact is the foundation for the modular spectrum {1, 2, φ, 2/φ}, where the √2 appears on the posted rung's diagonal units. The reader can now see why the posting's signature is the diagonal ratio 2 and its square root, not a power of φ.

THEOREM relativeModular_not_scalar · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
relativeModular_not_scalar · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean:356 
/-- **PROPOSITION 2: the relative modular operator is not scalar.** The
posted rung's diagonal eigenvalue is `2`, the unposted rung's is `1`, and no
single scalar can be both. -/
theorem relativeModular_not_scalar {a : ℝ} (ha : a ≠ 0) :
    ¬ ∃ c : ℂ, ∀ X : M4, relativeModular a X = c • X := by
  rintro ⟨c, hc⟩
  have h00 := hc (Matrix.single 0 0 (1 : ℂ))
  rw [relativeModular_eigen, eigen_00 ha] at h00
  have h22 := hc (Matrix.single 2 2 (1 : ℂ))
  rw [relativeModular_eigen, eigen_22 ha] at h22
  have key : ∀ (d : ℝ) (i : Sector),
      ((d : ℝ) : ℂ) • Matrix.single i i (1 : ℂ) = c • Matrix.single i i (1 : ℂ) →
      ((d : ℝ) : ℂ) = c := by
    intro d i h
    have e := congr_fun (congr_fun h i) i
    simp [Matrix.single] at e
    exact e
  have e1 := key 2 0 h00
  have e2 := key 1 2 h22
  have h21 : ((2 : ℝ) : ℂ) = ((1 : ℝ) : ℂ) := by rw [e1, e2]
  norm_num at h21
THEOREM relativeModular_not_scalar · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
relativeModular_not_scalar · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean:356 
/-- **PROPOSITION 2: the relative modular operator is not scalar.** The
posted rung's diagonal eigenvalue is `2`, the unposted rung's is `1`, and no
single scalar can be both. -/
theorem relativeModular_not_scalar {a : ℝ} (ha : a ≠ 0) :
    ¬ ∃ c : ℂ, ∀ X : M4, relativeModular a X = c • X := by
  rintro ⟨c, hc⟩
  have h00 := hc (Matrix.single 0 0 (1 : ℂ))
  rw [relativeModular_eigen, eigen_00 ha] at h00
  have h22 := hc (Matrix.single 2 2 (1 : ℂ))
  rw [relativeModular_eigen, eigen_22 ha] at h22
  have key : ∀ (d : ℝ) (i : Sector),
      ((d : ℝ) : ℂ) • Matrix.single i i (1 : ℂ) = c • Matrix.single i i (1 : ℂ) →
      ((d : ℝ) : ℂ) = c := by
    intro d i h
    have e := congr_fun (congr_fun h i) i
    simp [Matrix.single] at e
    exact e
  have e1 := key 2 0 h00
  have e2 := key 1 2 h22
  have h21 : ((2 : ℝ) : ℂ) = ((1 : ℝ) : ℂ) := by rw [e1, e2]
  norm_num at h21
THEOREM two_not_zpow_phi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
two_not_zpow_phi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean:737 
/-- **Escape 1: the diagonal ratio `2` is no integer power of `phi`.**
`phi^0 = 1`, `phi^1 < 2`, `phi^k >= phi^2 > 2.5` for `k >= 2`, and
`0 < phi^k < 1` for `k < 0`. So the modular ratio group is not generated by
`phi` alone. -/
theorem two_not_zpow_phi : ¬ ∃ k : ℤ, phi ^ k = 2 := by
  rintro ⟨k, hk⟩
  rcases lt_trichotomy k 0 with hneg | rfl | hpos
  · have h2 : phi ^ k < 1 := by
      have hmk : (1 : ℝ) < phi ^ (-k) := one_lt_zpow₀ one_lt_phi (by omega)
      have hinv : phi ^ k = (phi ^ (-k))⁻¹ := by
        rw [← zpow_neg, neg_neg]
      rw [hinv]
      exact inv_lt_one_of_one_lt₀ hmk
    linarith [hk, h2]
  · rw [zpow_zero] at hk
    norm_num at hk
  · rcases eq_or_lt_of_le (show (1 : ℤ) ≤ k from hpos) with h1 | h2
    · subst h1
      rw [zpow_one] at hk
      linarith [phi_lt_two, hk]
    · have hk2 : phi ^ k = phi ^ (2 : ℤ) * phi ^ (k - 2) := by
        rw [← zpow_add₀ (ne_of_gt phi_pos)]
        congr 1
        omega
      have hge1 : (1 : ℝ) ≤ phi ^ (k - 2) := one_le_zpow₀ one_lt_phi.le (by omega)
      have h25 : (2.5 : ℝ) < phi ^ (2 : ℤ) := by
        rw [zpow_ofNat]
        exact phi_squared_bounds.1
      have hmul : phi ^ (2 : ℤ) * (1 : ℝ) ≤ phi ^ (2 : ℤ) * phi ^ (k - 2) :=
        mul_le_mul_of_nonneg_left hge1 (le_of_lt (zpow_pos phi_pos 2))
      have hgt : phi ^ k > 2 := by
        rw [hk2]
        linarith [hmul, h25]
      linarith [hk, hgt]
THEOREM sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean:772 
/-- **Escape 2: `sqrt(2)` is not in the rational-phi field.** If
`sqrt(2) = p + q phi` with rational `p q`, squaring and using `phi^2 =
phi + 1` with rational independence gives `p^2 + q^2 = 2` and
`2 p q + q^2 = 0`; the first case makes `2` a rational square, the second
makes `10` one. Both are `2 mod 4`, contradiction. -/
theorem sqrt_two_not_inQPhi : ¬ InQPhi (Real.sqrt 2) := by
  rintro ⟨p, q, hpq⟩
  have hsq : ((p : ℝ) + (q : ℝ) * phi) ^ 2 = 2 := by
    rw [← hpq, Real.sq_sqrt (by norm_num)]
  have hexp : ((p ^ 2 + q ^ 2 : ℚ) : ℝ) + ((2 * p * q + q ^ 2 : ℚ) : ℝ) * phi
      = ((2 : ℚ) : ℝ) + ((0 : ℚ) : ℝ) * phi := by
    push_cast
    linear_combination hsq - (q : ℝ) ^ 2 * phi_sq_eq
  obtain ⟨h1, h2⟩ := rat_linear_independent hexp
  have hq0 : q * (2 * p + q) = 0 := by linear_combination h2
  rcases mul_eq_zero.mp hq0 with hqz | hqz
  · subst hqz
    simp at h1
    exact not_rat_sq_of_two_mod_four (by norm_num : 2 % 4 = 2) (by exact_mod_cast h1)
  · have hqeq : q = -2 * p := by linear_combination hqz
    rw [hqeq] at h1
    have h5 : 5 * p ^ 2 = 2 := by linear_combination h1
    have h10 : (5 * p) ^ 2 = 10 := by linear_combination 5 * h5
    exact not_rat_sq_of_two_mod_four (by norm_num : 10 % 4 = 2) (by exact_mod_cast h10)

What this page does not claim

The declaration does not claim that the ratio 2 is generated by φ alone. The declaration does not claim that √2 lies in the rational-φ field. The declaration does not attempt a type III1 classification or establish the Krieger ratio set of any infinite factor completion.

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/T10DirectedPostingModularSeed.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