Pith. sign in
module module moderate

IndisputableMonolith.Information.Quantum_Error_Rate_RS

show as:
view Lean formalization →

Defines the Recognition Science quantum-error-rate package: a domain cost built from the J-cost, a canonical positive threshold, and an exact RS QEC-threshold statement with an inhabited certificate. Information theorists and RS auditors cite it when converting abstract cost bounds into a concrete error-rate cutoff. The module is mostly definitional, with short nonnegativity and positivity lemmas and a certificate wrapper.

claimIn RS units, a domain cost $C$ is built from the J-cost on positive reals; it is nonnegative and agrees with its pointwise evaluation. A canonical threshold $\theta>0$ is fixed, and the exact RS quantum-error-correction threshold asserts that error rates below $\theta$ are admissible, witnessed by an inhabited certificate.

background

Recognition Science measures mismatch with the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain. The Cost import supplies that functional; Constants supplies the RS tick $\tau_0=1$ and the native unit system ($c=1$, $\hbar=\varphi^{-5}$, etc.).

This module sits in the Information domain. It packages a domain-level cost (aggregated J-cost on a positive scale), records that the cost is nonnegative and matches its point evaluation, and introduces a canonical positive threshold used as the RS quantum-error cutoff. The main named claim is the exact RS QEC threshold, accompanied by a certificate type that is inhabited.

No external physical noise model is assumed beyond the RS cost calculus; the threshold is an internal RS quantity, not a device-specific fidelity number.

proof idea

Definition-heavy module. Domain cost is introduced as a Cost-derived quantity; equality-at-evaluation and nonnegativity are short lemmas from the J-cost's known properties. The canonical threshold is a positive constant (positivity lemma). The exact RS QEC-threshold statement packages the cost-threshold comparison; the certificate is a Prop/structure with an inhabitation proof, so downstream code can discharge 'threshold met' by producing cert rather than replaying the cost algebra.

why it matters in Recognition Science

Gives the Information layer a single place for the RS quantum-error cutoff: cost, threshold, exact threshold claim, and certificate. Downstream work that needs a hard error-rate bound in RS units (rather than a floating phenomenological rate) is meant to import this package. It does not yet appear in the supplied used-by graph, so it is a leaf interface for later QEC or channel-capacity arguments.

In the broader framework it ties the T5 J-uniqueness cost to an operational information bound, parallel to how mass and coupling constants sit on the $\varphi$-ladder. It does not itself force $D=3$ or the eight-tick octave; those remain upstream in the forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)