structure
definition
RecognitionBridge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OntologyPredicates on GitHub at line 392.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
389(Paper Eq. 15–17) which requires injectivity of ι.
390-/
391
392structure RecognitionBridge (C : Type*) (E : Type*) where
393 R : C → E
394 ι : E → ℝ
395 ι_pos : ∀ e, 0 < ι e
396 c_ref : C
397
398noncomputable def RecognitionBridge.ratio {C E : Type*}
399 (b : RecognitionBridge C E) (c : C) : ℝ :=
400 b.ι (b.R c) / b.ι (b.R b.c_ref)
401
402lemma RecognitionBridge.ratio_pos {C E : Type*}
403 (b : RecognitionBridge C E) (c : C) : 0 < b.ratio c :=
404 div_pos (b.ι_pos _) (b.ι_pos _)
405
406noncomputable def RecognitionBridge.toCostBridge {C E : Type*}
407 (b : RecognitionBridge C E) : CostBridge C where
408 χ := b.ratio
409 χ_pos := b.ratio_pos
410
411/-- Pairwise comparison ratio: x_{ab} = ι(R(a)) / ι(R(c)). -/
412noncomputable def RecognitionBridge.pairRatio {C E : Type*}
413 (b : RecognitionBridge C E) (a c : C) : ℝ :=
414 b.ι (b.R a) / b.ι (b.R c)
415
416lemma RecognitionBridge.pairRatio_pos {C E : Type*}
417 (b : RecognitionBridge C E) (a c : C) : 0 < b.pairRatio a c :=
418 div_pos (b.ι_pos _) (b.ι_pos _)
419
420/-! ## Event-Space Equivalence Pipeline (Paper §3.1, Eq. 15–17)
421
422The paper derives the chain: