pith. sign in
module module high

IndisputableMonolith.Measurement.KernelMatch

show as:
view Lean formalization →

KernelMatch supplies the recognition profile r(ϑ) solving J(r(ϑ)) = 2 tan ϑ from Local-Collapse eq (D.1), together with pointwise, differential, and integral kernel-match lemmas. Measurement theorists bridging recognition cost to geodesic action cite it when establishing C = 2A. The module assembles algebraic identities on top of the imported Cost, PathAction, and TwoBranchGeodesic interfaces.

claimThe recognition profile satisfies $J(r(ϑ)) = 2 tan ϑ$, where $J$ is the J-cost function; this profile yields pointwise, differential, and integral kernel matches between recognition cost and two-branch geodesic action.

background

The module sits in the Measurement domain. It imports Cost for the J-cost function, PathAction for a lightweight interface to recognition paths and their action/weights, and TwoBranchGeodesic for the two-branch rotation geometry whose residual norm is ||R|| = π/2 - θ_s and whose rate action is A = -ln(sin θ_s). The central definition is the recognition profile drawn from equation (D.1) of Local-Collapse.

proof idea

This is a definition module, no proofs. It introduces recognitionProfile as the solution to the stated J-equation and records the three kernel-match statements as direct consequences of that equation.

why it matters in Recognition Science

KernelMatch supplies the profile and matching lemmas that feed the central theorem of C2ABridge establishing C = 2A exactly for any two-branch geodesic rotation. It therefore closes the algebraic step required by the measurement bridge in the Recognition Science framework.

scope and limits

used by (1)

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)