pith. machine review for the scientific record. sign in
def definition def or abbrev high

head

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  20def head : M.U := by

proof body

Definition body.

  21  have hpos : 0 < ch.n + 1 := Nat.succ_pos _
  22  exact ch.f ⟨0, hpos⟩
  23

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.