pith. sign in
module module high

IndisputableMonolith.Measurement.TwoBranchGeodesic

show as:
view Lean formalization →

TwoBranchGeodesic supplies the geometric primitives for two-branch rotations from angle θ_s to π/2 in the Recognition measurement setting. Downstream bridge modules cite it to establish the exact C=2A relation between recognition cost and residual action. The module consists of targeted definitions and lightweight lemmas that rest on the PathAction interface without importing measure-theoretic machinery.

claimA two-branch geodesic rotation $R(\theta_s \to \pi/2)$ equipped with residual action $A$, rate action, and normalized amplitudes derived from the J-cost on recognition paths.

background

The parent PathAction module supplies a minimal interface for recognition paths together with their action and weights, deliberately omitting piecewise-additivity and domain-shift lemmas to keep the build surface stable. TwoBranchGeodesic specializes this interface to the two-branch case that appears in quantum measurement. The sibling declarations introduce TwoBranchRotation, residualAction, rateAction, born_weight_from_rate, initialAmplitudeSquared, complementAmplitudeSquared, and the residual_action_invariant.

proof idea

This is a definition module, no proofs. It assembles the rotation object and its derived quantities (residual norm, amplitude squares, normalization) directly from the PathAction primitives.

why it matters in Recognition Science

The module supplies the concrete objects required by the C=2A bridge theorems in C2ABridge and the lightweight export in C2ABridgeLight. It also supplies the rotation profile used in KernelMatch to obtain the pointwise identity J(r(ϑ)) = 2 tan ϑ that yields the integral relation C = 2A. The construction therefore closes the central equivalence between recognition cost and residual-model rate action.

scope and limits

used by (3)

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)