structure
definition
def or abbrev
RecognitionBridge
show as:
view Lean formalization →
formal statement (Lean)
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) : ℝ :=
proof body
Definition body.
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:
423 J(x_{ab}) = 0 ⟺ x_{ab} = 1 ⟺ ι(R(a)) = ι(R(b))
424 → (if ι injective) R(a) = R(b) ⟺ a ~_n b
425 → (if R injective, i.e. R = R_all) a = b
426
427And the reverse: a = b ⟹ J(x_{ab}) = 0 (no injectivity needed).
428-/
429
430theorem RecognitionBridge.zero_cost_iff_ratio_one {C E : Type*}
431 (b : RecognitionBridge C E) (a c : C) :
432 defect (b.pairRatio a c) = 0 ↔ b.pairRatio a c = 1 :=
433 defect_zero_iff_one (b.pairRatio_pos a c)
434
435theorem RecognitionBridge.ratio_one_iff_equal_scale {C E : Type*}
436 (b : RecognitionBridge C E) (a c : C) :
437 b.pairRatio a c = 1 ↔ b.ι (b.R a) = b.ι (b.R c) := by
438 constructor
439 · intro h
440 have hne := ne_of_gt (b.ι_pos (b.R c))
441 unfold pairRatio at h
442 rwa [div_eq_iff hne, one_mul] at h
443 · intro h
444 unfold pairRatio
445 rw [h, div_self (ne_of_gt (b.ι_pos _))]
446
447/-- Zero cost + injective ι ⟹ equal events: R(a) = R(c). (Paper Eq. 15) -/
448theorem RecognitionBridge.zero_cost_implies_equal_recognition {C E : Type*}
449 (b : RecognitionBridge C E) (hInj : Function.Injective b.ι)
450 (a c : C) (h : defect (b.pairRatio a c) = 0) :
451 b.R a = b.R c :=
452 hInj ((b.ratio_one_iff_equal_scale a c).mp ((b.zero_cost_iff_ratio_one a c).mp h))
453
454/-- Zero cost + injective ι + injective R ⟹ state equality: a = c. (Paper Eq. 17) -/
455theorem RecognitionBridge.zero_cost_injective_R_implies_eq {C E : Type*}
456 (b : RecognitionBridge C E)
457 (hι_inj : Function.Injective b.ι)
458 (hR_inj : Function.Injective b.R)
459 (a c : C) (h : defect (b.pairRatio a c) = 0) :
460 a = c :=
461 hR_inj (b.zero_cost_implies_equal_recognition hι_inj a c h)
462
463/-- Reverse direction: identity implies zero cost (no injectivity needed).
464 (Paper §3.1.2) -/
465theorem RecognitionBridge.identity_implies_zero_cost {C E : Type*}
466 (b : RecognitionBridge C E) (a : C) :
467 defect (b.pairRatio a a) = 0 := by
468 have h1 : b.pairRatio a a = 1 := by
469 unfold pairRatio
470 exact div_self (ne_of_gt (b.ι_pos _))
471 exact (b.zero_cost_iff_ratio_one a a).mpr h1
472
473/-! ## General RSReal with Discrete Skeleton (Paper §1.1, Eq. 8–9)
474
475The paper defines RSReal with a general discrete skeleton D ⊆ ℝ
476and a synthesis-map variant RSReal_{F,D_U}(x).
477-/
478
479/-- RSReal with a general discrete skeleton D ⊆ ℝ. (Paper Eq. 8) -/