kernel_match_differential
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove the integrated kernel identity over an interval.
- Does not extend the equality to ϑ outside [0, π/2].
- Does not address physical units or scaling of the J-cost.
- Does not derive the explicit recognition profile from first principles.
formal statement (Lean)
105theorem kernel_match_differential (ϑ : ℝ) (hϑ : 0 ≤ ϑ ∧ ϑ ≤ π/2) :
106 Jcost (recognitionProfile ϑ) = 2 * Real.cot ϑ :=
proof body
Term-mode proof.
107 kernel_match_pointwise ϑ hϑ
108
109/-- The integrand match: ∫ J(r(ϑ)) dϑ = 2 ∫ tan ϑ dϑ -/