IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.MainTheorem
   3
   4/-!
   5# Finite Boolean bridge to positive ratios
   6
   7This module gives a modest discrete-to-continuous bridge: finite Boolean
   8events with positive weights compare by likelihood ratios, and those ratios
   9are positive whenever both event weights are positive.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace LogicAsFunctionalEquation
  15
  16/-- A finite weighted Boolean reality over `Fin n`. -/
  17structure FiniteBooleanReality (n : Nat) where
  18  weight : Fin n → ℝ
  19  positive_weight : ∀ i, 0 < weight i
  20
  21namespace FiniteBooleanReality
  22
  23/-- The weight of an event. -/
  24noncomputable def eventWeight {n : Nat} (R : FiniteBooleanReality n)
  25    (event : Fin n → Bool) : ℝ :=
  26  ∑ i, if event i then R.weight i else 0
  27
  28/-- A positive witness for an event. -/
  29def EventNonempty {n : Nat} (event : Fin n → Bool) : Prop :=
  30  ∃ i, event i = true
  31
  32/-- Nonempty finite Boolean events have positive weight. -/
  33theorem eventWeight_pos {n : Nat} (R : FiniteBooleanReality n)
  34    (event : Fin n → Bool) (hNonempty : EventNonempty event) :
  35    0 < R.eventWeight event := by
  36  rcases hNonempty with ⟨i₀, hi₀⟩
  37  unfold eventWeight
  38  have h_nonneg : ∀ i : Fin n, 0 ≤ (if event i then R.weight i else 0) := by
  39    intro i
  40    by_cases h : event i
  41    · simp [h, le_of_lt (R.positive_weight i)]
  42    · simp [h]
  43  have h_i0_pos : 0 < (if event i₀ then R.weight i₀ else 0) := by
  44    simp [hi₀, R.positive_weight i₀]
  45  have h_le_sum :
  46      (if event i₀ then R.weight i₀ else 0) ≤
  47        ∑ i, if event i then R.weight i else 0 := by
  48    exact Finset.single_le_sum (fun i _ => h_nonneg i) (Finset.mem_univ i₀)
  49  exact lt_of_lt_of_le h_i0_pos h_le_sum
  50
  51/-- Likelihood ratio of two events. -/
  52noncomputable def eventRatio {n : Nat} (R : FiniteBooleanReality n)
  53    (A B : Fin n → Bool) : ℝ :=
  54  R.eventWeight A / R.eventWeight B
  55
  56/-- Nonempty event comparisons land in positive ratios. -/
  57theorem eventRatio_pos {n : Nat} (R : FiniteBooleanReality n)
  58    (A B : Fin n → Bool)
  59    (hA : EventNonempty A) (hB : EventNonempty B) :
  60    0 < R.eventRatio A B := by
  61  unfold eventRatio
  62  exact div_pos (eventWeight_pos R A hA) (eventWeight_pos R B hB)
  63
  64/-- Finite Boolean comparison embeds into the positive-ratio domain whenever
  65both compared events have positive measure. -/
  66theorem finite_boolean_logic_embeds_into_positive_ratios {n : Nat}
  67    (R : FiniteBooleanReality n)
  68    (A B : Fin n → Bool)
  69    (hA : EventNonempty A) (hB : EventNonempty B) :
  70    ∃ r : ℝ, 0 < r ∧ r = R.eventRatio A B :=
  71  ⟨R.eventRatio A B, eventRatio_pos R A B hA hB, rfl⟩
  72
  73end FiniteBooleanReality
  74
  75end LogicAsFunctionalEquation
  76end Foundation
  77end IndisputableMonolith
  78