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

IndisputableMonolith.Measurement.C2ABridgeLight

show as:
view Lean formalization →

The C2ABridgeLight module exports existence of C and A with C = 2A where exp(-C) aligns with the two-branch geodesic rate action. Physicists modeling quantum measurement collapse via rotation geometry cite it when linking rate actions to exponential factors in Recognition Science. The module imports TwoBranchGeodesic and supplies a lightweight interface with no internal proofs.

claimExistence of $C, A$ such that $C = 2A$ and $e^{-C}$ matches the factor derived from the geodesic residual norm $||R|| = π/2 - θ_s$.

background

This module sits in the Measurement domain and imports the two-branch quantum measurement geodesic. The upstream TwoBranchGeodesic formalizes rotation geometry from Local-Collapse §3 and Appendix A, with residual norm $||R|| = π/2 - θ_s$ (geodesic length) and rate action $A = -ln(sin θ_s)$. The sibling C_equals_2A supplies the core identity that this lightweight export re-exports.

proof idea

This is a definition module, no proofs. It re-exports the C = 2A relation and exponential match by direct import of the geodesic definitions from TwoBranchGeodesic.

why it matters in Recognition Science

The module bridges the two-branch geodesic rate action to the C = 2A identity, supporting the measurement results that follow from the sibling C_equals_2A. It supplies the lightweight export step required for exponential matching in the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)