theorem proved term proof

`K_gate_eqK`

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

formal statement (Lean)

  44theorem K_gate_eqK (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  45  ((tau_rec_display U) / U.tau0 = K_gate_ratio) ∧ ((lambda_kin_display U) / U.ell0 = K_gate_ratio) := by

proof body

Term-mode proof.

  46  exact ⟨tau_rec_display_ratio U hτ, lambda_kin_display_ratio U hℓ⟩
  47
  48end RSUnits
  49end Constants
  50end IndisputableMonolith

used by (2)

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

single_inequality_audit in IndisputableMonolith.Constants.KDisplay decl_use
units_quotient_preserves_K in IndisputableMonolith.Constants.KDisplay decl_use

depends on (15)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
K_gate_ratio in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display_ratio in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display_ratio 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