175noncomputable def physical_space_is_quotient {L E : Type*} [RSConfigSpace L] 176 (m : RSMeasurement L E) : 177 RecognitionQuotient (toRecognizer m) ≃ Set.range m.measure := by
proof body
Definition body.
178 -- Specialize the generic quotient≃image theorem to the recognizer induced by `m`. 179 simpa [toRecognizer] using (quotient_equiv_image (r := toRecognizer m)) 180 181/-! ## J-Cost as Comparative Recognizer -/ 182 183/-- **Structural Definition**: The J-cost function is a comparative recognizer. 184 185 In RS, J(ℓ₁, ℓ₂) measures the "information cost" of transitioning 186 between ledger states. This is inherently comparative: 187 - J(ℓ, ℓ) = 0 (no cost to stay) 188 - J(ℓ₁, ℓ₂) ≥ 0 (transitions have non-negative cost) 189 - Smaller J means "closer" states 190 191 This provides the metric-like structure on configuration space. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.