Encyclopedia Masses Masses Mass Genesis T10 Directed Posting Modular Seed No Posting Diagonal Eigenv
ARTICLE 3 claims 3 theorems
Masses Mass Genesis T10 Directed Posting Modular Seed No Posting Diagonal Eigenv
A machine-checked theorem isolates the exact fingerprint of a single irreversible accounting event, distinguishing it from the background it lands in.
The posting's signature
In the Recognition Science framework, a ledger is a discrete record of events, and the framework's library is a machine-checked collection of formal theorems about such records. One question the framework asks is whether a single new entry can be told apart from the structure that was already there. The declaration no_posting_diagonal_eigenvalue_one answers that question for a specific, minimal construction: it proves that the new entry, called a posting, leaves a measurable signature that no background fluctuation can mimic.
The setup is a four-sector algebra, two phases of a settlement window crossed with two rungs of a ladder. Before the posting, the ledger's weight profile follows a golden-ratio ladder, with the ratio phi appearing between rungs. The posting adds one quantum of load at the base rung only. The theorem's content is about the relative modular operator, a standard tool from operator algebra that compares two states on the algebra: the state before the posting and the state after. The operator's eigenvalues are the ratios of the two weights at each sector. The theorem states that without the posting, every diagonal eigenvalue is 1, meaning the two states are identical on the diagonal. With the posting, the diagonal eigenvalue at the posted rung becomes 2, and its square root becomes sqrt(2). This is the posting's unique fingerprint.
The proof is a control argument. It shows that the appearance of sqrt(2) in the modular spectrum is entirely due to the posting, not to the golden-ratio background. The background alone, with its phi ratios, produces only the eigenvalue 1 on the diagonal. The posting introduces the ratio 2 and its square root, and these are not powers of phi. The theorem also proves that sqrt(2) does not lie in the field generated by phi over the rationals, so the posting's signature is genuinely new content, not a rearrangement of the ladder's existing ratios.
This matters because it gives a precise, checkable way to identify a single irreversible event in a ledger. The framework models the posting as a nilpotent matrix unit, an operation that cannot be undone. The theorem shows that this operation has a measurable consequence in the modular data, one that is provably absent when no posting occurs. The result is a theorem, proved in the machine-checked library, about a specific definitional model. The model is a choice; the properties proved about it are not.
The declaration does not claim that this construction describes any physical system. It does not claim that the golden-ratio ladder is the only possible background, nor that the posting's signature is the only way to detect an event. It establishes a precise mathematical fact about a minimal example, and that fact is what the framework uses as a building block for larger claims about mass generation.
THEOREM sectorRung_one · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
private theorem sectorRung_one : sectorRung 1 = 0 := by decide
THEOREM two_not_zpow_phi · sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
/-- **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]
/-- **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)
THEOREM sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
/-- **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 theorem does not claim that the golden-ratio ladder is the only possible background for a ledger. The theorem does not claim that the posting's signature is the only way to detect an event. The theorem does not claim that this minimal construction describes any physical system.
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:
- How does the posting's modular signature connect to the framework's derivation of particle masses?
- What larger constructions build on this minimal seed to model realistic mass spectra?
- Does the non-commutation of the modular square root with the orbit translation have a physical interpretation?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM sectorRung_one · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
private theorem sectorRung_one : sectorRung 1 = 0 := by decideThe theorem proves that without the posting, every diagonal eigenvalue is 1. sectorRung_one · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.leanTHEOREM two_not_zpow_phi · sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
/-- **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]/-- **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)The posting introduces the ratio 2 and its square root, and these are not powers of phi. two_not_zpow_phi · sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.leanTHEOREM sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean
/-- **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)The theorem proves that sqrt(2) does not lie in the field generated by phi over the rationals. sqrt_two_not_inQPhi · IndisputableMonolith/Masses/MassGenesis/T10DirectedPostingModularSeed.lean