chainFlux
plain-language theorem explainer
chainFlux defines the integer net change along a chain as the difference of the phi valuation at its terminal and initial units. Workers proving conservation laws in the Recognition monolith cite this when establishing zero-flux results for closed paths. The definition is a direct one-line subtraction that invokes the head and last projections on the supplied chain.
Claim. Let $L$ be a ledger on a recognition structure $M$ and let $ch$ be a chain in $M$. The chain flux is defined as $phi(L, last(ch)) - phi(L, head(ch))$.
background
The module supplies a minimal RecognitionStructure stub for standalone compilation. A Chain consists of a finite sequence of units linked by the recognition relation R, together with head and last selectors that extract the first and final units via Fin-indexed access. A Ledger equips each unit with integer debit and credit maps. The phi function, drawn from the Recognition module, returns an integer for each ledger-unit pair and satisfies phi-zero when debit equals credit at every unit.
proof idea
The definition is a one-line wrapper that subtracts the phi value at the chain head from the phi value at the chain last, using the head and last accessors defined in the Chain namespace.
why it matters
This definition supplies the basic telescoping quantity for the Conserves class, which asserts zero flux on any chain with head equal to last, and for the T3_continuity theorem that follows directly from it. It supports the atomicity and continuity steps (T2 and T3) in the unified forcing chain, where path conservation is required before the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.