kernel_match_differential
plain-language theorem explainer
Physicists integrating the kernel in the Local-Collapse model rely on J(r(ϑ)) = 2 cot ϑ for the recognition profile when ϑ ranges over [0, π/2]. The result supplies the differential form that integrates to C = 2A. It follows in one step from the pointwise identity.
Claim. For all real numbers ϑ satisfying 0 ≤ ϑ ≤ π/2, if r(ϑ) denotes the recognition profile 1 + 2 cot ϑ + √((1 + 2 cot ϑ)² − 1), then the J-cost satisfies J(r(ϑ)) = 2 cot ϑ.
background
The KernelMatch module proves the constructive kernel match from Local-Collapse Appendix D. The recognitionProfile function implements the profile r(ϑ) solving J(r(ϑ)) = 2 cot ϑ pointwise, with the module doc noting that this enables the integral identity C = 2A. The upstream kernel_match_pointwise theorem establishes Jcost(recognitionProfile ϑ) = 2 cot ϑ under the angle constraint 0 ≤ ϑ ≤ π/2, quoting its doc as the core technical lemma enabling C = 2A.
proof idea
The proof is a one-line wrapper that applies kernel_match_pointwise ϑ hϑ.
why it matters
This supplies the differential kernel match required for the integral identity C = 2A in the same module. It realizes the key step from Local-Collapse Appendix D and aligns with the Recognition Composition Law. The construction sits between the pointwise lemma and the integral match, consistent with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.