def definition def or abbrev

`tau_rec_display`

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

formal statement (Lean)

  10@[simp] noncomputable def tau_rec_display (U : RSUnits) : ℝ :=

proof body

Definition body.

  11  (2 * Real.pi * U.tau0) / (8 * Real.log phi)
  12
  13/-- Length-side (kinematic) display definition: λ_kin(display) = (2π·ℓ₀) / (8 ln φ). -/

used by (22)

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

computeRatios in IndisputableMonolith.Certificates.UnitsKGate decl_use
display_null_condition in IndisputableMonolith.Constants.KDisplay decl_use
display_rate_matches_structural_rate in IndisputableMonolith.Constants.KDisplay decl_use
display_ratio_scale_invariant in IndisputableMonolith.Constants.KDisplay decl_use
displays_invariant_under_equivalence in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_eq_c_of_nonzero in IndisputableMonolith.Constants.KDisplay decl_use
display_speed_positive in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_tolerance in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_units_invariant in IndisputableMonolith.Constants.KDisplay decl_use
single_inequality_audit in IndisputableMonolith.Constants.KDisplay decl_use
tau_rec_display_ne_zero in IndisputableMonolith.Constants.KDisplay decl_use
tau_rec_display_pos in IndisputableMonolith.Constants.KDisplay decl_use
units_quotient_preserves_K in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_eqK in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_from_tau_rec in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display_ratio in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec in IndisputableMonolith.Constants.RSNativeUnits decl_use
tau_rec_eq_K_gate_ratio in IndisputableMonolith.Constants.RSNativeUnits decl_use
display_speed_identity in IndisputableMonolith.TruthCore.Display decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use

depends on (8)

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