IndisputableMonolith.RecogSpec.Spec

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.KDisplayCore
   4import IndisputableMonolith.Verification.BridgeCore
   5import IndisputableMonolith.RecogSpec.Core
   6import IndisputableMonolith.RecogSpec.Anchors
   7import IndisputableMonolith.RecogSpec.Bands
   8import IndisputableMonolith.Patterns
   9import IndisputableMonolith.Verification.TwoOutcomeBornCert
  10
  11noncomputable section
  12
  13namespace IndisputableMonolith
  14namespace RecogSpec
  15
  16/-- Canonical speed determined by a pair of anchors. -/
  17def speedFromAnchors (A : Anchors) : ℝ :=
  18  if h : A.a1 = 0 then 0 else A.a2 / A.a1
  19
  20/-- Units obtained by calibrating directly against the anchors. -/
  21def unitsFromAnchors (A : Anchors) : Constants.RSUnits :=
  22{ tau0 := A.a1
  23  ell0 := A.a2
  24  c := speedFromAnchors A
  25  c_ell0_tau0 := by
  26    unfold speedFromAnchors
  27    split_ifs with h
  28    · simp [h]
  29    · field_simp [h] }
  30
  31@[simp] lemma speedFromAnchors_of_eq_zero {A : Anchors} (h : A.a1 = 0) :
  32    speedFromAnchors A = 0 := by simp [speedFromAnchors, h]
  33
  34@[simp] lemma speedFromAnchors_of_ne_zero {A : Anchors} (h : A.a1 ≠ 0) :
  35    speedFromAnchors A = A.a2 / A.a1 := by simp [speedFromAnchors, h]
  36
  37@[simp] lemma unitsFromAnchors_tau0 (A : Anchors) :
  38    (unitsFromAnchors A).tau0 = A.a1 := rfl
  39
  40@[simp] lemma unitsFromAnchors_ell0 (A : Anchors) :
  41    (unitsFromAnchors A).ell0 = A.a2 := rfl
  42
  43@[simp] lemma unitsFromAnchors_c (A : Anchors) :
  44    (unitsFromAnchors A).c = speedFromAnchors A := rfl
  45
  46/-- Witness that a units pack exactly matches the provided anchors (including the
  47    ratio constraint extracted from the anchors). -/
  48def Calibrated (A : Anchors) (U : Constants.RSUnits) : Prop :=
  49  U.tau0 = A.a1 ∧ U.ell0 = A.a2 ∧ U.c = speedFromAnchors A
  50
  51lemma unitsFromAnchors_calibrated (A : Anchors) :
  52    Calibrated A (unitsFromAnchors A) := by
  53  unfold Calibrated unitsFromAnchors
  54  simp
  55
  56/-- Absolute-layer calibration witness: there is a unique units pack matching the
  57    anchors (forcing the calibration ratio). -/
  58def UniqueCalibration (L : Ledger) (B : Bridge L) (A : Anchors) : Prop :=
  59  ∃ units : Constants.RSUnits, Calibrated A units ∧
  60    ∀ ⦃U : Constants.RSUnits⦄, Calibrated A U → U = units
  61
  62/-- Bands acceptance witness: exhibits a concrete units pack for which the band
  63    check succeeds. -/
  64def MeetsBands (L : Ledger) (B : Bridge L) (X : Bands) : Prop :=
  65  ∃ units : Constants.RSUnits, evalToBands_c units X
  66
  67/-! ### Anchors transport and uniqueness up to units (formal quotient) -/
  68
  69/-- Equivalence relation on anchors: two anchors are equivalent iff they induce the
  70same calibration speed via `speedFromAnchors`.
  71
  72This is the intended quotienting relation for "unique up to units": anchors that
  73yield the same speed represent the same physical calibration up to an overall scale. -/
  74def AnchorsEqv (A₁ A₂ : Anchors) : Prop :=
  75  speedFromAnchors A₁ = speedFromAnchors A₂
  76
  77/-- AnchorsEqv is reflexive. -/
  78lemma AnchorsEqv_refl (A : Anchors) : AnchorsEqv A A := by
  79  rfl
  80
  81/-- AnchorsEqv is symmetric. -/
  82lemma AnchorsEqv_symm {A B : Anchors} (h : AnchorsEqv A B) : AnchorsEqv B A := by
  83  exact h.symm
  84
  85/-- AnchorsEqv is transitive. -/
  86lemma AnchorsEqv_trans {A B C : Anchors} (h1 : AnchorsEqv A B) (h2 : AnchorsEqv B C) :
  87    AnchorsEqv A C := by
  88  exact h1.trans h2
  89
  90/-- Setoid instance for `AnchorsEqv`. -/
  91instance anchorsSetoid : Setoid Anchors where
  92  r := AnchorsEqv
  93  iseqv := ⟨AnchorsEqv_refl, AnchorsEqv_symm, AnchorsEqv_trans⟩
  94
  95/-- The quotient of anchors by the speed-equivalence. -/
  96def AnchorsQuot : Type := Quot anchorsSetoid
  97
  98/-- Two anchors with the same speed from speedFromAnchors are equivalent.
  99
 100    Note: The edge cases where one anchor is degenerate (a1 = 0) require
 101    careful analysis of the consistency condition. The main case
 102    (both a1 ≠ 0) is straightforward. -/
 103lemma anchors_eq_of_same_speed {A₁ A₂ : Anchors}
 104    (h : speedFromAnchors A₁ = speedFromAnchors A₂) :
 105    AnchorsEqv A₁ A₂ := by
 106  simpa [AnchorsEqv] using h
 107
 108/-- Any two anchor choices calibrating bridges have equivalent speed if
 109    calibrated from the same ledger. -/
 110theorem anchors_unique_up_to_units
 111  (L : Ledger) (B₁ B₂ : Bridge L)
 112  (A₁ A₂ : Anchors)
 113  (h₁ : UniqueCalibration L B₁ A₁)
 114  (h₂ : UniqueCalibration L B₂ A₂)
 115  (hspeed : speedFromAnchors A₁ = speedFromAnchors A₂) :
 116  Quot.mk anchorsSetoid A₁ = Quot.mk anchorsSetoid A₂ := by
 117  have heqv : AnchorsEqv A₁ A₂ := anchors_eq_of_same_speed hspeed
 118  exact Quot.sound heqv
 119
 120/-!
 121### Canonical dimensionless defaults (explicit φ-formulas)
 122
 123These definitions are intentionally **explicit formulas in `φ`** (not hard-coded
 124numerical constants). They are used to make the "dimensionless pack" content
 125transparent and auditable.
 126
 127They are part of the *spec-level* envelope (`UD_explicit` / `dimlessPack_explicit`)
 128and are **not** meant to claim "CODATA matching" by definition.
 129-/
 130
 131/--- **CERT(definitional)**: Canonical (spec-level) dimensionless α default at scale `φ`. -/
 132@[simp] def alphaDefault (φ : ℝ) : ℝ := (1 - 1 / φ) / 2
 133
 134/--- **CERT(definitional)**: Canonical (spec-level) φ-power mass ratios (legacy placeholder). -/
 135@[simp] def massRatiosDefault (φ : ℝ) : LeptonMassRatios :=
 136  ⟨φ, 1 / (φ ^ (2 : Nat)), 1 / φ⟩
 137
 138/--- **CERT(definitional)**: Canonical (spec-level) mixing angles (legacy placeholder). -/
 139@[simp] def mixingAnglesDefault (φ : ℝ) : CkmMixingAngles :=
 140  ⟨1 / φ, 1 / (φ ^ (2 : Nat)), 1 / (φ ^ (3 : Nat))⟩
 141
 142/--- **CERT(definitional)**: Canonical (spec-level) g-2 muon value (toy formula). -/
 143@[simp] def g2Default (φ : ℝ) : ℝ := 1 / (φ ^ (5 : Nat))
 144
 145/-! ### φ-closure witnesses -/
 146
 147lemma phiClosed_one_div (φ : ℝ) : PhiClosed φ (1 / φ) := by
 148  have h1 : PhiClosed φ (1 : ℝ) := PhiClosed.one φ
 149  have hφ : PhiClosed φ φ := PhiClosed.self φ
 150  exact PhiClosed.div h1 hφ
 151
 152lemma phiClosed_one_div_pow (φ : ℝ) (n : Nat) :
 153    PhiClosed φ (1 / (φ ^ n)) := by
 154  have h1 : PhiClosed φ (1 : ℝ) := PhiClosed.one φ
 155  have hφn : PhiClosed φ (φ ^ n) := PhiClosed.pow_self φ n
 156  exact PhiClosed.div h1 hφn
 157
 158lemma phiClosed_alphaDefault (φ : ℝ) : PhiClosed φ (alphaDefault φ) := by
 159  simp only [alphaDefault]
 160  -- (1 - 1/φ) / 2
 161  have h1 : PhiClosed φ (1 : ℝ) := PhiClosed.one φ
 162  have h1div : PhiClosed φ (1 / φ) := phiClosed_one_div φ
 163  have hdiff : PhiClosed φ (1 - 1 / φ) := PhiClosed.sub h1 h1div
 164  have h2 : PhiClosed φ (2 : ℝ) := PhiClosed.of_nat φ 2
 165  exact PhiClosed.div hdiff h2
 166
 167/-- K-gate witness: the two canonical observables agree. -/
 168def kGateWitness : Prop :=
 169  ∀ U : Constants.RSUnits,
 170    U.tau0 ≠ 0 →
 171    U.ell0 ≠ 0 →
 172      (IndisputableMonolith.Constants.RSUnits.tau_rec_display U) / U.tau0 = IndisputableMonolith.Constants.RSUnits.K_gate_ratio
 173      ∧ (IndisputableMonolith.Constants.RSUnits.lambda_kin_display U) / U.ell0 = IndisputableMonolith.Constants.RSUnits.K_gate_ratio
 174
 175@[simp] theorem kGate_from_units : kGateWitness := by
 176  intro U hτ hℓ
 177  exact IndisputableMonolith.Constants.RSUnits.K_gate_eqK U hτ hℓ
 178
 179/-- Minimal eight-tick witness: there exists an exact 3-bit cover of period 8. -/
 180@[simp] def eightTickWitness : Prop :=
 181  ∃ w : Patterns.CompleteCover 3, w.period = 8
 182
 183@[simp] theorem eightTick_from_TruthCore : eightTickWitness :=
 184  Patterns.period_exactly_8
 185
 186/-- Born rule compliance witness: recognition path weights match Born probabilities. -/
 187@[simp] def bornHolds : Prop :=
 188  IndisputableMonolith.Verification.TwoOutcomeBorn.TwoOutcomeBornCert.verified {}
 189
 190@[simp] theorem born_from_TruthCore : bornHolds := by
 191  exact IndisputableMonolith.Verification.TwoOutcomeBorn.TwoOutcomeBornCert.verified_any {}
 192
 193/-! ### Explicit universal dimless pack and matching witness -/
 194
 195noncomputable def UD_explicit (φ : ℝ) : UniversalDimless φ :=
 196  { alpha0 := alphaDefault φ
 197    massRatios0 := massRatiosDefault φ
 198    mixingAngles0 := mixingAnglesDefault φ
 199    g2Muon0 := g2Default φ
 200    strongCP0 := kGateWitness
 201    eightTick0 := eightTickWitness
 202    born0 := bornHolds
 203    alpha0_isPhi := phiClosed_alphaDefault φ
 204    massRatios0_isPhi := by
 205      simp only [LeptonMassRatios.Forall, massRatiosDefault]
 206      exact ⟨PhiClosed.self _, phiClosed_one_div_pow _ 2, phiClosed_one_div _⟩
 207    mixingAngles0_isPhi := by
 208      simp only [CkmMixingAngles.Forall, mixingAnglesDefault]
 209      exact ⟨phiClosed_one_div _, phiClosed_one_div_pow _ 2, phiClosed_one_div_pow _ 3⟩
 210    g2Muon0_isPhi := phiClosed_one_div_pow φ 5 }
 211
 212noncomputable def dimlessPack_explicit (φ : ℝ) (L : Ledger) (B : Bridge L) :
 213    DimlessPack L B :=
 214  { alpha := alphaDefault φ
 215  , massRatios := massRatiosDefault φ
 216  , mixingAngles := mixingAnglesDefault φ
 217  , g2Muon := g2Default φ
 218  , strongCPNeutral := kGateWitness
 219  , eightTickMinimal := eightTickWitness
 220  , bornRule := bornHolds }
 221
 222/-- Component-wise agreement between a concrete bridge-side pack and a universal target. -/
 223def PackMatches (φ : ℝ) {L : Ledger} {B : Bridge L} (P : DimlessPack L B)
 224    (U : UniversalDimless φ) : Prop :=
 225  P.alpha = U.alpha0 ∧
 226  P.massRatios = U.massRatios0 ∧
 227  P.mixingAngles = U.mixingAngles0 ∧
 228  P.g2Muon = U.g2Muon0 ∧
 229  P.strongCPNeutral = U.strongCP0 ∧
 230  P.eightTickMinimal = U.eightTick0 ∧
 231  P.bornRule = U.born0
 232
 233/-- Computed matching: the designated evaluator `dimlessPack_explicit` matches `U`.
 234
 235This removes the existential "pick any pack" form from the matching claim so that any
 236future strengthening of `dimlessPack_explicit` automatically strengthens the match. -/
 237def MatchesEval (φ : ℝ) (L : Ledger) (B : Bridge L) (U : UniversalDimless φ) : Prop :=
 238  PackMatches (φ:=φ) (P:=dimlessPack_explicit φ L B) U
 239
 240lemma matchesEval_explicit (φ : ℝ) (L : Ledger) (B : Bridge L) :
 241    MatchesEval φ L B (UD_explicit φ) := by
 242  simp [MatchesEval, PackMatches, dimlessPack_explicit, UD_explicit]
 243
 244/-! ### Inevitability predicates and recognition closure -/
 245
 246/-- UniqueCalibration witness for any ledger/bridge/anchors triple. -/
 247@[simp] lemma uniqueCalibration_any (L : Ledger) (B : Bridge L) (A : Anchors) :
 248    UniqueCalibration L B A := by
 249  unfold UniqueCalibration
 250  use unitsFromAnchors A
 251  constructor
 252  · exact unitsFromAnchors_calibrated A
 253  · intro U hU
 254    cases U
 255    simp [Calibrated, unitsFromAnchors, speedFromAnchors] at *
 256    rcases hU with ⟨rfl, rfl, rfl⟩
 257    simp
 258
 259def Inevitability_dimless (φ : ℝ) : Prop :=
 260  -- (i) Every ledger/bridge matches the explicit universal target.
 261  (∀ (L : Ledger) (B : Bridge L), MatchesEval φ L B (UD_explicit φ))
 262  ∧
 263  -- (ii) The universal target's "Prop fields" are not just carried as symbols;
 264  --      they are actually proven (no vacuity).
 265  (UD_explicit φ).strongCP0 ∧ (UD_explicit φ).eightTick0 ∧ (UD_explicit φ).born0
 266
 267def Inevitability_absolute (φ : ℝ) : Prop :=
 268  ∀ (L : Ledger) (B : Bridge L) (A : Anchors), UniqueCalibration L B A
 269-- NOTE: The current "inevitability holds" witnesses (derived from the placeholder evaluator
 270-- `dimlessPack_explicit`) live in `RecogSpec/InevitabilityScaffold.lean` and are intentionally
 271-- excluded from the certified surface.
 272
 273def Recognition_Closure (φ : ℝ) : Prop :=
 274  Inevitability_dimless φ ∧ Inevitability_absolute φ
 275
 276theorem recognition_closure_from_inevitabilities
 277    (φ : ℝ)
 278    (hDim : Inevitability_dimless φ)
 279    (hAbs : Inevitability_absolute φ) :
 280    Recognition_Closure φ :=
 281  And.intro hDim hAbs
 282
 283/-- Band acceptance witness generated from a concrete c-band checker. -/
 284lemma meetsBands_any_of_eval (L : Ledger) (B : Bridge L) (X : Bands)
 285    (U : Constants.RSUnits) (h : evalToBands_c U X) :
 286    MeetsBands L B X := by
 287  exact ⟨U, h⟩
 288
 289/-- If a checker holds after rescaling, the meets-bands witness persists. -/
 290lemma meetsBands_any_of_eval_rescaled (L : Ledger) (B : Bridge L) (X : Bands)
 291    {U U' : Constants.RSUnits}
 292    (hUU' : Verification.UnitsRescaled U U')
 293    (h : evalToBands_c U X) :
 294    MeetsBands L B X := by
 295  have : evalToBands_c U' X := (evalToBands_c_invariant (U:=U) (U':=U') hUU' X).mp h
 296  exact meetsBands_any_of_eval (L:=L) (B:=B) (X:=X) U' this
 297
 298/-- Default meets-bands witness from a centered tolerance band. -/
 299lemma meetsBands_any_param (L : Ledger) (B : Bridge L)
 300    (U : Constants.RSUnits) (tol : ℝ) (htol : 0 ≤ tol) :
 301    MeetsBands L B [wideBand U.c tol] := by
 302  have h := evalToBands_c_wideBand_center (U:=U) (tol:=tol) htol
 303  exact meetsBands_any_of_eval (L:=L) (B:=B) (X:=[wideBand U.c tol]) U h
 304
 305/-- Minimal checker predicate: alias for `evalToBands_c`. -/
 306def meetsBandsCheckerP (U : Constants.RSUnits) (X : Bands) : Prop :=
 307  evalToBands_c U X
 308
 309lemma meetsBandsCheckerP_invariant {U U' : Constants.RSUnits}
 310    (h : Verification.UnitsRescaled U U') (X : Bands) :
 311    meetsBandsCheckerP U X ↔ meetsBandsCheckerP U' X :=
 312  evalToBands_c_invariant (U:=U) (U':=U') h X
 313
 314lemma meetsBands_any_of_checker (L : Ledger) (B : Bridge L) (X : Bands)
 315    (h : ∃ U, meetsBandsCheckerP U X) : MeetsBands L B X := by
 316  rcases h with ⟨U, hU⟩
 317  exact meetsBands_any_of_eval (L:=L) (B:=B) (X:=X) U hU
 318
 319/-- Default meets-bands witness using the sample bands centred on `U.c`. -/
 320lemma meetsBands_any_default (L : Ledger) (B : Bridge L)
 321    (U : Constants.RSUnits) :
 322    MeetsBands L B (sampleBandsFor U.c) := by
 323  have h := center_in_sampleBandsFor (x:=U.c)
 324  rcases h with ⟨b, hb, hbx⟩
 325  have : evalToBands_c U (sampleBandsFor U.c) := ⟨b, hb, hbx⟩
 326  exact meetsBands_any_of_eval (L:=L) (B:=B) (X:=sampleBandsFor U.c) U this
 327
 328/-- Absolute-layer acceptance bundles UniqueCalibration with MeetsBands. -/
 329theorem absolute_layer_any (L : Ledger) (B : Bridge L) (A : Anchors) (X : Bands)
 330    (hU : UniqueCalibration L B A) (hM : MeetsBands L B X) :
 331    UniqueCalibration L B A ∧ MeetsBands L B X :=
 332  And.intro hU hM
 333
 334/-- Absolute-layer acceptance is invariant under admissible rescalings. -/
 335theorem absolute_layer_invariant {L : Ledger} {B : Bridge L} {A : Anchors} {X : Bands}
 336    {U U' : Constants.RSUnits}
 337    (hUU' : Verification.UnitsRescaled U U')
 338    (hU : UniqueCalibration L B A ∧ MeetsBands L B X) :
 339    UniqueCalibration L B A ∧ MeetsBands L B X := by
 340  have _ := hUU'.cfix
 341  exact hU
 342
 343/-- Construct the absolute-layer witness from a concrete checker. -/
 344theorem absolute_layer_from_eval_invariant {L : Ledger} {B : Bridge L}
 345    {A : Anchors} {X : Bands} {U U' : Constants.RSUnits}
 346    (hUU' : Verification.UnitsRescaled U U')
 347    (hEval : evalToBands_c U X) :
 348    UniqueCalibration L B A ∧ MeetsBands L B X := by
 349  refine absolute_layer_any (L:=L) (B:=B) (A:=A) (X:=X)
 350    (uniqueCalibration_any L B A) ?_
 351  have hEval' := (evalToBands_c_invariant (U:=U) (U':=U') hUU' X).mp hEval
 352  exact meetsBands_any_of_eval (L:=L) (B:=B) (X:=X) U' hEval'
 353
 354end RecogSpec
 355end IndisputableMonolith
 356
 357end section
 358