kernel_match_differential
plain-language theorem explainer
Researchers deriving kernel identities in Recognition Science cite this result to obtain the differential relation J(r(ϑ)) dϑ = 2 tan ϑ dϑ from the explicit profile. It asserts that the J-cost of the recognition profile at angle ϑ equals twice the cotangent of ϑ for ϑ in the closed interval from 0 to π/2. The proof is a direct one-line application of the pointwise kernel match lemma.
Claim. For real ϑ satisfying 0 ≤ ϑ ≤ π/2, if r(ϑ) denotes the recognition profile 1 + 2 cot ϑ + √((1 + 2 cot ϑ)^2 − 1), then the J-cost of r(ϑ) equals 2 cot ϑ.
background
The module develops the kernel matching property from Local-Collapse Appendix D. The recognition profile is the explicit function r(ϑ) = 1 + 2 cot ϑ + √((1 + 2 cot ϑ)^2 − 1) constructed to solve the pointwise relation for the J-cost. The J-cost is the Recognition Science function J(x) = (x + x^{-1})/2 − 1 that quantifies recognition effort.
proof idea
The proof is a one-line wrapper that applies the pointwise kernel match lemma to the supplied ϑ and interval hypothesis.
why it matters
This supplies the differential form of the kernel match, which supports the integral identity C = 2A in the same module and realizes the constructive match from Local-Collapse Appendix D. It contributes to the measurement framework where J-cost relations connect to geometric quantities such as area elements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.