theorem
proved
quadratic1D_zero_valid
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Models.Quadratic on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
64 ledger := quadratic1DLedger
65
66/-- Zero is the unique valid state. -/
67theorem quadratic1D_zero_valid : quadratic1DStrainLedger.isValid 0 :=
68 ⟨quadratic1D_equilibrium, quadratic1D_ledger_closed 0⟩
69
70/-! ## Quadratic Octave -/
71
72/-- Observation channel: identity observation, quality = strain. -/
73def quadratic1DChannel : DisplayChannel ℝ ℝ where
74 observe := id
75 quality := fun x => x ^ 2
76
77/-- The 1D quadratic octave. -/
78def quadratic1DOctave : Octave where
79 State := ℝ
80 strain := quadratic1DStrain
81 channels := {
82 Index := Unit
83 Obs := fun _ => ℝ
84 channel := fun _ => quadratic1DChannel
85 }
86 inhabited := ⟨0⟩
87
88theorem quadratic1DOctave_wellPosed : quadratic1DOctave.wellPosed :=
89 ⟨(0 : ℝ), quadratic1D_equilibrium⟩
90
91/-! ## Shifted Quadratic (demonstrates argmin invariance) -/
92
93/-- Shifted quadratic: J(x) = (x - a)² with minimum at a. -/
94def shiftedQuadraticStrain (a : ℝ) : StrainFunctional ℝ where
95 J := fun x => (x - a) ^ 2
96
97instance (a : ℝ) : StrainFunctional.NonNeg (shiftedQuadraticStrain a) where