def definition def or abbrev

`rateAction`

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

formal statement (Lean)

  37noncomputable def rateAction (rot : TwoBranchRotation) : ℝ :=

Definition body.

  38  - Real.log (Real.sin rot.θ_s)
  39
  40/-- Rate action is positive for θ_s ∈ (0, π/2) -/

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

amplitude_modulus_bridge in IndisputableMonolith.Measurement.C2ABridge decl_use
measurement_bridge_C_eq_2A in IndisputableMonolith.Measurement.C2ABridge decl_use
weight_bridge in IndisputableMonolith.Measurement.C2ABridge decl_use
weight_equals_born in IndisputableMonolith.Measurement.C2ABridge decl_use
C_equals_2A in IndisputableMonolith.Measurement.C2ABridgeLight decl_use
born_weight_from_rate in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use
rateAction_pos in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
TwoBranchRotation in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use