pith. sign in
module module high

IndisputableMonolith.Measurement.C2ABridge

show as:
view Lean formalization →

The measurement bridge module constructs the recognition path from two-branch geodesic rotation by matching the J-profile to the rotation geometry. It supplies the integral identity equating recognition cost to twice the geodesic action. Derivations of the Born rule from recognition cost cite this construction. The argument proceeds by pointwise kernel identity on the profile followed by integration over the rotation parameter.

claim$C = 2A$, where the recognition cost $C$ is the integral of the J-profile along the path lifted from geodesic rotation angle, and $A$ is the rate action of the two-branch geodesic.

background

The setting is the measurement domain. TwoBranchGeodesic formalizes the two-branch rotation geometry from Local-Collapse §3 and Appendix A. Key results: residual norm ||R|| = π/2 - θ_s (geodesic length) and rate action A = -ln(sin θ_s). KernelMatch proves the constructive kernel match from Local-Collapse Appendix D. The key lemma: for the profile r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 − 1), we have J(r(ϑ)) = 2 tan ϑ pointwise, enabling the integral identity C = 2A. PathAction supplies the minimal interface for paths and weights.

proof idea

This is a composition module. It lifts the geodesic rotation through the recognition profile to define the path, then integrates the pointwise kernel identity from KernelMatch against the action from TwoBranchGeodesic to obtain the equality.

why it matters in Recognition Science

This module supplies the C = 2A relation required by the BornRule module, which derives Born's rule P(I) = |α_I|² from the recognition cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ). It fills the bridge step in the measurement chain from geodesic geometry to probability weights.

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)