IndisputableMonolith.Measurement.KernelMatch

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Measurement.PathAction
   4import IndisputableMonolith.Measurement.TwoBranchGeodesic
   5
   6/-!
   7# Kernel Matching: Pointwise Identity J(r) dt = 2 dA
   8
   9This module proves the constructive kernel match from Local-Collapse Appendix D.
  10
  11The key lemma: for the profile
  12  r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 − 1),
  13we have J(r(ϑ)) = 2 tan ϑ pointwise, enabling the integral identity C = 2A.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Measurement
  18
  19open Real Cost
  20
  21/-- Recognition profile from eq (D.1) of Local-Collapse:
  22    r(ϑ) solves J(r(ϑ)) = 2 tan ϑ. -/
  23noncomputable def recognitionProfile (ϑ : ℝ) : ℝ :=
  24  1 + 2 * Real.cot ϑ + Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1)
  25
  26/-- The argument to arcosh is at least 1 for ϑ ∈ [0, π/2] -/
  27lemma arcosh_arg_ge_one (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  28  1 ≤ 1 + 2 * Real.cot ϑ := by
  29  have hsin : 0 ≤ Real.sin ϑ := by
  30    have hmem : ϑ ∈ Set.Icc (0 : ℝ) Real.pi := by
  31      constructor
  32      · exact hϑ.1
  33      · have hpi2_le_pi : (Real.pi / 2 : ℝ) ≤ Real.pi := by nlinarith [Real.pi_pos]
  34        exact le_trans hϑ.2 hpi2_le_pi
  35    simpa using Real.sin_nonneg_of_mem_Icc hmem
  36  have hcos : 0 ≤ Real.cos ϑ := by
  37    have hmem : ϑ ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) := by
  38      constructor
  39      · have hneg : (-(Real.pi / 2) : ℝ) ≤ 0 := by nlinarith [Real.pi_pos]
  40        exact le_trans hneg hϑ.1
  41      · exact hϑ.2
  42    simpa using Real.cos_nonneg_of_mem_Icc hmem
  43  have hcot : 0 ≤ Real.cot ϑ := by
  44    -- Rewrite `cot` as `cos / sin` on reals.
  45    simpa [Real.cot_eq_cos_div_sin] using (div_nonneg hcos hsin)
  46  have hprod : 0 ≤ 2 * Real.cot ϑ := by
  47    have htwo : 0 ≤ (2 : ℝ) := by norm_num
  48    exact mul_nonneg htwo hcot
  49  simpa using add_le_add_left hprod 1
  50
  51/-- Recognition profile is positive -/
  52lemma recognitionProfile_pos (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  53  0 < recognitionProfile ϑ := by
  54  have hy : 1 ≤ 1 + 2 * Real.cot ϑ := arcosh_arg_ge_one ϑ hϑ
  55  have hypos : 0 < 1 + 2 * Real.cot ϑ := lt_of_lt_of_le zero_lt_one hy
  56  have hs : 0 ≤ Real.sqrt ((1 + 2 * Real.cot ϑ) ^ 2 - 1) := Real.sqrt_nonneg _
  57  exact add_pos_of_pos_of_nonneg hypos hs
  58
  59/-- Pointwise kernel matching: J(r(ϑ)) = 2 tan ϑ
  60    This is the core technical lemma enabling C = 2A -/
  61theorem kernel_match_pointwise (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
  62  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ := by
  63  classical
  64  set y := 1 + 2 * Real.cot ϑ
  65  set s := Real.sqrt (y ^ 2 - 1)
  66  have hy : 1 ≤ y := by
  67    simpa [y] using arcosh_arg_ge_one ϑ hϑ
  68  have hy_pos : 0 < y := lt_of_lt_of_le zero_lt_one hy
  69  have hynonneg : 0 ≤ y := le_trans (by norm_num) hy
  70  have hrad_nonneg : 0 ≤ y ^ 2 - 1 := by
  71    have hsub : 0 ≤ y - 1 := sub_nonneg.mpr hy
  72    have hadd : 0 ≤ y + 1 := add_nonneg hynonneg (by norm_num)
  73    have hx := mul_nonneg hsub hadd
  74    convert hx using 1 <;> ring
  75  have hs_sq : s ^ 2 = y ^ 2 - 1 := by
  76    have := Real.mul_self_sqrt hrad_nonneg
  77    simpa [s, pow_two] using this
  78  have hxmul : (y + s) * (y - s) = 1 := by
  79    calc
  80      (y + s) * (y - s) = y ^ 2 - s ^ 2 := by ring
  81      _ = y ^ 2 - (y ^ 2 - 1) := by simpa [pow_two, hs_sq]
  82      _ = 1 := by ring
  83  have hxpos : 0 < y + s := add_pos_of_pos_of_nonneg hy_pos (Real.sqrt_nonneg _)
  84  have hxinv :
  85      (y + s) ⁻¹ = y - s := by
  86    have hxnonzero : y + s ≠ 0 := ne_of_gt hxpos
  87    have hx' := congrArg (fun t => (y + s)⁻¹ * t) hxmul
  88    have hx'' : (y - s) = (y + s)⁻¹ := by
  89      simpa [mul_assoc, hxnonzero] using hx'
  90    simpa [recognitionProfile, y, s] using hx''.symm
  91  have hxsum : (y + s) + (y - s) = 2 * y := by ring
  92  have hydiv : (2 * y) / 2 = y := by
  93    have : (2 : ℝ) ≠ 0 := by norm_num
  94    simpa [mul_comm] using (mul_div_cancel' y this)
  95  have hy_sub : y - 1 = 2 * Real.cot ϑ := by simp [y]
  96  calc
  97    Jcost (recognitionProfile ϑ)
  98        = ((y + s) + (y + s)⁻¹) / 2 - 1 := by simp [Jcost, recognitionProfile, y, s]
  99    _ = ((y + s) + (y - s)) / 2 - 1 := by simp [hxinv]
 100    _ = (2 * y) / 2 - 1 := by simpa [hxsum]
 101    _ = y - 1 := by simpa [hydiv]
 102    _ = 2 * Real.cot ϑ := hy_sub
 103
 104/-- Differential form of kernel match: J(r) dϑ = 2 tan ϑ dϑ -/
 105theorem kernel_match_differential (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
 106  Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ :=
 107  kernel_match_pointwise ϑ hϑ
 108
 109/-- The integrand match: ∫ J(r(ϑ)) dϑ = 2 ∫ tan ϑ dϑ -/
 110theorem kernel_integral_match (θ_s : ℝ) (hθ : 0 < θ_s ∧ θ_s < π/2) :
 111  ∫ ϑ in (0)..(π/2 - θ_s), Jcost (recognitionProfile (ϑ + θ_s)) =
 112  2 * ∫ ϑ in (0)..(π/2 - θ_s), Real.cot (ϑ + θ_s) := by
 113  -- Follows by integrating the pointwise identity
 114  -- measurability and integrability are standard for these smooth functions
 115  have hb_nonneg : 0 ≤ π/2 - θ_s := sub_nonneg.mpr (le_of_lt hθ.2)
 116  have hpt : ∀ ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s),
 117      Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
 118    intro ϑ hϑ
 119    apply kernel_match_pointwise (ϑ + θ_s)
 120    constructor
 121    · have hθ_nonneg : 0 ≤ θ_s := le_of_lt hθ.1
 122      exact add_nonneg hϑ.1 hθ_nonneg
 123    · have : ϑ ≤ π/2 - θ_s := hϑ.2
 124      have hsum := add_le_add_right this θ_s
 125      simpa [add_comm, add_left_comm, add_assoc] using hsum
 126  have h_ae :
 127      ∀ᵐ ϑ ∂MeasureTheory.volume,
 128        ϑ ∈ Set.uIoc 0 (π/2 - θ_s) →
 129          Jcost (recognitionProfile (ϑ + θ_s)) = 2 * Real.cot (ϑ + θ_s) := by
 130    refine Filter.Eventually.of_forall ?_
 131    intro ϑ hϑ
 132    have hIoc : ϑ ∈ Set.Ioc (0 : ℝ) (π/2 - θ_s) := by
 133      simpa [Set.uIoc, hb_nonneg] using hϑ
 134    have hIcc : ϑ ∈ Set.Icc (0 : ℝ) (π/2 - θ_s) := by
 135      exact ⟨le_of_lt hIoc.1, hIoc.2⟩
 136    exact hpt ϑ hIcc
 137  have hcongr :=
 138    intervalIntegral.integral_congr_ae
 139      (μ := MeasureTheory.volume)
 140      (a := 0) (b := π/2 - θ_s)
 141      (f := fun ϑ => Jcost (recognitionProfile (ϑ + θ_s)))
 142      (g := fun ϑ => 2 * Real.cot (ϑ + θ_s)) h_ae
 143  simpa using hcongr
 144
 145end Measurement
 146end IndisputableMonolith
 147