code_distance
plain-language theorem explainer
code_distance defines the infimum of J-cost over configurations with positive cost for a map X from Ω to reals. Researchers analyzing fault tolerance in Recognition Science thermodynamics cite it when bounding error thresholds via the φ-ladder. The definition is realized directly as an infimum over the positive-cost subtype.
Claim. For a map $X : Ω → ℝ$, the code distance is $∧{ω : {ω : Ω // J(X(ω)) > 0}} J(X(ω))$, the infimum of J-cost over all states with strictly positive cost.
background
The module develops the error-correction viewpoint of RS thermodynamics, where physical laws remain stable because ledger dynamics implements fault tolerance. Recognition defects are deviations from the J=0 ground state; defect energy is the cost to create such a deviation; error syndromes are detectable signatures; and correction dynamics return the system to equilibrium. The 8-tick cycle supplies the error-correction period while the φ-ladder supplies the code distance.
proof idea
The definition is a direct infimum over the subtype of configurations where Jcost exceeds zero. It imports the Jcost function from ObserverForcing.cost and MultiplicativeRecognizerL4.cost without further lemmas or tactics.
why it matters
This definition supplies the minimum non-trivial error cost that characterizes the φ-ladder structure, with the accompanying comment identifying d_φ = J(φ) ≈ 0.118. It completes the link between Recognition Science ledger dynamics and quantum error correction concepts such as stabilizer codes and fault-tolerance thresholds. No downstream theorems yet depend on it, leaving open its integration with CorrectionProtocol or is_fault_tolerant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.