quadratic1DChannel
plain-language theorem explainer
The quadratic1DChannel supplies a one-dimensional observation channel for the RRF quadratic model, with identity observation and squared state as quality. Researchers building continuous optimization test cases in Recognition Science cite it when constructing strain-based channels for equilibrium analysis. The definition is a direct record instantiation of DisplayChannel with no auxiliary lemmas.
Claim. The one-dimensional quadratic channel is the display channel on the reals whose observation map is the identity and whose quality function is the square map $q(x) = x^2$.
background
The RRF quadratic model takes state space ℝⁿ with cost J(x) = ‖x‖² and supplies a concrete setting for continuous optimization inside Recognition Science. The module documentation states that this demonstrates RRF structures can model such problems and serves as a testing ground for minimizer theorems. DisplayChannel from RRF.Core.Core is the record type that packages an observation map together with a quality (strain) function.
proof idea
Direct record construction: the observe field is set to the identity function and the quality field to the squaring map on ℝ. No lemmas from the upstream list (octave, id, etc.) are invoked; the definition is a one-line wrapper instantiating the DisplayChannel structure.
why it matters
This channel is used by quadratic1DOctave to assemble the full octave structure for the 1D quadratic case. It supplies the concrete observation component required by the quadratic model documentation, which positions the module as a testbed for theorems about minimizers and equilibrium states. Within the Recognition framework it supports the continuous-state side of RRF structures without invoking the phi-ladder or discrete forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.