pith. sign in
module module high

IndisputableMonolith.Physics.QuantumErrorCorrectionFromJCost

show as:
view Lean formalization →

This module derives quantum error correction thresholds directly from the J-cost function. It establishes that codes correct errors when J falls below J(φ) while logical errors become positive above threshold. Quantum information researchers would cite it to ground error-correction bounds in the Recognition Science cost structure. The module supplies the necessary type definitions and lemmas that certify below-threshold operation.

claimThe module introduces QECCodeType together with the predicate below_threshold_correct asserting that a code corrects errors whenever its J-cost satisfies $J < J(φ)$. It also defines QECCert as the certificate object witnessing this regime and proves logical_error_positive for $J > J(φ)$.

background

The module imports the Cost module whose J-cost is the unique function satisfying the Recognition Composition Law and the fixed-point condition at φ. It works inside the eight-tick octave setting where spatial dimension D=3 and the Berry threshold is φ^{-1}. The sibling declarations QECCodeType, qecCodeCount, dft8ModeCount and dft8_eq_8 supply the discrete Fourier structure used to count logical modes.

proof idea

This is a definition module. It declares QECCodeType and QECCert, then proves below_threshold_correct and logical_error_positive by direct appeal to the J-cost monotonicity already established in the Cost module. The remaining declarations dft8ModeCount and dft8_eq_8 are one-line equalities that fix the mode count at eight.

why it matters in Recognition Science

The module supplies the quantum-error-correction interface required by the larger Recognition Science derivation of physics from the single functional equation. It connects the J-uniqueness result (T5) to concrete error thresholds and thereby supports the claim that below-threshold operation is forced once J < J(φ). No downstream theorems are listed yet, indicating this block remains an open attachment point for later quantum-information lemmas.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)