code_distance

formal source

 107
 108/-- The code distance is the minimum cost of a non-trivial error.
 109    In RS, this is related to the φ-ladder structure. -/
 110noncomputable def code_distance (X : Ω → ℝ) : ℝ :=
 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 -/
 115noncomputable def phi_code_distance : ℝ :=
 116  Jcost Foundation.PhiForcing.φ
 117
 118/-- The φ-code distance is positive. -/
 119theorem phi_code_distance_pos : 0 < phi_code_distance := by
 120  unfold phi_code_distance
 121  apply Jcost_pos_of_ne_one
 122  · exact Foundation.PhiForcing.phi_pos
 123  · exact (Foundation.PhiForcing.phi_gt_one).ne'
 124
 125/-! ## Logical Operators -/
 126
 127/-- A logical operator is an operation that preserves the code structure.
 128    In RS, these correspond to recognition-preserving transformations. -/
 129structure LogicalOperator (X : Ω → ℝ) where
 130  /-- The operator as a function -/
 131  op : Ω → Ω
 132  /-- The operator preserves cost structure -/
 133  preserves_cost : ∀ ω, Jcost (X (op ω)) = Jcost (X ω)
 134
 135/-- The identity is always a logical operator. -/
 136def id_logical_op (X : Ω → ℝ) : LogicalOperator X where
 137  op := id
 138  preserves_cost := fun _ => rfl
 139
 140/-! ## Connection to Physical Laws -/