kernel_integral_match
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.