quadratic1DStrainLedger
plain-language theorem explainer
The declaration defines the combined strain-ledger structure for the one-dimensional quadratic RRF model on real numbers. Researchers testing continuous optimization and equilibrium properties in Recognition Science would cite this instance when verifying zero as the unique valid state. It is assembled by direct field assignment from the quadratic strain functional and the trivial ledger constraint.
Claim. Let $J(x) = |x|^2$ be the quadratic cost on the state space $X = ℝ$. The strain-ledger for the one-dimensional quadratic model is the structure StrainLedger$(ℝ)$ whose strain functional is the quadratic strain map and whose ledger constraint is the zero debit-credit pair.
background
The RRF quadratic model takes state space $ℝ$ with cost $J(x) = ‖x‖²$ to demonstrate continuous optimization and supply a testing ground for minimizer theorems. The StrainLedger structure from the core module assembles a StrainFunctional (the cost evaluator) with a LedgerConstraint (the balance enforcer) into a single object for full RRF state evaluation. The sibling quadratic1DLedger supplies the trivial constraint with debit and credit identically zero.
proof idea
This is a definition that constructs the StrainLedger record by direct assignment of the strain field to quadratic1DStrain and the ledger field to quadratic1DLedger. No lemmas or tactics are invoked beyond the record constructor.
why it matters
This definition supplies the concrete StrainLedger instance required by the downstream quadratic1D_zero_valid theorem, which states that zero is the unique valid state. It realizes the module's purpose of furnishing a testable quadratic model for minimizer properties inside the RRF framework and connects to the Recognition Science forcing chain through the J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.