pith. machine review for the scientific record. sign in
def definition def or abbrev high

net

show as:
view Lean formalization →

The net definition computes the integer difference between debit and credit for a state under a given ledger constraint in the RRF strain module. Researchers modeling recognition balance or ledger conservation cite this when checking closure conditions in discrete systems. The implementation is a direct subtraction of the two component functions from the ledger constraint record.

claimFor a ledger constraint $L$ on a state space and a state $x$, the net balance is defined by $net(L,x) := debit_L(x) - credit_L(x)$, where debit and credit are the maps supplied by $L$.

background

Strain in the RRF framework measures deviation from equilibrium, with the governing law that strain approaches zero as the J-cost functional approaches zero. This module supplies abstract interfaces for computing such strain measures on discrete states drawn from fluid and vorticity models. A ledger constraint supplies two maps from states to integers: one for total debits and one for total credits. The net balance for a particular state is their difference. This construction extends ledger concepts from the foundation layer, where net is instead the sum of total debit and total credit.

proof idea

The definition is implemented directly as the subtraction of the credit map applied to the state from the debit map applied to the state, using the two fields of the ledger constraint structure.

why it matters in Recognition Science

This definition underpins conservation verification in graded ledger structures and octave loop constructions used in coherence technology and photobiomodulation patterns. It supports derivations in cosmology for matter-antimatter balance and in CPM law of existence for projection constants. The requirement that net balance equals zero for closed ledgers aligns with the strain law that J tends to zero, closing the loop on recognition equilibrium.

scope and limits

formal statement (Lean)

  90def net (L : LedgerConstraint State) (x : State) : ℤ :=

proof body

Definition body.

  91  L.debit x - L.credit x
  92

used by (36)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 6 more

depends on (6)

Lean names referenced from this declaration's body.