quadratic1DLedger
plain-language theorem explainer
This definition supplies the trivial ledger constraint on the reals for the quadratic RRF model, with both debit and credit identically zero. Researchers constructing combined strain-ledger objects in one dimension cite it to obtain an always-closed ledger. The construction is a direct record instantiation of the LedgerConstraint structure using constant-zero functions.
Claim. The quadratic 1D ledger is the LedgerConstraint on $ℝ$ defined by $debit(x) := 0$ and $credit(x) := 0$ for every $x ∈ ℝ$.
background
In the quadratic model, states are elements of $ℝ^n$ equipped with the cost $J(x) = ‖x‖²$. The LedgerConstraint structure from the core strain module is a record whose two fields are functions State → ℤ; any instance must satisfy that the sum of debits equals the sum of credits for every state. This definition supplies the zero ledger on $ℝ$ that meets the constraint identically.
proof idea
Direct definition that populates the debit and credit fields of LedgerConstraint ℝ with the constant-zero function.
why it matters
The definition is assembled with quadratic1DStrain inside quadratic1DStrainLedger to produce a complete strain-ledger pair. It directly supports the closedness theorem quadratic1D_ledger_closed and the claim that zero is the unique valid state. Within the Recognition Science RRF framework it supplies the minimal always-closed ledger needed to test continuous optimization and minimizer results in one dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.