head
plain-language theorem explainer
The head operator extracts the initial unit from a finite chain in a recognition structure. Researchers establishing flux conservation along cycles cite it when reducing closed-chain differences to zero. The implementation verifies the zeroth index is admissible via the successor property and retrieves the corresponding element from the chain's sequence function.
Claim. Let $M$ be a recognition structure with universe $U$ and recognition relation $R$. For a chain $ch$ of length $n$ in $M$, the head of $ch$ is the element at position zero in the chain's sequence function.
background
A RecognitionStructure pairs a universe $U$ of units with a binary recognition relation $R$ on $U$. Chains are finite sequences in $U$ such that consecutive terms satisfy $R$, with the structure supporting operations like head and last extraction. The module opens with T1, the statement that nothing recognizes itself, which constrains admissible chains and recognition graphs.
proof idea
A positivity lemma establishes $0 < n+1$ from the successor property on natural numbers. The chain's internal sequence function is then applied directly at the zero index to return the head unit. This is a direct index extraction with no further rewriting.
why it matters
The definition supplies the starting point for chainFlux, which subtracts the phi-value at the head from the value at the last element. It is required by the Conserves class and by T3 continuity, which concludes that head-equals-last implies zero flux. In the broader framework it supports T2 atomicity by enabling per-tick uniqueness checks on closed chains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.