KernelMatchCert
plain-language theorem explainer
Empty certificate packaging the pointwise identity J(r(ϑ)) = 2 cot ϑ on ϑ ∈ [0, π/2], with r the recognition profile. Measurement and bridge authors cite it when discharging the C = 2A kernel step. Verification is a one-line wrapper around the existing pointwise kernel-match lemma.
Claim. A kernel-match certificate is a unit record whose verification predicate asserts: for every real angle $\vartheta$ with $0 \le \vartheta \le \pi/2$, the recognition cost satisfies $J(r(\vartheta)) = 2\cot\vartheta$, where $r$ is the recognition profile and $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost $J(x) = (x + x^{-1})/2 - 1$ is the unique nonnegative recognition cost fixed by the Recognition Composition Law (T5). It vanishes only at ratio one and measures genuine distinction.
The recognition profile $r(\vartheta)$ is the explicit positive solution of $J(r) = 2\cot\vartheta$ on the closed quadrant $[0,\pi/2]$, written $r(\vartheta) = 1 + 2\cot\vartheta + \sqrt{(1+2\cot\vartheta)^2-1}$. It comes from the Local-Collapse measurement kernel (eq. D.1).
This module sits in Verification and only imports Measurement.KernelMatch. The certificate is a packaging layer: the mathematical content lives upstream as the pointwise identity, and the cert exposes a uniform verified predicate for downstream bridge proofs.
proof idea
The structure itself is empty (only Repr). The verified predicate is definitionally the universal statement over $\vartheta \in [0,\pi/2]$.
verified_any is a one-line wrapper: introduce the angle and its bounds, then apply Measurement.kernel_match_pointwise, which already proves $J(r(\vartheta)) = 2\cot\vartheta$ by direct algebraic expansion (set $y = 1+2\cot\vartheta$, take the positive square-root branch, and simplify).
why it matters
Doc-comment flags this as a foundational ingredient for the $C = 2A$ bridge proof: the pointwise match equates recognition cost along the profile to twice the cotangent amplitude factor. That identity is the core technical lemma enabling the continuum kernel equality.
In the RS forcing chain the cost is the T5-unique $J$, so the certificate ties measurement geometry back to the unique cost functional rather than an ad-hoc kernel. No downstream consumers are wired yet in the graph; the cert is the stable API surface those bridge theorems are expected to call.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.