quadratic1D_ledger_closed
plain-language theorem explainer
The quadratic 1D ledger constraint holds as closed for any real-valued state. Researchers modeling continuous optimization within Recognition Science's RRF framework cite this result to confirm the trivial ledger satisfies the balance condition. The proof is a direct term application of reflexivity to the zero-valued debit and credit functions.
Claim. For every real number $x$, the ledger constraint with debit and credit both equal to the zero function satisfies debit($x$) = credit($x$).
background
The quadratic model sets the state space to the reals and uses the squared Euclidean norm as the cost function. This provides a setting for studying minimizers and optimization in RRF structures. A LedgerConstraint consists of debit and credit maps. The isClosed predicate requires that debit equals credit at a given state, as stated in the definition: 'A state satisfies the ledger constraint if debit = credit.' The specific quadratic1DLedger instance sets both maps to the constant zero function on the reals, rendering the constraint trivially satisfied for all states.
proof idea
This theorem is proved by a term-mode reflexivity tactic (rfl). The equality debit x = credit x holds definitionally because quadratic1DLedger defines both components as the zero function.
why it matters
It is invoked in the quadratic1D_zero_valid theorem to establish that zero is the unique valid state under the combined strain and ledger conditions. This closes the ledger part of the quadratic model, which the module describes as a testing ground for theorems about minimizers in continuous optimization settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.