pith. machine review for the scientific record. sign in
theorem proved term proof high

eight_tick_corrects_3

show as:
view Lean formalization →

The eight-tick code has minimum distance 7 and therefore corrects up to three errors via the standard relation t = (d-1)/2. Researchers deriving quantum error correction bounds from Recognition Science phase structure would cite this equality when bounding channel capacity. The proof is a direct reflexivity check on the distance parameter already assigned in the code definition.

claimFor the error-correcting code built from the eight-tick phases, the minimum distance $d$ satisfies $(d-1)/2 = 3$.

background

The module derives error correction bounds from the eight-tick structure. The fundamental time quantum is one tick, and the eight phases are defined as $kπ/4$ for $k=0,…,7$, giving the periodic octave that supplies natural redundancy through phase correlations. Upstream results fix the tick as the RS-native time unit and establish the phase function over Fin 8.

proof idea

The proof is a one-line wrapper that applies reflexivity to the pre-defined minimum distance of the eight-tick code.

why it matters in Recognition Science

This equality supplies the concrete distance for the eight-tick code, supporting the module claim that eight-tick phases furnish natural quantum error correction. It sits inside the eight-tick octave step of the forcing chain and connects to quantum channel capacity results that use the same phase structure.

scope and limits

formal statement (Lean)

 123theorem eight_tick_corrects_3 :
 124    -- 8-tick code corrects up to 3 errors
 125    (eightTickCode.d - 1) / 2 = 3 := by rfl

proof body

Term-mode proof.

 126
 127/-! ## Quantum Error Correction -/
 128
 129/-- Quantum error correction is different:
 130
 131    - Can't measure without disturbing
 132    - No cloning
 133    - Errors are continuous (not just bit flips)
 134
 135    Yet QEC is possible! Using entanglement and syndrome measurement.
 136
 137    In RS: 8-tick phases provide natural QEC through phase correlations. -/

depends on (11)

Lean names referenced from this declaration's body.