theorem proved term proof

`display_speed_identity`

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

formal statement (Lean)

  34theorem display_speed_identity (U : Constants.RSUnits) :
  35  (Constants.RSUnits.lambda_kin_display U) / (Constants.RSUnits.tau_rec_display U) = U.c :=

proof body

Term-mode proof.

  36  Constants.RSUnits.display_speed_eq_c U
  37
  38end TruthCore
  39
  40end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.

RSUnits in IndisputableMonolith.Constants 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
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
U in IndisputableMonolith.Recognition decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use