`RecognitionBridge`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.OntologyPredicates
domain: Foundation
line: 392 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.OntologyPredicates on GitHub at line 392.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

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:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.