phi
plain-language theorem explainer
The definition phi extracts the net balance on a ledger by subtracting credit from debit for each unit in the carrier of a recognition structure. Researchers tracking recognition events or ledger imbalances in discrete models would reference this when computing net counts. It is realized as a direct functional abbreviation with no lemmas or reductions applied.
Claim. For a recognition structure $M$ and ledger $L$ on $M$, the map $phi(L)$ sends each element $u$ of the carrier $M.U$ to the integer $L.debit(u) - L.credit(u)$.
background
Recognition structures pair a carrier type U with a recognition relation R. The Ledger structure supplies debit and credit maps from that carrier to the integers, supporting an accounting of recognition events. The module opens with the T1 principle that nothing can recognize itself. Upstream, the RSNativeUnits.U supplies the RS-native gauge: τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1. Concrete siblings define M with unit carrier and L with constant debit and credit equal to 1.
proof idea
This is a one-line definition that directly subtracts the credit map from the debit map on the supplied ledger for each carrier element u.
why it matters
The definition supplies the basic net-count operation for ledgers inside the Recognition module and thereby supports the T1 (MP) principle. It aligns with the forcing chain by furnishing a concrete imbalance measure that can feed later steps toward J-uniqueness and self-similar fixed points. No downstream theorems are recorded yet, so its precise role in conservation or cycle proofs remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.