quadratic1DOctave
Defines the 1D quadratic octave as an Octave instance whose state space is the real line, whose strain functional is the quadratic strain, and whose single channel uses identity observation with quadratic quality. Researchers modeling continuous optimization inside RRF would cite this concrete example when testing minimizer theorems. The definition is a direct record construction that assembles the four fields from sibling definitions quadratic1DStrain and quadratic1DChannel.
claimThe 1D quadratic octave is the structure with state space $State = ℝ$, strain functional $J(x) = x^2$, channels indexed by the unit type with observation map the identity and quality map $x ↦ x^2$, and inhabited element $0$.
background
The Octave structure supplies an abstract state space together with a strain functional (the J-cost) and a collection of observation channels; its definition carries no physical constants such as φ or the eight-tick period. In the quadratic model the state space is the real line and the strain is the square norm, providing a testing ground for continuous optimization as stated in the module documentation. Upstream results supply the concrete components: quadratic1DStrain for the strain field and quadratic1DChannel for the display channel.
proof idea
Direct record construction: the State field is set to ℝ, the strain field is assigned quadratic1DStrain, the channels field is built from a Unit-indexed record whose channel map returns quadratic1DChannel, and the inhabited field is the constant 0.
why it matters in Recognition Science
This definition supplies the basic continuous model that feeds the well-posedness theorem quadratic1DOctave_wellPosed. It demonstrates that RRF structures can represent continuous optimization problems and serves as a minimal test case before the phi-ladder or eight-tick octave hypotheses are added. The construction therefore closes the scaffolding gap between the abstract Octave interface and concrete minimizer statements.
scope and limits
- Does not incorporate physical constants φ or the eight-tick octave.
- Does not prove well-posedness or uniqueness of equilibria.
- Does not extend to higher-dimensional or discrete state spaces.
- Does not reference the Recognition Composition Law or the forcing chain T0–T8.
Lean usage
theorem example : quadratic1DOctave.wellPosed := quadratic1DOctave_wellPosedformal statement (Lean)
78def quadratic1DOctave : Octave where
79 State := ℝ
proof body
Definition body.
80 strain := quadratic1DStrain
81 channels := {
82 Index := Unit
83 Obs := fun _ => ℝ
84 channel := fun _ => quadratic1DChannel
85 }
86 inhabited := ⟨0⟩
87