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

qecThresholdCert

show as:
view Lean formalization →

The definition assembles the QEC threshold certificate by packaging positivity and exact phi-inverse ratio properties of the threshold function on the phi-ladder. Researchers modeling fault-tolerant quantum computation would cite it to embed empirical thresholds (surface code near rung 9, colour code near rung 8) into the Recognition Science structure. It is a one-line wrapper that instantiates the required structure fields from three local theorems.

claimThe QEC threshold certificate asserts that for every natural number $k$ the threshold value at rung $k$ is positive, the threshold at rung $k+1$ equals the threshold at rung $k$ multiplied by $phi^{-1}$, and the ratio of thresholds at adjacent rungs equals $phi^{-1}$.

background

The module defines the threshold function on the phi-ladder and supplies the certificate structure QECThresholdCert whose fields are positivity for all rungs, one-step multiplicative decay by $phi^{-1}$, and adjacent ratio exactly $phi^{-1}$. The local setting states that the quantum error correction fault-tolerance threshold sits on the phi-ladder with adjacent-code-family thresholds rationing by exactly phi, matching empirical values such as surface code threshold approximately 1 percent at rung 9 and colour code approximately 1.7 percent at rung 8. Upstream results supply the supporting theorems that establish positivity via zpow positivity and the two ratio identities via algebraic simplification of the exponent.

proof idea

The definition is a one-line wrapper that instantiates the QECThresholdCert structure by direct assignment of its three fields to the theorems qecThresholdAt_pos, qecThresholdAt_succ_ratio, and qecThresholdAt_adjacent_ratio.

why it matters in Recognition Science

This certificate supplies the core positivity and ratio properties required by the downstream QECThresholdCert in QECThresholdFromPhiLadder, which augments the structure with the fixed count of five code families. It realizes the module claim that adjacent thresholds ratio by exactly phi, aligning with the phi-ladder structure forced by the T5 J-uniqueness and T6 self-similar fixed point in the unified forcing chain. The declaration closes the local information-domain scaffolding for the QEC prediction with no remaining open questions.

scope and limits

formal statement (Lean)

  60def qecThresholdCert : QECThresholdCert where
  61  threshold_pos := qecThresholdAt_pos

proof body

Definition body.

  62  one_step_ratio := qecThresholdAt_succ_ratio
  63  adjacent_ratio := qecThresholdAt_adjacent_ratio
  64
  65end
  66end QuantumErrorCorrectionThreshold
  67end Information
  68end IndisputableMonolith

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.