last
plain-language theorem explainer
last selects the terminal unit from a finite recognition chain by direct indexing into its sequence map. Flux and conservation lemmas cite it to evaluate differences across closed cycles. The implementation constructs a successor Fin index via the length inequality and applies the chain map.
Claim. For a chain $ch : Chain(M)$, the terminal unit is $ch.f ⟨ch.n, ch.n < ch.n + 1⟩$, where $M$ is the recognition structure with unit type $U$ and recognition relation $R$ given by structural equality.
background
The Recognition module implements T1 (MP): Nothing cannot recognize itself. RecognitionStructure pairs a unit type $U$ (the trivial type with structural equality) and a recognition relation $R$. Chain packages a length $n$, a map $f : Fin(n+1) → U$, and the adjacency condition that consecutive units satisfy $R$ (from the upstream Chain structure with minimal axioms for standalone compilation).
proof idea
The definition introduces the inequality $hlt : ch.n < ch.n + 1$ by Nat.lt_succ_self, then returns the image of $ch.f$ at the Fin index built from $ch.n$ and $hlt$.
why it matters
last supplies the endpoint for chainFlux (phi difference) and the Conserves class that enforces zero flux on closed chains, thereby supporting T2 Atomicity and T3 continuity. It is invoked in reversal involution and eight-tick periodicity lemmas, completing the basic operations required after T1 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.