pith. sign in
module module high

IndisputableMonolith.Measurement.TwoBranchGeodesic

show as:
view Lean formalization →

The TwoBranchGeodesic module defines the two-branch rotation geometry for quantum measurement paths from initial angle θ_s to π/2. It supplies the explicit objects required by the C=2A equivalence and kernel-matching arguments. The structure rests on the lightweight PathAction interface for recognition costs and weights. Researchers deriving the central measurement bridge cite this module for the geodesic construction.

claimTwo-branch geodesic rotation from angle $θ_s$ to $π/2$ satisfying the recognition path action interface.

background

This module sits in the Measurement domain and imports the PathAction interface. That interface supplies a lightweight setup for recognition paths together with their action and weights; heavy measure-theoretic results on piecewise additivity and domain shifts are deliberately omitted. The module introduces the central object TwoBranchRotation together with supporting definitions for residual action, rate action, amplitude squares, and normalization invariants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the geometric foundation for the C=2A bridge proved in C2ABridge, which states that C equals 2A exactly for any two-branch geodesic rotation. It is also imported by the lightweight export C2ABridgeLight and by KernelMatch, whose key lemma establishes the pointwise identity J(r(ϑ)) = 2 tan ϑ for the profile r(ϑ) = (1 + 2 tan ϑ) + √((1 + 2 tan ϑ)² − 1). The construction therefore closes the two-branch case inside the recognition path action framework.

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)