`K_gate_eqK`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.KDisplayCore
domain: Constants
line: 44 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.KDisplayCore on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  41    _ = (2 * Real.pi * U.ell0) / (8 * Real.log phi) := by rw [h]
  42
  43/-- Canonical K-gate: both route ratios equal K_gate_ratio. -/
  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
  46  exact ⟨tau_rec_display_ratio U hτ, lambda_kin_display_ratio U hℓ⟩
  47
  48end RSUnits
  49end Constants
  50end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.