phi
The definition phi extracts the net integer balance for each unit by subtracting its credit entry from its debit entry in a supplied ledger. Chain module users reference it when tracking recognition imbalances ahead of conservation statements. The construction is a direct one-line functional definition with no auxiliary lemmas.
claimLet $M$ be a recognition structure and $L$ a ledger on $M$. The map $phi_L : U_M to Z$ is given by $phi_L(u) = debit_L(u) - credit_L(u)$.
background
The module supplies a minimal RecognitionStructure stub consisting of a unit set $U$ and a recognition relation $R$. A Ledger is the structure that attaches two maps, debit and credit, each sending units to integers. Upstream results fix the RS-native gauge with one tick as the time unit and one voxel as the length unit, while example ledgers in the Recognition module set constant debit and credit values of 1 or 0.
proof idea
One-line definition that subtracts the credit component from the debit component of the Ledger structure.
why it matters in Recognition Science
The net-balance map supplies the basic defect measure required by conservation and atomicity statements in the Chain module. It aligns with the forcing chain steps that introduce J-uniqueness and the eight-tick octave, and it prepares the ground for the Recognition Composition Law by quantifying recognition defects on the phi-ladder.
scope and limits
- Does not enforce conservation between debit and credit maps.
- Does not specify the recognition relation inside the structure.
- Does not evaluate balances in physical units or continuous time.
- Does not extend the codomain beyond integers.
formal statement (Lean)
38def phi {M} (L : Ledger M) : M.U → ℤ := fun u => L.debit u - L.credit u
proof body
Definition body.
39