LogicalOperator
plain-language theorem explainer
LogicalOperator encodes maps on state space that leave the J-cost of a recognition function X unchanged. Error-correction work in Recognition Science cites it when building stabilizer-preserving transformations on the ledger. The structure is a direct definition that packages an operator with a single cost-equality axiom drawn from the cost algebra.
Claim. Let $X : Ω → ℝ$ be a recognition function. A logical operator is a map $op : Ω → Ω$ such that $J_{cost}(X(op(ω))) = J_{cost}(X(ω))$ for every state $ω$.
background
The module develops an error-correction reading of RS thermodynamics. Physical stability arises because ledger dynamics implements fault tolerance, with the ledger acting as a stabilizer code, defects as stabilizer violations, and the eight-tick cycle as the correction period. Recognition defects are deviations from the J=0 ground state; defect energy is the cost of creating such a deviation.
proof idea
This is a structure definition with no proof body. It directly records the operator function together with the cost-preservation condition supplied by CostAlgebra.preserves_cost and the J-cost definition from ObserverForcing.cost.
why it matters
The structure supplies the basic notion of a recognition-preserving map needed for the fault-tolerance model. It is used immediately by id_logical_op to show that the identity qualifies. The definition supports the link between the phi-ladder code distance and the eight-tick octave, reinforcing that stable physical laws follow from ledger-level error correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.