theorem proved term proof

`display_speed_positive`

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

formal statement (Lean)

  97theorem display_speed_positive (U : RSUnits) (h : 0 < U.tau0) (hc : 0 < U.c) :
  98  0 < (lambda_kin_display U) / (tau_rec_display U) := by

Term-mode proof.

  99  rw [display_speed_eq_c U h]
 100  exact hc
 101
 102/-- Displays scale uniformly: ratio is scale-invariant -/

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
display_speed_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display in IndisputableMonolith.Constants.KDisplayCore decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
U in IndisputableMonolith.Recognition decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use