EightTickCode
plain-language theorem explainer
The EightTickCode structure defines a quantum error-correcting code that encodes logical qubits via the eight-phase periodicity of the Recognition Science time quantum. Researchers modeling fault-tolerant computation in discrete spacetime would cite it to link phase redundancy directly to syndrome detection. The definition is a direct structure declaration that introduces qubit counts and an 8-tick flag with a derived rate.
Claim. An eight-tick code is a structure consisting of natural numbers $n_ {physical}$ (number of physical qubits) and $n_{logical}$ (number of logical qubits) together with a boolean flag that is true when the encoding uses the eight-tick phase structure.
background
Recognition Science takes the tick as the fundamental time quantum, with one octave equal to eight ticks. The eight phases are defined by $kπ/4$ for $k=0,…,7$. The module derives quantum error correction from this 8-tick redundancy: physical qubits sit in phase patterns, an error shifts the pattern, and a syndrome measurement identifies the shift without revealing the logical information.
proof idea
The declaration is a direct structure definition. It introduces the three fields n_physical, n_logical and uses_8tick (default true), then computes the rate as the rational quotient of logical to physical qubits. No lemmas or tactics are invoked.
why it matters
This supplies the type for the concrete eight-tick logical code that places one logical qubit in eight physical qubits using even phases. It realizes the eight-tick octave as a source of natural redundancy for error correction and feeds the information-theoretic phase-space construction in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.