pith. machine review for the scientific record. sign in
def definition def or abbrev

alpha_inv_phys

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  40noncomputable def alpha_inv_phys (Q : ℝ) : ℝ :=

proof body

Definition body.

  41  if Q ≥ Q_lock then
  42    alpha_inv_running Q Q_lock (1 / alpha_locked)
  43  else
  44    1 / alpha_locked
  45
  46/-- **THEOREM: Physical Coupling Continuity**
  47    The physical coupling is continuous at the lock-in boundary.
  48    Both branches agree at Q = Q_lock (proved in `alpha_lock_at_scale`). -/

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.