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

IndisputableMonolith.Measurement.TwoBranchGeodesic

show as:
view Lean formalization →

This module supplies the geometric definitions for a two-branch geodesic rotation in recognition paths, starting at angle θ_s and terminating at π/2. Downstream bridge modules cite it to establish the exact C=2A relation between recognition cost and residual action. The module consists entirely of supporting definitions and invariants with no internal proofs.

claimA two-branch geodesic rotation in recognition path space from initial angle $θ_s$ to terminal angle $π/2$, equipped with residual action $A$ and rate action functions that satisfy the pointwise kernel identity $J(r(θ)) = 2 tan θ$.

background

The module imports the lightweight PathAction interface, which defines recognition paths together with their action and weight functionals while omitting heavy measure-theoretic results. It introduces the two-branch rotation as the central object for quantum measurement, along with sibling definitions for residual action, rate action, amplitude squares, and normalization invariants. These constructs operate in the setting where recognition cost C is computed along geodesics on the phi-ladder.

proof idea

This is a definition module containing no proofs. It exports the rotation object and its derived action functions for direct use in downstream equivalence statements.

why it matters in Recognition Science

The definitions feed the central C=2A theorem in C2ABridge and the kernel-matching lemma in KernelMatch, which together establish the constructive identity between recognition cost and residual-model rate action. The module supplies the geometric component required for the measurement bridge in the Recognition 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)