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)
168theorem displays_invariant_under_equivalence {U1 U2 : RSUnits}
169 (h : UnitsEquivalent U1 U2) (hτ1 : U1.tau0 ≠ 0) (hℓ1 : U1.ell0 ≠ 0) :
170 (tau_rec_display U1) / U1.tau0 = (tau_rec_display U2) / U2.tau0 := by
proof body
Tactic-mode proof.
171 obtain ⟨_, α, hα, hτ2, _⟩ := h
172 have hτ2' : U2.tau0 ≠ 0 := by simp [hτ2, hα, hτ1]
173 rw [tau_rec_display_ratio U1 hτ1, tau_rec_display_ratio U2 hτ2']
174
175/-! Measurement Protocols and Falsifiers -/
176
177/-- Measurement protocol for K-gate validation -/
depends on (18)
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
-
UnitsEquivalent
in IndisputableMonolith.Constants.KDisplay
decl_use
-
tau_rec_display
in IndisputableMonolith.Constants.KDisplayCore
decl_use
-
tau_rec_display_ratio
in IndisputableMonolith.Constants.KDisplayCore
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
Measurement
in IndisputableMonolith.Data.Import
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
Measurement
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
Measurement
in IndisputableMonolith.Quantum.NonlocalityNoSignaling
decl_use
-
Falsifiers
in IndisputableMonolith.Relativity.ILG.Falsifiers
decl_use
-
RSUnits
in IndisputableMonolith.TruthCore.Display
decl_use