theorem
proved
tactic proof
observable_factors_through_quotient
show as:
view Lean formalization →
formal statement (Lean)
204theorem observable_factors_through_quotient (O : RSUnits → ℝ)
205 (hQuot : ∀ U α, α ≠ 0 → O {tau0 := α * U.tau0, ell0 := α * U.ell0, c := U.c,
proof body
Tactic-mode proof.
206 c_ell0_tau0 := by calc U.c * (α * U.tau0) = α * (U.c * U.tau0) := by ring
207 _ = α * U.ell0 := by rw [U.c_ell0_tau0]} = O U) :
208 ∀ U1 U2, UnitsEquivalent U1 U2 → O U1 = O U2 := by
209 intro U1 U2 h
210 obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
211 -- U2 = scaled version of U1
212 have h1 := hQuot U1 α hα
213 -- Need to show the scaled U1 equals U2
214 have hU2_eq : U2 = {tau0 := α * U1.tau0, ell0 := α * U1.ell0, c := U1.c,
215 c_ell0_tau0 := by calc U1.c * (α * U1.tau0) = α * (U1.c * U1.tau0) := by ring
216 _ = α * U1.ell0 := by rw [U1.c_ell0_tau0]} := by
217 cases U2
218 simp only [RSUnits.mk.injEq]
219 exact ⟨hτ, hℓ, hc.symm⟩
220 rw [hU2_eq]
221 exact h1.symm
222
223/-! Documentation and Usage -/
224
225/-!
226Standard K-gate verification procedure (documentation).
227
2281. Measure τ_rec via time-first route (e.g., pulsar timing)
2292. Measure λ_kin via length-first route (e.g., interferometry)
2303. Compute K from each: K_τ = τ_rec/τ0, K_λ = λ_kin/ℓ0
2314. Check agreement: |K_τ - K_λ| < tolerance
2325. If check fails → bridge falsified
233-/
234
235end RSUnits
236
237end Constants
238end IndisputableMonolith