Pith. sign in
module module high

IndisputableMonolith.Measurement.TwoBranchGeodesic

show as:
view Lean formalization →

Defines the two-branch geodesic model of a quantum measurement: a rotation from start angle θ_s to π/2, with residual and rate actions, Born weights, and amplitude squares. Measurement and verification modules cite it as the geometric substrate for C = 2A and the two-outcome Born certificate. The module is mostly definitions and elementary identities built on the path-action interface.

claimA two-branch measurement is a geodesic rotation from angle $\theta_s$ to $\pi/2$. On that path one defines residual action $A$, residual norm, rate action, Born weight from the rate, and the squared amplitudes $\sin^2\theta_s$ and $\cos^2\theta_s$, with normalization and residual-action invariance identities.

background

Recognition measurement is cast as path action on recognition trajectories. The upstream PathAction module supplies a minimal interface for paths and their actions/weights, deliberately omitting heavy measure theory so paper exports stay stable.

This module specializes that interface to the two-outcome case: a single angular geodesic from a start angle $\theta_s$ to the measurement pole $\pi/2$. The geometric objects are residual action (cost accumulated along the residual model), rate action, and the associated Born weight. Amplitudes are the usual trigonometric squares of the start angle, required to sum to one.

The setting is the Local-Collapse / C = 2A program: recognition cost $C$ is to be identified with twice a residual rate action $A$ on this geodesic, after which normalized path weights become $\cos^2\theta$ and $\sin^2\theta$.

proof idea

Definition-heavy module, not a single deep theorem. It introduces the two-branch rotation structure, residual and rate actions, positivity of the rate action, Born weight extracted from the rate, initial and complement amplitude squares, their normalization, and invariance of residual action under the model symmetries. Downstream bridges then prove $C = 2A$ and the Born certificate on top of these objects; the hard analytic work (kernel match $J(r(\vartheta)) = 2\cot\vartheta$) lives in KernelMatch and C2ABridge.

why it matters in Recognition Science

This is the geometric substrate for the central measurement bridge. C2ABridge and its lightweight export prove that for any two-branch geodesic rotation, recognition cost equals twice residual rate action exactly ($C = 2A$). KernelMatch supplies the pointwise identity $J(r(\vartheta)),dt = 2,dA$ on the explicit profile $r(\vartheta)$, which integrates to that bridge. TwoOutcomeBornCert upgrades the weight identity to normalized probabilities $P_{\cos} = \cos^2\theta$ and $P_{\sin} = \sin^2\theta$. Without the two-branch geodesic objects defined here, those modules have nothing to act on. In the broader RS chain this is the measurement-side realization of cost-driven collapse, not a forcing-chain (T0–T8) step.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)