eightTickSyndrome
plain-language theorem explainer
The eightTickSyndrome extracts a boolean list from an 8-phase pattern to represent detected errors in the Recognition Science 8-tick structure. Researchers deriving Hamming or singleton bounds for 8-tick codes cite this when quantifying the natural redundancy supplied by phase correlations. The definition is a direct conversion of a Fin 8 function to List Bool.
Claim. For a phase pattern $p : [8] → {0,1}$, the syndrome is the list $[p(0), p(1), …, p(7)]$.
background
The module INFO-005 derives error-correction bounds from the 8-tick structure. In Recognition Science the 8-tick octave supplies built-in redundancy: each bit is encoded across eight successive phases, and phase correlations allow syndrome-based recovery. The upstream tick definition supplies the fundamental time quantum τ₀ = 1 with the explicit remark that one octave equals eight ticks.
proof idea
One-line wrapper that applies List.ofFn to the input Fin 8 → Bool function, producing the corresponding List Bool.
why it matters
This definition supplies the concrete syndrome map required by the module’s target of deriving fundamental error-correction bounds from 8-tick phases. It directly supports sibling results such as hamming_bound_8tick and eight_tick_corrects_3, and instantiates the RS mechanism in which the eight-tick octave (T7) furnishes natural redundancy for detecting up to seven errors and correcting up to three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.