pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Syndrome

show as:
view Lean formalization →

Syndrome records the boolean measurement outcomes that identify which error occurred in an 8-tick redundant encoding. Workers constructing fault-tolerant codes from Recognition Science phase structure cite it when building toric or surface codes. The declaration is a plain structure with a list of bits and a uniqueness flag defaulting to true.

claimA syndrome is a list of boolean bits together with a boolean flag (default true) that asserts distinct errors produce distinct measurement outcomes.

background

The module derives quantum error correction from the eight-tick octave, where the eight phases supply natural redundancy so that phase-shift errors can be detected by syndrome measurements without revealing logical information. Upstream, the module imports the active-edge count A from IntegrationGap, Masses.Anchor, and Modal.Actualization; these fix the per-tick coherence unit and the actualization operator that selects the realized configuration after each tick. The PeriodicTable.Block type is also imported to label chemical packing offsets that later anchor mass ladders in the same framework.

proof idea

The declaration is a structure definition that directly introduces the two fields bits and unique; no lemmas or tactics are applied.

why it matters in Recognition Science

Syndrome supplies the data type used by the downstream toricCode definition, which states that qubits lie on torus edges and logical information resides in homology classes. It realizes the module's core claim that 8-tick redundancy produces error syndromes from phase measurements, directly supporting the patent note for novel QEC codes based on Recognition Science. The structure therefore bridges the T7 eight-tick foundation to concrete error-correction bounds.

scope and limits

formal statement (Lean)

 100structure Syndrome where
 101  /-- Syndrome bits -/
 102  bits : List Bool
 103  /-- Syndrome uniquely identifies error -/
 104  unique : Bool := true

proof body

Definition body.

 105
 106/-! ## Classical Code Foundation -/
 107
 108/-- A classical linear code [n, k, d].
 109    - n: Block length
 110    - k: Message length
 111    - d: Minimum distance (corrects ⌊(d-1)/2⌋ errors) -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.