Pith. sign in
module module high

IndisputableMonolith.Measurement.KernelMatch

show as:
view Lean formalization →

Defines the recognition profile r(ϑ) by the Local-Collapse kernel equation J(r(ϑ)) = 2 cot ϑ, and proves the matching identities (pointwise, differential, integral) that identify the J-cost along that profile with the two-branch measurement geometry. Cited by anyone building the C = 2A bridge. The module is mostly algebraic inversion of J plus positivity and integral bookkeeping.

claimThe recognition profile $r(\vartheta)$ is the unique positive solution of $J(r(\vartheta)) = 2\cot\vartheta$, where $J(x) = \frac{x+x^{-1}}{2}-1$. The module establishes the pointwise kernel identity, its differential form, and the matching integral identity needed to equate recognition cost with residual rate action.

background

Recognition Science measures cost with the unique symmetric functional $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced at T5 of the unified chain. Local-Collapse introduces a recognition profile $r(\vartheta)$ on the two-branch measurement angle by the kernel equation $J(r(\vartheta)) = 2\cot\vartheta$ (eq.\ (D.1)).

The surrounding measurement stack supplies the geometric side: TwoBranchGeodesic formalizes residual norm $|R| = \pi/2 - \theta_s$ and rate action $A = -\ln(\sin\theta_s)$; PathAction gives the lightweight path-weight interface. This module sits between those geometric objects and the cost functional from Cost, defining $r$ and proving that the $J$-kernel really matches the cotangent source term.

proof idea

The module first defines recognitionProfile by inverting $J$ on the right-hand side $2\cot\vartheta$, using the standard arcosh representation of $J^{-1}$ and a lemma that the argument is at least one on the physical angle range. Positivity of $r$ is immediate from that construction.

Pointwise kernel match is then the defining equation restated. The differential and integral forms follow by differentiating under the profile and integrating the resulting identity against the two-branch measure; no heavy measure theory is required beyond the PathAction interface.

why it matters in Recognition Science

This is the algebraic hinge of the measurement bridge. Downstream, C2ABridge proves the exact equivalence $C = 2A$ for any two-branch geodesic rotation; that proof needs the kernel identity $J(r(\vartheta)) = 2\cot\vartheta$ as a foundational ingredient. KernelMatchCert packages the same identity for the verification layer.

In framework terms the module converts the abstract $J$-cost (T5) into an explicit angular profile on the eight-tick / two-branch geometry, so recognition cost and residual rate action become interchangeable. Without the match, the $C = 2A$ claim stays formal.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (6)