IndisputableMonolith.Verification.BridgeCore

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Verification
   6
   7open Constants
   8
   9/-!
  10# Verification Bridge Core (certified-surface friendly)
  11
  12This module contains the **minimal** bridge-invariance infrastructure used by the
  13certified surface (RS spec / band invariance):
  14
  15- `UnitsRescaled` (anchor rescaling relation with fixed `c`)
  16- `Observable` + `BridgeEval` + `anchor_invariance`
  17- canonical K-gate observables and the bridge-level equality `K_gate_bridge`
  18
  19It intentionally avoids the larger rendering/manifest scaffolds in `IndisputableMonolith/Verification.lean`
  20so the certified import-closure stays small and non-smuggled.
  21-/
  22
  23/-- Anchor rescaling relation: scale time and length anchors together by s>0, keep c fixed. -/
  24structure UnitsRescaled (U U' : RSUnits) where
  25  s    : ℝ
  26  hs   : 0 < s
  27  tau0 : U'.tau0 = s * U.tau0
  28  ell0 : U'.ell0 = s * U.ell0
  29  cfix : U'.c = U.c
  30
  31def UnitsRescaled.refl (U : RSUnits) : UnitsRescaled U U :=
  32{ s := 1
  33, hs := by norm_num
  34, tau0 := by simp [one_mul]
  35, ell0 := by simp [one_mul]
  36, cfix := rfl }
  37
  38noncomputable def UnitsRescaled.symm {U U' : RSUnits} (h : UnitsRescaled U U') : UnitsRescaled U' U := by
  39  refine
  40    { s := h.s⁻¹
  41      hs := inv_pos.mpr h.hs
  42      tau0 := ?_
  43      ell0 := ?_
  44      cfix := h.cfix.symm }
  45  · have hs0 : h.s ≠ 0 := ne_of_gt h.hs
  46    have hcancel : h.s⁻¹ * (h.s * U.tau0) = U.tau0 := by
  47      calc
  48        h.s⁻¹ * (h.s * U.tau0) = (h.s⁻¹ * h.s) * U.tau0 := by
  49          simpa using (mul_assoc h.s⁻¹ h.s U.tau0).symm
  50        _ = U.tau0 := by simp [hs0]
  51    calc
  52      U.tau0 = h.s⁻¹ * (h.s * U.tau0) := hcancel.symm
  53      _ = h.s⁻¹ * U'.tau0 := by simp [h.tau0.symm]
  54  · have hs0 : h.s ≠ 0 := ne_of_gt h.hs
  55    have hcancel : h.s⁻¹ * (h.s * U.ell0) = U.ell0 := by
  56      calc
  57        h.s⁻¹ * (h.s * U.ell0) = (h.s⁻¹ * h.s) * U.ell0 := by
  58          simpa using (mul_assoc h.s⁻¹ h.s U.ell0).symm
  59        _ = U.ell0 := by simp [hs0]
  60    calc
  61      U.ell0 = h.s⁻¹ * (h.s * U.ell0) := hcancel.symm
  62      _ = h.s⁻¹ * U'.ell0 := by simp [h.ell0.symm]
  63
  64def UnitsRescaled.trans {U U' U'' : RSUnits} (h₁ : UnitsRescaled U U') (h₂ : UnitsRescaled U' U'') :
  65    UnitsRescaled U U'' :=
  66{ s := h₂.s * h₁.s
  67, hs := mul_pos h₂.hs h₁.hs
  68, tau0 := by
  69    calc
  70      U''.tau0 = h₂.s * U'.tau0 := h₂.tau0
  71      _ = h₂.s * (h₁.s * U.tau0) := by simp [h₁.tau0]
  72      _ = (h₂.s * h₁.s) * U.tau0 := by ring
  73, ell0 := by
  74    calc
  75      U''.ell0 = h₂.s * U'.ell0 := h₂.ell0
  76      _ = h₂.s * (h₁.s * U.ell0) := by simp [h₁.ell0]
  77      _ = (h₂.s * h₁.s) * U.ell0 := by ring
  78, cfix := by
  79    calc
  80      U''.c = U'.c := h₂.cfix
  81      _ = U.c := h₁.cfix }
  82
  83/-- A numeric display is dimensionless if it is invariant under anchor rescalings. -/
  84def Dimensionless (f : RSUnits → ℝ) : Prop := ∀ {U U'}, UnitsRescaled U U' → f U = f U'
  85
  86/-- Observable: a dimensionless display ready for bridge evaluation. -/
  87structure Observable where
  88  f       : RSUnits → ℝ
  89  dimless : Dimensionless f
  90
  91/-- Bridge evaluation (A ∘ Q): evaluate any observable under anchors; invariant by construction. -/
  92@[simp] def BridgeEval (O : Observable) (U : RSUnits) : ℝ := O.f U
  93
  94/-- Anchor-invariance (Q): evaluation does not depend on rescaled anchors. -/
  95theorem anchor_invariance (O : Observable) {U U'}
  96  (hUU' : UnitsRescaled U U') : BridgeEval O U = BridgeEval O U' := O.dimless hUU'
  97
  98/-- K_A observable equals constant K; dimensionless by definition. -/
  99noncomputable def K_A_obs : Observable :=
 100{ f := fun _ => Constants.K
 101, dimless := by intro _U _U' _h; rfl }
 102
 103/-- K_B observable equals constant K; dimensionless by definition. -/
 104noncomputable def K_B_obs : Observable :=
 105{ f := fun _ => Constants.K
 106, dimless := by intro _U _U' _h; rfl }
 107
 108/-- The two route displays agree identically as observables (bridge-level K-gate). -/
 109theorem K_gate_bridge : ∀ U, BridgeEval K_A_obs U = BridgeEval K_B_obs U := by
 110  intro U; simp [BridgeEval, K_A_obs, K_B_obs]
 111
 112end Verification
 113end IndisputableMonolith
 114