def definition def or abbrev

`residualAction`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  29noncomputable def residualAction (rot : TwoBranchRotation) : ℝ :=

Definition body.

  30  π/2 - rot.θ_s
  31
  32/-- Residual norm ||R|| = dθ/dt integrated over the rotation -/

From the project-wide theorem graph. These declarations reference this one in their body.

residual_action_invariant in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use
residualNorm in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use

Lean names referenced from this declaration's body.

TwoBranchRotation in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use