Foundation Schrodinger Derivation Schrodinger Equation Cert Inhabited

The certification

The Schrödinger equation, iħ∂ψ/∂t = Ĥψ, is the central equation of non-relativistic quantum mechanics. It describes how a quantum system's wavefunction, a mathematical object encoding the probabilities of its possible states, changes over time. The equation is named after Erwin Schrödinger, who published it in 1926, and it forms the basis for most of atomic and molecular physics. Its standard derivation starts from classical wave mechanics and applies a quantization rule, a procedure that is physically motivated but not itself derived from deeper principles.

Within the Recognition Science framework, the equation is not assumed but rather emerges from a more basic structure. The framework models reality as a discrete ledger, a record of events that changes in fixed steps. From this starting point, a forcing chain of theorems establishes an eight-tick recognition cycle, a fundamental period of eight steps. This cycle defines a finite state space, called Signal8, consisting of eight complex numbers. The single-step evolution of this system is a cyclic shift, moving each value to the next position in the cycle.

The framework's library, a machine-checked collection of formal theorems, proves that this cyclic shift has a unique set of basis modes, the discrete Fourier transform modes. Each mode evolves by picking up a phase factor, a complex number of magnitude one. By identifying this phase factor with the standard quantum mechanical evolution operator, exp(-iEt/ħ), the framework extracts an energy for each mode. These energies are real numbers, making the corresponding Hamiltonian Hermitian, and they are all non-negative. The key result is that the evolution of any state in Signal8 is exactly a linear superposition of these phase-evolved modes, which is precisely the discrete form of Schrödinger's equation.

The declaration schrodingerEquationCert_inhabited is the master certificate for this derivation. It states that the structure SchrodingerEquationCert is inhabited, meaning that all the required components of the derivation exist and are internally consistent. This certificate bundles together the proofs of the eigenmode evolution, the Hermitian property, the energy non-negativity, the superposition principle, and the unitarity of the evolution. It is a single, auditable object that attests to the fact that the discrete Schrödinger equation is a theorem of the framework's axioms, not an additional assumption.

What the certificate does not claim is equally important. The continuum form of the equation, iħ∂ψ/∂t = Ĥψ, is not directly proved. Instead, it is recovered in a slow-mode limit, where the time step τ₀ is small. The framework proves a bound on the error of this approximation, showing that the difference between the discrete evolution and the continuum flow is quadratic in the time step. This means the continuum equation is a derived approximation, valid in a specific limit, not an exact consequence. The certificate also does not claim that the framework's Hamiltonian is the same as any specific physical Hamiltonian, such as that of a hydrogen atom; it establishes the form of the equation, not its specific content for any particular system.

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

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

theorem schrodingerEquationCert_inhabited : Nonempty SchrodingerEquationCert :=
  ⟨schrodingerEquationCert⟩

/-- **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 declaration does not prove the continuum Schrödinger equation exactly, only as a limit with a bounded error. It does not claim the framework's Hamiltonian matches any specific physical system's Hamiltonian. It does not assert that the framework's derivation replaces the standard postulatory introduction of the Schrödinger equation in all contexts.

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: