pith. sign in
module module high

IndisputableMonolith.Information.QuantumErrorCorrection

show as:
view Lean formalization →

This module defines Pauli-basis error expansions and discrete quantum codes within Recognition Science, anchoring them to the eight-tick cycle. Information theorists modeling fault tolerance in RS-native units would cite it when linking error syndromes to the discrete clock. It consists entirely of definitions and supporting structures imported from Constants and EightTick, with no proofs.

claimQuantum errors expand as $E = α I + β X + γ Y + δ Z$, with $I$ the identity (no error), $X$ the bit-flip, $Y$ the bit-plus-phase flip, and $Z$ the phase flip, all realized inside the eight-tick discrete clock.

background

The module sits in the Information domain and imports the RS time quantum τ₀ = 1 tick together with the eight-tick cycle whose phases are 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. Sibling declarations introduce PauliError, ErrorModel, the depolarizing channel, EightTickCode, Syndrome, repetitionCode3, CSSCode, steaneCode, eightTickLogicalCode and SurfaceCode. The supplied doc-comment states that any error operator admits the Pauli expansion above.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the error-model layer required by the eight-tick octave (T7) and feeds the construction of logical codes that preserve redundancy under the Recognition Composition Law. It directly supports downstream definitions such as eight_tick_encodes_redundancy and eightTickLogicalCode inside the same module.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)