is_protected_observable
plain-language theorem explainer
An observable O is protected under correction protocol C for field X when its value is invariant after correction on all zero J-cost states. Researchers modeling fault-tolerant thermodynamics in Recognition Science cite this definition to establish stability of conserved quantities. The definition directly encodes the commutation condition as a universal property over states.
Claim. An observable $O : Ω → ℝ$ is protected under a correction protocol $C$ for field $X$ when $∀ ω, O(C(ω)) = O(ω)$ or the J-cost of $X(ω)$ is positive.
background
The module frames Recognition Science thermodynamics through error correction: recognition defects are deviations from the J=0 ground state, defect energy is the positive J-cost, and correction dynamics return the system to equilibrium. CorrectionProtocol is the structure supplying a map correct : Ω → Ω that is cost-decreasing and fixes ground states. The eight-tick cycle supplies the correction period while the phi-ladder supplies code distance. Upstream, the phi-ladder lattice hypothesis structure provides the Poisson summation tool that downstream results may discharge.
proof idea
This is a direct definition encoding the protection condition as the universal statement that the observable is unchanged after correction or the state carries positive J-cost. No lemmas or tactics are invoked; the body is the literal predicate used by the downstream conservation theorem.
why it matters
The definition supplies the target predicate for the theorem that conservation laws are protected observables, confirming that quantities conserved in the J=0 sector remain stable. It realizes the error-correction viewpoint of the thermodynamics module, connecting ledger dynamics to fault tolerance via the eight-tick cycle and phi-ladder code distance. It touches the open question of discharging the phi-ladder Poisson summation hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.