eightTickLogicalCode
The eightTickLogicalCode supplies the concrete parameters for the 8-tick code structure: eight physical qubits encoding one logical qubit at rate 1/8 with the 8-tick flag set. Quantum information researchers deriving error correction from Recognition Science phase redundancy would cite this as the base encoding instance. The definition is a direct record construction that populates the four fields of the structure without additional lemmas.
claimThe 8-tick logical code is the structure with eight physical qubits, one logical qubit, the 8-tick phase flag enabled, and rate equal to one-eighth.
background
The module derives quantum error correction from the eight-tick redundancy of Recognition Science. The referenced EightTickCode structure records that physical qubits are encoded in 8-tick phase patterns, an error shifts the phase pattern, syndrome measurement detects the shift, and correction restores the original phase. The definition populates this structure with the minimal parameters that realize one logical qubit inside the eight-phase pattern.
proof idea
The definition constructs the EightTickCode record directly by assigning n_physical to 8, n_logical to 1, uses_8tick to true, and rate to 1/8.
why it matters in Recognition Science
This definition realizes the module target of extracting QEC principles from 8-tick redundancy and supplies the base object for any later theorems on syndrome extraction or channel capacity. It instantiates the eight-tick octave (T7) from the forcing chain and aligns with the phi-ladder correction factor supplied by the upstream QuantumChannelCapacityFromPhi result. No downstream uses are recorded, so its role in full distance or threshold proofs remains open.
scope and limits
- Does not specify the explicit encoding states such as even-phase superpositions.
- Does not prove error detection, correction, or code distance.
- Does not connect to concrete quantum channel models or capacity bounds.
- Does not address scalability, thresholds, or lattice embeddings.
formal statement (Lean)
179def eightTickLogicalCode : EightTickCode := {
proof body
Definition body.
180 n_physical := 8,
181 n_logical := 1,
182 uses_8tick := true,
183 rate := 1/8
184}
185
186/-! ## Surface Codes -/
187
188/-- Surface codes are the leading approach for scalable QEC.
189
190 - Qubits on a 2D lattice
191 - Stabilizer measurements on plaquettes
192 - Error correction via matching
193
194 In RS: The 2D structure relates to holographic boundary. -/