Foundation Schrodinger Derivation

The derivation

The Schrödinger equation, written iħ ∂ψ/∂t = Ĥψ, is the central rule of quantum mechanics. It says that the way a quantum state ψ changes over time is governed by a mathematical operator Ĥ, the Hamiltonian, which encodes the system's energy. In the standard formulation, this equation is a postulate: it is accepted because it works, not because it follows from something deeper. The Recognition Science framework asks whether that postulate can be derived from a more basic principle.

The framework's answer is that it can, under a specific discrete model. The derivation starts with the framework's own concept of a recognition event, a discrete record of a comparison. The framework forces an eight-tick cycle for these events, meaning time advances in eight distinct steps. This cycle defines a space of possible states, called Signal8, which consists of eight complex numbers, one for each tick. The one-step evolution operator, which moves a state forward by a single tick, is a cyclic shift: it moves each number to the next position in the cycle.

The key move is to find the natural basis for this shift. The framework proves that the discrete Fourier transform on eight points, the DFT-8 basis, is the unique basis that diagonalizes the shift. In this basis, each basis mode is an eigenvector of the shift, meaning it simply gets multiplied by a phase factor. The framework then identifies this phase factor with the standard time-evolution factor exp(-iE_k τ₀/ħ), where E_k is the energy of the mode, τ₀ is the duration of one tick, and ħ is the reduced Planck constant. This identification reads off the energy eigenvalues: E_k = ħπk/(4τ₀), which are real and nonnegative. The one-tick evolution on each mode is then exactly the integrated Schrödinger flow for that energy.

Because the evolution is linear, the result extends from single modes to arbitrary superpositions. The framework's machine-checked library of formal theorems proves that the cyclic shift on any state in Signal8 is the sum of the shifts on its DFT-8 components, each multiplied by its own phase factor. This is the discrete Schrödinger equation. The continuum form, iħ ∂ψ/∂t = Ĥψ, is recovered in the slow-mode limit, where the tick duration τ₀ is small. The framework proves a bound on the Taylor remainder of the phase factor, showing that the approximation error vanishes in this limit.

In Recognition Science, the Schrödinger equation is not an input but an output. The framework models time as a discrete process of recognition events, and the equation emerges as the exact description of how a state evolves over one tick, with the continuum form as a well-controlled limit. This does not replace the standard quantum mechanics, which remains the correct empirical theory; it offers a different starting point, one where the form of the equation is forced by the structure of the recognition cycle.

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

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

/-- **SCHRÖDINGER ON GENERAL STATES.** For `ψ = Σ_k c_k · dft8_mode k`,
    the discrete one-tick evolution acts as
    `ψ(τ₀) = Σ_k exp(-iE_k τ₀/ℏ) · c_k · dft8_mode k`. -/
theorem schrodinger_dft_decomposition (c : Fin 8 → ℂ) :
    cyclic_shift (∑ k, c k • dft8_mode k) =
      ∑ k, Complex.exp (-Complex.I * (quarterTurnEnergy k : ℂ) * (tau0 : ℂ) / (hbar : ℂ))
        • (c k • dft8_mode k) := by
  -- cyclic_shift is linear, so it commutes with finite sums
  have hsum : cyclic_shift (∑ k, c k • dft8_mode k) =
      ∑ k, cyclic_shift (c k • dft8_mode k) := by
    induction (Finset.univ : Finset (Fin 8)) using Finset.induction_on with
    | empty =>
        simp
        funext t
        simp [cyclic_shift]
    | @insert k S hk ih =>
        rw [Finset.sum_insert hk, cyclic_shift_add, ih, Finset.sum_insert hk]
  rw [hsum]
  apply Finset.sum_congr rfl
  intro k _
  exact discrete_schrodinger_eigenmode k (c k)

What this page does not claim

This derivation does not claim that the Schrödinger equation is the only possible evolution law. It does not claim that the framework's discrete model is the physical reality of time. It does not claim that the framework derives the specific Hamiltonian of any real-world 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/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: