head
plain-language theorem explainer
The definition head extracts the initial element of a chain over recognition structure M by indexing its underlying function at position zero. Chain flux and conservation statements in the module cite it when forming differences along sequences. The implementation is a direct one-line construction that witnesses positivity of the length index and applies the chain function.
Claim. For a chain $ch$ over recognition structure $M$, the head is $ch.f(0)$ where the index is witnessed by the positivity proof $0 < ch.n + 1$.
background
The Chain module works with Ledger M and RecognitionStructure M, where M.U is the set of recognition units equipped with the native RS gauge (tau0 = 1 tick, ell0 = 1 voxel, c = 1). A chain is a finite sequence of such units; its length parameter n and function f : Fin (n+1) -> M.U are the data used by head. Upstream Recognition.head supplies the identical accessor pattern, while Cycle3.M gives a concrete three-cycle instance of the same structure. The module doc describes the setting as a minimal stub sufficient for standalone compilation of chain properties.
proof idea
One-line wrapper that applies Nat.succ_pos to obtain the positivity witness for index zero, then feeds the indexed element directly to ch.f.
why it matters
head is the starting point for chainFlux, which subtracts phi values to produce an integer difference; that difference is the subject of the Conserves class and the T3_continuity theorem. The accessor therefore sits at the base of atomicity and continuity statements (T2 and T3) that feed the larger forcing chain. It touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.