Foundation Schrodinger Derivation Discrete Schrodinger Eigenmode

The discrete eigenmode equation

The Schrödinger equation is the rule that tells a quantum system how its state changes from one instant to the next. In its familiar continuous form, iℏ∂ψ/∂t = Ĥψ, it describes an evolving wavefunction ψ under the action of an energy operator Ĥ. The equation is normally taken as a starting point of quantum mechanics, not something one derives from more basic principles.

In Recognition Science, the equation is not a postulate. The framework begins with a different picture: reality keeps a ledger, a discrete record of recognition events, and each event advances the system by one step. For an eight-step cycle, the state of the system at any moment is a list of eight complex numbers, written Signal8. One step of the cycle is a cyclic shift, moving each entry one position forward. The declaration discrete_schrodinger_eigenmode proves, as a theorem in the framework's machine-checked library, that a single step of this cycle on any basic mode is exactly the integrated Schrödinger flow for that mode: ψ(τ₀) = exp(-iE_k τ₀/ℏ) · ψ(0). The energy E_k = ℏ·πk/(4τ₀) comes out of the cycle itself, with ℏ and τ₀ fixed by the framework's constants.

The theorem is one of eight linked results in the module. Together they show that the shift operator is linear, that it preserves the norm of each mode, that the energies are real and nonnegative, and that the full evolution on any eight-component state is a superposition of these basic modes. The Taylor expansion of the one-step phase then recovers the continuous Schrödinger equation, with a remainder that vanishes in the slow-mode limit. The framework's library checks every step with no gaps and no special axioms beyond the standard logical ones.

What the declaration does not claim is just as important. It does not claim that the continuous Schrödinger equation holds exactly at every instant; the discrete version is exact, and the continuum form is a limit with a bounded remainder. It does not claim that this derivation replaces the physical postulates of quantum mechanics, only that within the framework the equation follows from the recognition cycle. And it does not claim that the energies match any measured spectrum; the comparison to experiment is a separate empirical check, not part of the theorem.

/-- **DISCRETE SCHRÖDINGER (eigenmode form).** For every DFT mode `k`
    and every coefficient `c`, the integrated one-tick evolution is
    exactly `ψ(τ₀) = exp(-i E_k τ₀ / ℏ) · ψ(0)`. -/
theorem discrete_schrodinger_eigenmode (k : Fin 8) (c : ℂ) :
    cyclic_shift (c • dft8_mode k) =
      Complex.exp (-Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ))
        • (c • dft8_mode k) := by
  rw [eigenmode_evolution_scaled k c]
  rw [omega8_pow_eq_evolution_factor k]

/-- The recognition-Hamiltonian eigenvalue on the k-th DFT mode.

    By identifying the one-tick phase `ω₈^k = exp(-iπk/4)` with the
    Schrödinger evolution factor `exp(-i E_k τ₀ / ℏ)`, we read off
    `E_k = ℏ · πk / (4 τ₀)`. With the RS-native quanta
    `ℏ = φ⁻⁵`, `τ₀ = 1`, this gives `E_k = φ⁻⁵ · πk / 4`. -/
def quarterTurnEnergy (k : Fin 8) : ℝ :=
  hbar * (Real.pi * (k.val : ℝ)) / (4 * tau0)

/-- **LINEARITY.** The one-tick recognition evolution is `ℂ`-linear,
    so the discrete Schrödinger equation extends from eigenmodes to
    arbitrary linear combinations. -/
theorem schrodinger_linear (ψ φ : Signal8) (a b : ℂ) :
    cyclic_shift (a • ψ + b • φ) = a • cyclic_shift ψ + b • cyclic_shift φ := by
  rw [cyclic_shift_add, cyclic_shift_smul, cyclic_shift_smul]

/-- One-tick evolution preserves the norm on each mode (unitarity). -/
theorem eigenmode_norm_preserved (k : Fin 8) (c : ℂ) (t : Fin 8) :
    ‖cyclic_shift (c • dft8_mode k) t‖ = ‖(c • dft8_mode k) t‖ := by
  rw [eigenmode_evolution_scaled k c]
  -- Now: ‖((omega8^k.val) • (c • dft8_mode k)) t‖ = ‖(c • dft8_mode k) t‖
  simp only [Pi.smul_apply, smul_eq_mul, norm_mul]
  have homega : ‖omega8 ^ k.val‖ = 1 := by
    rw [norm_pow, omega8_abs, one_pow]
  rw [homega, one_mul]

/-- The Hamiltonian eigenvalues are real: `Ĥ_RS` is Hermitian. -/
theorem quarterTurnEnergy_real (k : Fin 8) :
    (quarterTurnEnergy k : ℂ).im = 0 := by
  simp

/-- Energy nonnegativity: every eigenvalue is `≥ 0`. -/
theorem quarterTurnEnergy_nonneg (k : Fin 8) : 0 ≤ quarterTurnEnergy k := by
  unfold quarterTurnEnergy
  have h1 : 0 ≤ hbar := le_of_lt hbar_pos
  have h2 : 0 ≤ Real.pi * (k.val : ℝ) :=
    mul_nonneg Real.pi_pos.le (Nat.cast_nonneg _)
  have h3 : 0 ≤ hbar * (Real.pi * (k.val : ℝ)) := mul_nonneg h1 h2
  have h4 : 0 < 4 * tau0 := by
    have htau : 0 < tau0 := tau0_pos
    linarith
  exact div_nonneg h3 h4.le

/-- **TAYLOR REMAINDER BOUND.** For each eigenmode `k`, when the
    one-tick phase satisfies `‖ -i E_k τ₀ / ℏ ‖ ≤ 1`, the increment
    `cyclic_shift (c • dft8_mode k) - (c • dft8_mode k) - z • (c • dft8_mode k)`
    differs from the linear-in-τ₀ Schrödinger drift by at most a
    quadratic remainder.

    Specifically, with `z := -i E_k τ₀ / ℏ`, the residual
    `(exp z - 1 - z) · ψ` is bounded by `‖z‖² · ‖ψ‖`. -/
theorem schrodinger_remainder_bound (k : Fin 8) (c : ℂ) (t : Fin 8)
    (hsmall : ‖(-Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ))‖ ≤ 1) :
    let z : ℂ := -Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ)
    ‖(Complex.exp z - 1 - z) • (c • dft8_mode k) t‖ ≤
      ‖z‖ ^ 2 * ‖(c • dft8_mode k) t‖ := by
  intro z
  have hbnd := exp_taylor_remainder hsmall
  rw [Pi.smul_apply, smul_eq_mul, norm_mul]
  exact mul_le_mul_of_nonneg_right hbnd (norm_nonneg _)

What this page does not claim

The continuous Schrödinger equation holds exactly at all times; only the discrete step is exact, and the continuum form is a limit with a bounded remainder. This derivation replaces the physical postulates of quantum mechanics; it shows a consequence within the framework. The energies E_k match any measured atomic spectrum; no comparison to experiment is part of this theorem.

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/Foundation/SchrodingerDerivation.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: