pith. machine review for the scientific record. sign in
def definition def or abbrev high

recognition_action

show as:
view Lean formalization →

Recognition action C for a geodesic rotation equals twice the residual rate action A. Quantum gravity researchers bridging collapse models to Born-rule probabilities cite this scaling. The definition is obtained by direct multiplication of the rate_action term.

claimLet $C(θ_s)$ denote the recognition action and $A(θ_s)$ the residual rate action for separation angle $θ_s$. Then $C(θ_s) = 2 A(θ_s)$, where $A(θ_s) = -ln(sin θ_s)$ for $0 < θ_s < π/2$.

background

The module Coherence Collapse and Born Rule Bridge defines recognition cost along a path γ as the integral of the J-cost function. Residual rate action A is defined as -ln(sin θ_s) for the separation angle θ_s in a two-branch geodesic rotation. This local setting formalizes the link between gravitational effects and quantum measurement probabilities via the C = 2A relation.

proof idea

One-line definition that multiplies the result of rate_action by two.

why it matters in Recognition Science

This definition supplies the central C = 2A identity used in born_weight_is_sin_sq to recover the Born rule as sin²(θ_s) and in the CoherenceCollapseCert structure to certify the collapse model. It realizes the paper's core result connecting recognition costs to gravitational collapse rates, distinguishing from Penrose-Diósi models by predicting a plateau after orthogonality.

scope and limits

formal statement (Lean)

  66noncomputable def recognition_action (theta_s : ℝ) : ℝ := 2 * rate_action theta_s

proof body

Definition body.

  67

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.