module module

`IndisputableMonolith.Foundation.SchrodingerDerivation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.UnifiedForcingChain module_import
IndisputableMonolith.Gravity.LedgerSuperposition module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Spectral.DFT8 module_import

declarations in this module (22)

abbrev Signal8 L64
theorem eigenmode_evolution_exact L71
theorem cyclic_shift_smul L76
theorem cyclic_shift_add L82
theorem eigenmode_evolution_scaled L89
def quarterTurnEnergy L101
theorem quarterTurnEnergy_real L105
theorem quarterTurnEnergy_nonneg L110
theorem quarterTurnEnergy_zero L122
theorem quarterTurnEnergy_pos L126
theorem omega8_pow_eq_evolution_factor L142
theorem discrete_schrodinger_eigenmode L163
theorem schrodinger_difference_eigenmode L173
theorem eigenmode_norm_preserved L181
theorem schrodinger_linear L195
theorem schrodinger_dft_decomposition L202
lemma exp_taylor_remainder L224
theorem schrodinger_remainder_bound L236
structure SchrodingerEquationCert L250
def schrodingerEquationCert L280
theorem schrodingerEquationCert_inhabited L289
theorem schrodinger_equation_from_RS L307