code_distance
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not specify the concrete space Ω or the map X.
- Does not prove metric properties such as the triangle inequality.
- Does not connect the distance explicitly to the eight-tick cycle.
- Does not compute numerical values for arbitrary codes.
formal statement (Lean)
110noncomputable def code_distance (X : Ω → ℝ) : ℝ :=
proof body
Definition body.
111 ⨅ ω : { ω : Ω // Jcost (X ω) > 0 }, Jcost (X ω.val)
112
113/-- The φ-code distance: minimum cost at a φ-ladder step.
114 d_φ = J(φ) = (√5 - 2)/2 ≈ 0.118 -/