pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Measurement.C2ABridge

show as:
view Lean formalization →

The C2ABridge module constructs the recognition path from geodesic rotation by applying the recognition profile to the two-branch geometry. It establishes the integral identity C = 2A linking the recognition cost functional to the path action. Researchers deriving the Born rule from recognition cost would cite this bridge. The module assembles pointwise kernel matching from the imported lemmas followed by integration over the rotation angle.

claimThe module establishes the bridge $C = 2A$, where $C = 2A$ follows from integrating the pointwise identity $J(r(ϑ)) = 2 tan ϑ$ for the profile $r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 - 1)$ against the two-branch geodesic action $A = -ln(sin θ_s)$ with residual norm $||R|| = π/2 - θ_s$.

background

This module sits in the Measurement domain and imports the minimal PathAction interface for recognition paths and weights, the TwoBranchGeodesic geometry with residual norm $||R|| = π/2 - θ_s$ and rate action $A = -ln(sin θ_s)$, and the KernelMatch result that supplies the profile $r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)^2 - 1)$ satisfying $J(r(ϑ)) = 2 tan ϑ$ pointwise. These pieces enable the integral identity $C = 2A$ that converts recognition cost into path action. The setting follows the Local-Collapse construction of the two-branch rotation and the constructive kernel match from Appendix D.

proof idea

The module defines pathFromRotation to lift the geodesic rotation into a recognition path, introduces integral_cot_from_theta as an auxiliary, and proves measurement_bridge_C_eq_2A by integrating the pointwise kernel identity over the rotation interval. It further defines weight_bridge, weight_equals_born, and amplitude_modulus_bridge to prepare the link to probability weights. The argument is a direct assembly of the three imported modules with no additional sorry statements.

why it matters in Recognition Science

This module supplies the $C = 2A$ identity required by the downstream BornRule module, which derives $P(I) = |α_I|^2$ from the recognition cost $J$ and the amplitude bridge $𝒜 = exp(-C/2)·exp(iφ)$. It completes the measurement bridge step that converts the recognition profile into observable probabilities, consistent with the J-uniqueness landmark and the forcing chain from T5 onward.

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)