is_fault_tolerant
plain-language theorem explainer
A recognition system with observable X is fault-tolerant relative to a threshold if every probability distribution whose expected cost lies below the threshold admits a correction protocol that halves that cost. Researchers modeling thermodynamic stability through error correction in Recognition Science would cite the definition. It is introduced directly as a universal-existential statement over distributions and protocols with no auxiliary lemmas.
Claim. A recognition system with observable $X:Ω→ℝ$ is fault-tolerant relative to a threshold $ft$ when, for every probability distribution $p$ on $Ω$, if the expected cost of $X$ under $p$ is strictly less than the threshold value then there exists a correction protocol $C$ such that the expected cost of $X$ after applying $C$ is strictly less than half the original expected cost.
background
Recognition Science treats physical stability as the consequence of ledger dynamics that bound recognition defects (deviations from the J=0 ground state). The module frames the ledger as a stabilizer code, defects as errors, the eight-tick cycle as the correction period, and the φ-ladder as the source of code distance. FaultToleranceThreshold is the structure whose single field is a positive real number below which errors are corrected faster than they accumulate. Expected cost is the integral of the observable against the distribution, built from the J-cost defined in ObserverForcing and the derived cost of multiplicative recognizers.
proof idea
The declaration is a direct definition of a Prop. It opens with a universal quantifier over ProbabilityDistribution, imposes the strict inequality on expected_cost against the threshold field, and asserts existence of a CorrectionProtocol whose corrected distribution satisfies the halved-cost inequality. No tactics or external lemmas appear; the body simply assembles the already-defined notions of expected_cost, CorrectionProtocol, and ProbabilityDistribution.
why it matters
The definition supplies the central property in the error-correction account of RS thermodynamics, making precise the claim that ledger dynamics implement fault tolerance. It directly encodes the module's link between the eight-tick cycle (T7) and the φ-ladder structure for code distance. Although the current dependency graph records no immediate users, the definition closes the conceptual step from defect energy to bounded accumulation that the module introduction identifies as the reason physical laws remain stable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.