kernel_integral_match
The theorem equates the integral of J-cost over the recognition profile from 0 to pi/2 minus theta sub s with twice the integral of cotangent of the shifted angle over the same interval. Researchers closing the C equals 2A relation in the measurement bridge would cite it to justify equating path action to twice the rate action. The proof integrates the pointwise identity by lifting it to almost-everywhere equality and applying the interval integral congruence lemma.
claimFor real $θ_s$ with $0 < θ_s < π/2$, let $r$ denote the recognition profile. Then $∫_0^{π/2 - θ_s} J_{cost}(r(ϑ + θ_s)) dϑ = 2 ∫_0^{π/2 - θ_s} cot(ϑ + θ_s) dϑ$.
background
The Kernel Matching module proves the constructive kernel match from Local-Collapse Appendix D. The recognition profile is given by r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 − 1), and the J-cost is the functional J(x) = (x + x^{-1})/2 − 1. The module establishes that J(r(ϑ)) equals 2 cot(ϑ) pointwise in the relevant range, enabling the integral identity C = 2A. Upstream results include the pointwise kernel match and basic arithmetic lemmas for nonnegativity and ordering.
proof idea
The proof first records nonnegativity of the upper integration limit. It then proves the pointwise equality on the closed interval by applying kernel_match_pointwise after checking the shifted argument stays in the valid domain via add_nonneg and add_le_add_right. This equality is lifted to an almost-everywhere statement over the open interval using Eventually.of_forall and conversion from uIoc to Icc. The final step invokes intervalIntegral.integral_congr_ae to equate the integrals.
why it matters in Recognition Science
This supplies the integrated kernel identity that feeds directly into measurement_bridge_C_eq_2A, the main C=2A Bridge Theorem asserting pathAction equals twice rateAction for the constructed path. It realizes the kernel match from Local-Collapse Appendix D and closes the step from pointwise J-cost identity to global action equality in the Recognition Science measurement framework.
scope and limits
- Does not establish the underlying pointwise identity.
- Does not extend beyond the interval (0, π/2 − θ_s) for θ_s in (0, π/2).
- Does not address measurability for non-smooth profiles.
- Does not generalize to other forcing chains or dimensions.
Lean usage
have hkernel : ∫ ϑ in (0)..(π/2 - rot.θ_s), Jcost (recognitionProfile (ϑ + rot.θ_s)) = 2 * ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s) := kernel_integral_match rot.θ_s rot.hθformal statement (Lean)
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
proof body
Tactic-mode proof.
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