theorem proved term proof

`single_inequality_audit`

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

formal statement (Lean)

  75theorem single_inequality_audit (U : RSUnits) (hτ : U.tau0 ≠ 0) (hℓ : U.ell0 ≠ 0) :
  76  (tau_rec_display U) / U.tau0 ≤ (lambda_kin_display U) / U.ell0 := by

proof body

Term-mode proof.

  77  have h := K_gate_eqK U hτ hℓ
  78  rw [h.1, h.2]
  79
  80/-- Tolerance band for K-gate measurement -/

depends on (16)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
K 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_eqK in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
tau_rec_display in IndisputableMonolith.Constants.KDisplayCore decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
U in IndisputableMonolith.Constants.RSNativeUnits decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
U in IndisputableMonolith.Recognition decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use