kernel_integral_match
plain-language theorem explainer
The theorem establishes that the integral of the J-cost of the recognition profile over [0, π/2 - θ_s] equals twice the integral of cot(ϑ + θ_s) over the same interval, for θ_s satisfying 0 < θ_s < π/2. Researchers deriving the C=2A relation in the measurement bridge would cite this result. The proof integrates the pointwise identity via almost-everywhere congruence after verifying bounds on the integration variable.
Claim. Let θ_s ∈ ℝ satisfy 0 < θ_s < π/2. Then ∫_{0}^{π/2 - θ_s} Jcost(recognitionProfile(ϑ + θ_s)) dϑ = 2 ∫_{0}^{π/2 - θ_s} cot(ϑ + θ_s) dϑ, where Jcost is the J-cost function and recognitionProfile is the profile r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 - 1).
background
The module proves the constructive kernel match from Local-Collapse Appendix D. The recognitionProfile is the function r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 − 1) for which the pointwise relation Jcost(r(ϑ)) = 2 cot(ϑ) holds, enabling the integral identity C = 2A. Jcost is the Recognition Science cost function J(x) = (x + x^{-1})/2 - 1. The local theoretical setting is the kernel match that connects path action to rate action in the Measurement domain.
proof idea
The tactic proof first establishes the pointwise identity Jcost(recognitionProfile(ϑ + θ_s)) = 2 cot(ϑ + θ_s) for ϑ in the closed interval by applying the sibling kernel_match_pointwise after verifying nonnegativity and upper bounds via add_nonneg and add_le_add_right. It lifts the identity to an almost-everywhere statement with respect to Lebesgue measure. It then invokes intervalIntegral.integral_congr_ae to equate the integrals and finishes with simpa.
why it matters
This declaration is used by measurement_bridge_C_eq_2A to prove pathAction(pathFromRotation rot) = 2 * rateAction rot. It supplies the integral step of the C=2A bridge theorem in the module documentation, realizing the pointwise identity J(r(ϑ)) dt = 2 dA from Local-Collapse Appendix D. In the Recognition Science framework it supports the measurement kernel that links to the forcing chain (T5 J-uniqueness, T6 phi fixed point) and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.