Foundation Schrodinger Derivation Eigenmode Evolution Scaled

The scaled eigenmode step

The Schrödinger equation is the rule that tells a quantum system how its state changes from one moment to the next. In its standard form it reads iħ ∂ψ/∂t = Ĥψ, where ψ is the wavefunction, ħ is the reduced Planck constant, and Ĥ is the Hamiltonian, the operator that encodes the system's energy. The equation is one of the pillars of modern physics, and its solutions describe everything from electrons in atoms to the behavior of particles in a potential well.

The declaration eigenmode_evolution_scaled is a small, precise step inside a larger framework called Recognition Science, which attempts to derive physical laws from a single principle about how a system keeps a discrete record of its own states. The theorem states that if you take a special solution of the Schrödinger equation, called an eigenmode, and multiply it by any complex number, then one step of time evolution on that scaled eigenmode is exactly the same as scaling the evolved eigenmode. In symbols, cyclic_shift (c • dft8_mode k) = (omega8 ^ k.val) • (c • dft8_mode k). This is a linearity property: the shift operator commutes with scalar multiplication.

In the framework's language, the time evolution is not a continuous flow but a discrete step, represented by an operator called cyclic_shift. The eigenmodes are vectors in an eight-dimensional complex space, and the theorem shows that scaling such a vector by a complex number c before applying the shift gives the same result as applying the shift first and then scaling. The proof is short and relies on two earlier facts: that the shift is linear over scalar multiplication, and that each eigenmode is an eigenvector of the shift with a specific phase factor. The declaration is tagged as a THEOREM, meaning it is proved in the machine-checked library of formal theorems with no unproved assumptions.

The theorem does not claim that the Schrödinger equation itself is derived in this step. It is a lemma that supports a later, larger result, which assembles the full discrete Schrödinger flow, including Hermiticity of the Hamiltonian, nonnegative energy, and the superposition principle. It also does not claim that the continuum limit of the equation is reached here; that requires a separate Taylor expansion argument. The theorem is about a single mode with a fixed scaling, not about arbitrary superpositions of modes, which is a separate linearity result.

In plain terms, the declaration establishes that the evolution operator respects the scaling of a single eigenmode, a necessary consistency condition for any linear quantum theory. It is a building block, not the whole edifice. The reader should see it as one verified step in a chain that aims to reconstruct quantum mechanics from a discrete recognition principle, with the full derivation and its limits documented elsewhere.

/-- Linearity: the one-tick evolution acts on `c • dft8_mode k`
    by the same eigenvalue. -/
theorem eigenmode_evolution_scaled (k : Fin 8) (c : ℂ) :
    cyclic_shift (c • dft8_mode k) = (omega8 ^ k.val) • (c • dft8_mode k) := by
  rw [cyclic_shift_smul, eigenmode_evolution_exact, smul_comm]

/-- `cyclic_shift` is `ℂ`-linear under scalar multiplication. -/
theorem cyclic_shift_smul (c : ℂ) (v : Fin 8 → ℂ) :
    cyclic_shift (c • v) = c • cyclic_shift v := by
  funext t
  simp [cyclic_shift, Pi.smul_apply]

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

/-- Linearity: the one-tick evolution acts on `c • dft8_mode k`
    by the same eigenvalue. -/
theorem eigenmode_evolution_scaled (k : Fin 8) (c : ℂ) :
    cyclic_shift (c • dft8_mode k) = (omega8 ^ k.val) • (c • dft8_mode k) := by
  rw [cyclic_shift_smul, eigenmode_evolution_exact, smul_comm]

What this page does not claim

This declaration does not derive the full Schrödinger equation. This declaration does not establish the continuum limit of the evolution. This declaration does not cover superpositions of different eigenmodes.

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: