Pith sign in
module module high

IndisputableMonolith.Measurement.C2ABridge

show as:
view Lean formalization →

Module C2ABridge constructs the recognition path from geodesic rotation using the recognition profile to establish the integral identity C = 2A. Researchers deriving the Born rule from the J-functional would cite this bridge. It assembles the pointwise kernel match from KernelMatch with the two-branch geodesic action definition.

claimThe identity $C = 2A$ holds for the recognition cost integral $C$ and the rate action $A = -\ln(\sin \theta_s)$ via the profile $r(\vartheta) = (1 + 2\tan\vartheta) + \sqrt{(1 + 2\tan\vartheta)^2 - 1}$ satisfying $J(r(\vartheta)) = 2\tan\vartheta$.

background

The module sits in the Measurement domain. It imports PathAction for lightweight recognition path interfaces and weights, TwoBranchGeodesic for the two-branch rotation geometry with residual norm $||R|| = \pi/2 - \theta_s$ and action $A = -\ln(\sin \theta_s)$, and KernelMatch for the pointwise identity $J(r(\vartheta)) = 2\tan\vartheta$ that enables the integral $C = 2A$ from Local-Collapse Appendix D.

The doc-comment states the module constructs the recognition path from geodesic rotation using the recognition profile. This supplies the missing link between the geodesic rate action and the full recognition cost functional.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the BornRule derivation by supplying the $C = 2A$ identity required for the amplitude bridge $\mathcal{A} = \exp(-C/2) \cdot \exp(i\phi)$. It fills the step from two-branch geodesic geometry to recognition cost in the measurement chain leading to $P(I) = |\alpha_I|^2$.

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)