kernel_match_pointwise
plain-language theorem explainer
The pointwise kernel match equates the J-cost of the recognition profile at angle ϑ to twice the cotangent of ϑ for ϑ in the closed interval from 0 to π/2. Measurement theorists cite this lemma to justify the integral identity C = 2A in the kernel-matching construction. The proof is a direct algebraic reduction that introduces auxiliary variables y and s, verifies domain conditions via arcosh_arg_ge_one, establishes the inverse relation (y + s)^{-1} = y - s, and substitutes into the definition of Jcost to reach 2 cot ϑ.
Claim. For every real number ϑ satisfying 0 ≤ ϑ ≤ π/2, the J-cost of the recognition profile at ϑ equals twice the cotangent of ϑ: $J(r(ϑ)) = 2 cot ϑ$, where r(ϑ) denotes the recognition profile function.
background
The module proves the constructive kernel match from Local-Collapse Appendix D. The recognition profile is the explicit map r(ϑ) = y + s with y = 1 + 2 cot ϑ and s = √(y² − 1), chosen so that J(r(ϑ)) collapses to a simple trigonometric expression. J-cost is the function J(x) = (x + x^{-1})/2 − 1 taken from the phi-forcing structure in PhiForcingDerived.of. The local setting is the Measurement domain, where this identity supplies the pointwise integrand needed for the area-action relation C = 2A. The proof also invokes arcosh_arg_ge_one to guarantee y ≥ 1 and the non-negativity infrastructure from LedgerFactorization.of.
proof idea
The tactic proof sets y := 1 + 2 cot ϑ and s := √(y² − 1). It first obtains y ≥ 1 from arcosh_arg_ge_one ϑ hϑ, confirms 0 ≤ y² − 1, and shows s² = y² − 1 by Real.mul_self_sqrt. Direct ring calculation then yields (y + s)(y − s) = 1, from which (y + s)^{-1} = y − s follows by multiplication. Substituting the inverse into the definition of Jcost produces ((y + s) + (y − s))/2 − 1, which simplifies by ring to y − 1 and finally to 2 cot ϑ.
why it matters
This is the core technical lemma enabling C = 2A as stated in the module documentation. It is invoked directly by kernel_integral_match and kernel_match_differential within the same module. In the Recognition Science framework the result supplies the pointwise match between J-cost and the area element in the measurement kernel, supporting the derivation of constants inside the alpha band (137.030, 137.039) and the overall forcing chain from T5 J-uniqueness onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.