Masses Mass Genesis T10 Rung Tower Modular Flow Orbit Translation N Sqrt Modular

The cyclic shift and its obstruction

In the Recognition Science framework, a ledger is a discrete record of events, and the rung tower is a model of particle masses as weights on N rungs, each with two phases (commit and clear). The modular operator is a matrix that encodes how the ledger's weights change after an irreversible posting event: one deposit of a quantum at a chosen rung. Its square root is the operator whose square gives the modular operator back.

The declaration orbitTranslationN_sqrtModular_noncommute proves, in the machine-checked library of formal theorems, that a cyclic shift of the rungs (moving each rung to the next, wrapping around) does not commute with the modular square root. Concretely, applying the shift first and then the square root gives a different result than applying the square root first and then the shift. The theorem is witnessed at the cyclic predecessor of the deposit rung, meaning the obstruction appears exactly one step before the rung where the deposit lands. This is a theorem about the finite matrix algebra, not a physical claim about particles.

What this establishes is negative with scope: the cyclic symmetry of the rung labels is broken by the modular structure. The tower's modular data does faithfully record which rung received the deposit, but the shift symmetry does not survive the square root. This matters because the framework's campaign seeks a principle that selects a distinguished rung from sector invariants alone; the non-commutation shows that the cyclic shift is not such a principle, since it cannot be used to map the modular structure onto itself.

The theorem does not claim that no symmetry of the tower exists, nor that the deposit rung is undetectable. It does not claim that the modular operator itself fails to record the deposit: the diagonal response at the deposit rung is strictly greater than 1, and the unlabeled spectrum determines the rung. It also does not claim anything about infinite-dimensional von Neumann algebras or Krieger ratio sets, which are explicitly out of scope. The non-commutation is proved for the specific orbit translation operator defined as a permutation matrix, with the adjoint action AdUN X = U X U†, and nothing more.

For the reader, the consequence is precise: the cyclic shift is a symmetry of the rung labels but not of the modular square root, so any selection principle that respects the modular structure cannot be built from this shift. The machinery makes the next question statable, namely where the deposit lands, but does not answer it.

/-- The orbit translation unitary: the permutation matrix of `rungShiftN`. -/
def orbitTranslationN {N : ℕ} (hN0 : 0 < N) : MN N :=
  fun i j => if j = rungShiftN hN0 i then (1 : ℂ) else 0

/-- Every rung has a cyclic predecessor, and it is never the rung itself
(for `N ≥ 2`). -/
theorem pred_exists {N : ℕ} (hN : 2 ≤ N) (k : Fin N) :
    ∃ x0 : Fin N, rungShiftN (by omega) (x0, commit) = (k, commit) ∧ x0 ≠ k := by
  by_cases hk : k.val = 0
  · refine ⟨⟨N - 1, by omega⟩, ?_, ?_⟩
    · unfold rungShiftN
      congr 1
      apply Fin.ext
      show (N - 1 + 1) % N = k.val
      rw [show N - 1 + 1 = N by omega, Nat.mod_self, hk]
    · intro heq
      have hv := congr_arg Fin.val heq
      change N - 1 = k.val at hv
      omega
  · refine ⟨⟨k.val - 1, by omega⟩, ?_, ?_⟩
    · unfold rungShiftN
      congr 1
      apply Fin.ext
      show (k.val - 1 + 1) % N = k.val
      rw [show k.val - 1 + 1 = k.val by omega, Nat.mod_eq_of_lt k.isLt]
    · intro heq
      have hv := congr_arg Fin.val heq
      change k.val - 1 = k.val at hv
      omega

/-- The relative modular operator of the pair: `Delta(X) = rho' X rho^{-1}`
(Connes/Tomita, finite-dimensional form). -/
def relativeModularN (a : ℝ) {N : ℕ} (k : Fin N) (X : MN N) : MN N :=
  rhoPostN a k * X * rhoPreInvN a

What this page does not claim

The theorem does not claim that the cyclic shift commutes with the modular operator itself, only with its square root. The theorem does not claim that the deposit rung is undetectable from the modular spectrum. The theorem does not claim anything about infinite-dimensional von Neumann algebras or Krieger ratio sets.

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: