chainFlux
Chain flux computes the integer difference in phi valuation between the terminal and initial elements of a recognition chain on a given ledger. Researchers establishing conservation laws or zero-flux lemmas in the RRF core cite this definition when handling closed chains. The implementation is a one-line re-export that delegates directly to the base Recognition.chainFlux computation.
claimLet $M$ be a recognition structure, $L$ a ledger on $M$, and $ch$ a chain in $M$. The chain flux is defined as $phi(L, last(ch)) - phi(L, head(ch))$, where $phi$ is the valuation map on the ledger.
background
The RRF.Core.Recognition module re-exports core concepts from the base Recognition library. A RecognitionStructure consists of a type U equipped with a binary recognition relation R. A Chain is a finite sequence of elements in U connected by successive recognitions, given as a structure carrying length n, a map from Fin(n+1) to U, and proofs that each consecutive pair satisfies the relation R. A Ledger supplies double-entry bookkeeping for recognition events.
proof idea
This is a one-line wrapper that applies the base chainFlux definition from the Recognition module.
why it matters in Recognition Science
This definition supplies the flux operation required by the Conserves class and the T3_continuity theorem, which establish zero flux for closed chains (head equal to last) under conservation. It bridges the original Recognition framework to the RRF re-export layer, supporting atomicity and continuity results. Parent results include chainFlux_zero_of_loop and chainFlux_zero_of_balanced, which derive zero flux from loop or balance conditions.
scope and limits
- Does not define the phi valuation function itself.
- Does not enforce any conservation property on the ledger.
- Does not restrict the length or internal structure of the input chain.
- Does not convert the integer result into physical units.
formal statement (Lean)
54def chainFlux {M : RecognitionStructure} (L : Recognition.Ledger M) (ch : Recognition.Chain M) : ℤ :=
proof body
Definition body.
55 Recognition.chainFlux L ch
56
57/-- Re-export: Atomic tick class. -/