def
definition
H_HamiltonianIsGenerator
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.HamiltonianEmergence on GitHub at line 152.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
DiscreteEvolution -
quadraticEnergy -
SmallDeviationState -
totalJcost -
totalJcost -
is -
of -
is -
of -
is -
of -
is -
totalJcost
used by
formal source
149 - Show U_Δ is approximately unitary: ‖U_Δ ψ‖² = ‖ψ‖² + O(ε³)
150 - Apply discrete Stone: generator of {U_Δ^n} is self-adjoint
151 - Identify generator with diagonalHamiltonian (from J''(1) = 1) -/
152def H_HamiltonianIsGenerator (N : ℕ) : Prop :=
153 ∃ (ev : DiscreteEvolution N),
154 ∀ (s : SmallDeviationState N),
155 |totalJcost s - quadraticEnergy s| ≤
156 2 * Finset.univ.sum fun i => |s.deviations i| ^ 3
157
158/-- The scalar part of the emergence hypothesis is already proved. -/
159theorem emergence_scalar_proved (N : ℕ) :
160 H_HamiltonianIsGenerator N :=
161 ⟨diagonalHamiltonian N, totalJcost_approx_quadratic⟩
162
163end
164
165end IndisputableMonolith.Foundation.HamiltonianEmergence