LedgerConstraint
plain-language theorem explainer
The structure equips any state type with integer-valued debit and credit functions. RRF strain modelers cite it to formalize double-entry balance before defining net and closure properties. As a structure definition it carries no proof.
Claim. For a state space $S$, the structure consists of two functions $debit : S → ℤ$ and $credit : S → ℤ$ representing total debits and credits respectively.
background
Strain measures deviation from equilibrium in the RRF framework, with the law that strain approaches zero corresponding to J approaching zero. The module supplies abstract interfaces for strain functionals and balance conditions on states.
proof idea
This is a structure definition introducing the fields debit and credit with no further computation or lemmas.
why it matters
It is used to construct StrainLedger combining strain and ledger evaluation. Downstream results include the equivalence closed_iff_net_zero and the definitions of isClosed and net. This supports the recognition principle that balanced states minimize strain, aligning with equilibrium requirements in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.