detect_vs_correct
The eight-tick code has minimum distance eight, permitting detection of seven errors and correction of three errors per codeword. Information theorists working inside the Recognition Science framework cite this when bounding phase-encoded redundancy. The proof is a one-line wrapper that splits the conjunction and reduces both sides by reflexivity.
claimThe minimum distance $d$ of the eight-tick code satisfies $d-1=7$ and $d-1=7$ with floor division giving correction radius three: $d-1=7$ and $(d-1)/2=3$.
background
The eight-tick code is built on the fundamental time quantum tick equal to one, with one octave defined as exactly eight ticks. This periodicity supplies the natural redundancy used for error correction in the Recognition Science information module. The module treats phase correlations across the octave as the source of the code distance, consistent with the eight-tick structure imported from Foundation.EightTick and Constants.tick.
proof idea
The proof is a one-line wrapper that applies the constructor tactic to split the conjunction and then reduces both equalities by reflexivity.
why it matters in Recognition Science
This supplies the concrete distance parameters that justify the rate bound R ≤ 7/8 and the majority-voting threshold p < 3/8 listed in the module comment. It closes the verification step linking the eight-tick octave (T7) to classical coding bounds inside the Recognition Science derivation of information capacity.
scope and limits
- Does not construct or prove existence of the eight-tick code.
- Does not establish optimality of distance eight.
- Does not derive Shannon capacity or channel coding theorems.
- Does not address quantum error-correction variants listed in the module.
formal statement (Lean)
185theorem detect_vs_correct :
186 (eightTickCode.d - 1 = 7) ∧ ((eightTickCode.d - 1) / 2 = 3) := by
proof body
Term-mode proof.
187 constructor <;> rfl
188
189/-! ## Bounds from 8-Tick -/
190
191/-- The 8-tick structure implies natural bounds:
192
193 **Rate bound**: R ≤ 7/8 for single-error correction
194 (Need 1 redundant bit per 8 for parity)
195
196 **Error bound**: p < 3/8 = 37.5% for majority voting
197 (Need majority of 8 to be correct)
198
199 These match classical coding theory! -/