Foundation Schrodinger Derivation Schrodinger Difference Eigenmode

The difference equation

The Schrödinger equation is the rule that tells how a quantum state changes with time. In its familiar form, iℏ∂ψ/∂t = Ĥψ, it is a differential equation: it describes an infinitesimal step. The declaration schrodinger_difference_eigenmode concerns the difference version of that step. It states that for any one of the eight basic modes of the system, applying the one-tick evolution operator and then subtracting the original mode equals the original mode multiplied by a phase factor minus one. In symbols, the theorem reads: cyclic_shift(c · dft8_mode k) − (c · dft8_mode k) = (exp(−iE_k τ₀/ℏ) − 1) · (c · dft8_mode k).

That equation is not an approximation. It is an exact identity, proved in the machine-checked library of formal theorems, and it holds for every mode index k and every complex coefficient c. The difference form is useful because it isolates the change caused by one tick of evolution. The factor (exp(−iE_k τ₀/ℏ) − 1) is the amount by which the mode's phase advances in a single step. When that step is small, the exponential can be expanded in a Taylor series, and the leading term recovers the familiar differential form of the Schrödinger equation. The library also proves a bound on the remainder of that expansion, so the passage from difference to differential form is controlled, not hand-waved.

The declaration sits inside a larger derivation. The eight modes come from an eight-tick recognition cycle, and the evolution operator is a cyclic shift on those eight points. The energies E_k are real and nonnegative, which makes the generator Hermitian. The theorem also records that the evolution preserves the norm of each mode and that superpositions evolve linearly. These are the standard properties one expects of quantum evolution, and here they are consequences of the recognition forcing chain rather than assumptions.

What the declaration does not claim is important. It does not claim that the Schrödinger equation is the only possible evolution law, nor that it applies to all physical systems. It establishes the difference equation for this specific eight-dimensional carrier and its DFT-8 basis. The continuum form is recovered in a slow-mode limit, with a bounded remainder, but the theorem itself is about the discrete system. It also does not claim that the energies E_k match any measured spectrum of a real particle; the values are fixed by the framework's constants, but the comparison to experiment is a separate empirical check, not part of this theorem.

/-- **DIFFERENCE FORM.** The one-tick increment on an eigenmode equals
    the integrated Schrödinger phase shift acting on the starting
    state. -/
theorem schrodinger_difference_eigenmode (k : Fin 8) (c : ℂ) :
    cyclic_shift (c • dft8_mode k) - (c • dft8_mode k) =
      (Complex.exp (-Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ)) - 1)
        • (c • dft8_mode k) := by
  rw [discrete_schrodinger_eigenmode k c]
  rw [sub_smul, one_smul]

/-- **DIFFERENCE FORM.** The one-tick increment on an eigenmode equals
    the integrated Schrödinger phase shift acting on the starting
    state. -/
theorem schrodinger_difference_eigenmode (k : Fin 8) (c : ℂ) :
    cyclic_shift (c • dft8_mode k) - (c • dft8_mode k) =
      (Complex.exp (-Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ)) - 1)
        • (c • dft8_mode k) := by
  rw [discrete_schrodinger_eigenmode k c]
  rw [sub_smul, one_smul]

/-- **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 _)

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

What this page does not claim

The theorem does not claim that the Schrödinger equation is the only possible evolution law. The theorem does not claim that the energies E_k match any measured spectrum of a real particle. The theorem does not claim that the continuum form is exact for all modes; it holds only in the slow-mode limit with a bounded remainder.

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: