FaultToleranceThreshold
plain-language theorem explainer
FaultToleranceThreshold packages the critical positive real for defect density in Recognition Science thermodynamics. Ledger stability analyses cite it when bounding accumulation against correction rates inside the eight-tick cycle. The declaration is a structure definition that introduces the threshold value together with its positivity witness.
Claim. A fault tolerance threshold is a positive real number $tau > 0$ such that defect densities below $tau$ permit correction dynamics to outpace accumulation in the recognition ledger.
background
The module frames error correction as the ledger mechanism that keeps physical laws stable. Recognition defects are deviations from the J=0 ground state; the defect functional equals J(x) for positive x and vanishes at unity. Defect energy, error syndromes, and correction dynamics are defined relative to the eight-tick cycle and the phi-ladder code distance that supplies stabilizer constraints.
proof idea
Structure definition. It declares the field threshold : real together with the witness threshold_pos : 0 < threshold. No lemmas or tactics are applied; the structure is used directly as a parameter in downstream predicates such as is_fault_tolerant.
why it matters
The definition supplies the threshold parameter to is_fault_tolerant, which states that expected cost below the threshold implies existence of a CorrectionProtocol. It completes the error-correction viewpoint of RS thermodynamics, linking the ledger to stabilizer codes, the eight-tick octave, and phi-ladder distance. The construction sits between the defect functional and the bounded-accumulation claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.