`RSUnits`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 481.

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

 478-/
 479
 480/-- Minimal RS units used in Core. -/
 481structure RSUnits where
 482  tau0 : ℝ
 483  ell0 : ℝ
 484  c    : ℝ
 485  c_ell0_tau0 : c * tau0 = ell0
 486
 487/-- Dimensionless bridge ratio \(K\).
 488
 489Defined (non-circularly) as \(K = \varphi^{1/2}\). -/
 490@[simp] noncomputable def K : ℝ := phi ^ (1/2 : ℝ)
 491
 492@[simp] lemma K_def : K = phi ^ (1/2 : ℝ) := rfl
 493
 494lemma K_pos : 0 < K := by
 495  -- φ > 0, hence φ^(1/2) > 0
 496  simpa [K] using Real.rpow_pos_of_pos phi_pos (1/2 : ℝ)
 497
 498lemma K_nonneg : 0 ≤ K := le_of_lt K_pos
 499
 500/-- Alias matching parallel-work naming convention. -/
 501lemma one_lt_phiPointSixOne : (1.6 : ℝ) < phi := by linarith [phi_gt_onePointSixOne]
 502
 503/-- Alias: phi_gt_one ≡ one_lt_phi, for parallel-work compat. -/
 504lemma phi_gt_one : 1 < phi := one_lt_phi
 505
 506/-- φ ≈ 1.618 (coarse upper bound used in some modules). -/
 507lemma phi_approx : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
 508
 509/-- J(φ) = φ - 3/2 (exact, using φ² = φ + 1). -/
 510lemma Jcost_phi_val : Cost.Jcost phi = phi - 3 / 2 := by
 511  rw [Cost.Jcost_eq_sq phi_ne_zero]

papers checked against this theorem

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