phi
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.