last
plain-language theorem explainer
last extracts the terminal U-value from a Chain by indexing its function f at position n. Chain-based flux and conservation arguments cite it when forming head-to-last differences. The implementation is a short tactic block that invokes Nat.lt_succ_self to build the required Fin index.
Claim. For a chain $ch$ of length $n$ in recognition structure $M$, last$(ch) := ch.f(n)$ where the index $n$ satisfies $n < n+1$ by the successor property on natural numbers.
background
The Chain structure packages a length $n : Nat$, a map $f : Fin(n+1) → M.U$, and an adjacency condition ok that records recognition steps between consecutive elements. M.U is the carrier of the recognition structure; in the RS-native setting it is the gauge with unit tick and voxel. This minimal version of Chain is supplied so that downstream modules can compile without the full RecognitionStructure axioms.
proof idea
The definition opens a have for the inequality ch.n < ch.n + 1 via Nat.lt_succ_self, then applies exact to ch.f on the constructed Fin index.
why it matters
last supplies the endpoint required by chainFlux and by the Conserves class that forces zero flux on closed chains. It is invoked by T3_continuity and by reversal and periodicity lemmas in Flight and CrossDomain. Within the framework it completes the basic chain vocabulary used for T2 atomicity and for the eight-tick periodicity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.