Foundation Schrodinger Derivation Schrodinger Remainder Bound

The remainder bound

The Schrödinger equation, iħ ∂ψ/∂t = Ĥψ, is the fundamental law of quantum mechanics, describing how a quantum system's state changes over time. It is a differential equation, meaning it relates a rate of change to the current state. In the Recognition Science framework, this equation is not taken as a starting point but is derived from a more basic structure: a discrete ledger of recognition events, a record of occurrences that changes in steps rather than continuously.

The derivation works on a carrier of eight possible states, called Signal8, where each state is a complex number. A single step in time is modeled by the operator cyclic_shift, which moves the system from one state to the next. The framework proves that this discrete evolution, on each of its eight fundamental modes, is exactly described by the phase factor exp(-iEₖτ₀/ħ), where Eₖ is the energy of mode k, τ₀ is the fundamental time step, and ħ is the reduced Planck constant. This is the exact, discrete version of the Schrödinger flow.

The theorem schrodinger_remainder_bound addresses the transition from this discrete, exact evolution to the familiar continuous differential equation. It proves a bound on the error made when the exponential phase factor is approximated by its first-order Taylor expansion, 1 + z, where z = -iEₖτ₀/ħ. The theorem states that the norm of the difference between the exact evolution and this linear approximation, applied to any mode, is at most the square of the norm of z, multiplied by the norm of the mode itself. In symbols: ‖(exp(z) - 1 - z) · (c · dft8_mode k) t‖ ≤ ‖z‖² · ‖(c · dft8_mode k) t‖.

The significance is that the error is quadratic in the small quantity z. In the slow-mode limit, where z is small, the remainder vanishes, and the discrete evolution recovers the continuous Schrödinger equation. The bound is a rigorous, machine-checked statement about the accuracy of this approximation. It is a theorem in the framework's library, a collection of formal theorems verified by a proof checker, with no unproved assumptions specific to the framework.

The theorem does not claim that the Schrödinger equation is universally valid, nor that it applies to all physical systems. It establishes a specific mathematical relationship within the framework's model, where the system is finite-dimensional with exactly eight states and the time step is fixed. It does not address the empirical question of whether this model accurately describes any particular real-world quantum system, nor does it claim to derive the equation from first principles outside the framework's axioms. The result is a precise statement about the internal consistency of the framework's derivation.

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

/-- Local abbreviation to keep type signatures readable. -/
abbrev Signal8 : Type := Fin 8 → ℂ

/-- The one-tick recognition evolution acts on each DFT-8 mode by
    multiplication by `ω₈^k = exp(-iπk/4)`. This is the spectral
    identity `cyclic_shift = ⊕ ω₈^k · I_{mode k}`. -/
theorem eigenmode_evolution_exact (k : Fin 8) :
    cyclic_shift (dft8_mode k) = (omega8 ^ k.val) • dft8_mode k :=
  dft8_shift_eigenvector k

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

What this page does not claim

The theorem does not claim that the Schrödinger equation is universally valid for all physical systems. It does not claim that the eight-state model accurately describes any particular real-world quantum system. It does not claim to derive the Schrödinger equation from first principles outside the framework's axioms.

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: