Pith. sign in
module module high

IndisputableMonolith.Information.QuantumErrorCorrectionThreshold

show as:
view Lean formalization →

The module defines the quantum error correction threshold at each rung k of the phi-ladder and shows the value lies below unity, decreasing at higher rungs. Researchers analyzing error rates in Recognition Science information models would cite these definitions. The module supplies the core function together with positivity and ratio lemmas derived from the phi-ladder structure.

claimThe quantum error correction threshold at $\phi$-ladder rung $k$ satisfies $\mathrm{qecThresholdAt}(k)<1$, with the threshold decreasing as rung index increases.

background

The module resides in the Information domain and imports the RS time quantum $\tau_0=1$ tick from Constants. It centers on the phi-ladder, the discrete scaling sequence generated by the self-similar fixed point phi from the forcing chain. Core objects include the threshold function qecThresholdAt(k), its positivity lemma, adjacent-ratio lemma, and the certification type QECThresholdCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies threshold values that support error-correction analysis within the Recognition Science information layer. It connects directly to the phi-ladder construction arising from T5 J-uniqueness and T6 phi fixed point in the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)