pith. sign in
module module high

IndisputableMonolith.Measurement.KernelMatch

show as:
view Lean formalization →

This module supplies the recognition profile r(ϑ) solving J(r(ϑ)) = 2 tan ϑ from Local-Collapse (D.1), together with pointwise and integral kernel-match lemmas. Measurement theorists citing the C=2A bridge would import it to equate cost kernels with two-branch geodesic actions. The module is a lightweight collection of definitions and basic algebraic checks that rely on imported path-action and geodesic interfaces.

claimThe recognition profile satisfies $J(r(ϑ)) = 2 tan ϑ$, where $J(x) = (x + x^{-1})/2 - 1$. Supporting lemmas establish pointwise equality of the kernel with the geodesic rate action and integral matching over the profile.

background

The module sits inside the Measurement domain and imports the J-cost from Cost, the minimal path-action interface from PathAction, and the two-branch geodesic geometry from TwoBranchGeodesic. In the latter, residual norm equals π/2 minus the rotation angle and rate action equals -ln(sin θ_s). The profile r(ϑ) is introduced exactly as the solution to the functional equation stated in Local-Collapse eq (D.1).

proof idea

This is a definition module. It introduces recognitionProfile as the solution to the stated J-equation, then records elementary consequences (arcosh_arg_ge_one, positivity, pointwise kernel match, differential match, and integral match) via direct algebraic verification and the imported geodesic identities.

why it matters in Recognition Science

The module supplies the kernel-matching step required by the C=2A bridge in C2ABridge, whose main theorem states that recognition cost C equals twice the residual-model rate action A for any two-branch geodesic rotation. It therefore closes the measurement-kernel link between the J-cost formalism and the two-branch geometry used in Local-Collapse.

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)