IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples

   1/-
   2  PrimitiveRecognitionCalculus/ValidComparisonExamples.lean
   3
   4  Worked valid-comparison examples.
   5
   6  `ValidComparison.lean` proves the abstract bridge doctrine. This file supplies
   7  examples the Delta plan asks for: real display, finite probability display, and
   8  finite Hilbert display.
   9
  10  No project-local axioms. No sorry.
  11-/
  12
  13import Mathlib
  14import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison
  15import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HilbertDisplayCompletion
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22namespace ValidComparisonExamples
  23
  24/-- Real display bridge: a Delta-real protocol displays to its real value, and
  25the observable is that same value. -/
  26noncomputable def realDisplayBridge :
  27    ValidComparison.Bridge DeltaReal.Protocol ℝ ℝ where
  28  display := DeltaReal.Protocol.value
  29  observeNative := DeltaReal.Protocol.value
  30  observeDisplay := id
  31  commutes := by intro x; rfl
  32
  33theorem real_display_valid_iff (x y : DeltaReal.Protocol) :
  34    ValidComparison.IsValidComparison realDisplayBridge x y ↔ x.value = y.value :=
  35  ValidComparison.validComparison_iff_native realDisplayBridge x y
  36
  37/-- Finite probability display bridge: a native finite event displays to its
  38rational counting probability. -/
  39noncomputable def probabilityDisplayBridge (N : ℕ) :
  40    ValidComparison.Bridge (DeltaProbability.Event N) ℚ ℚ where
  41  display := DeltaProbability.prob
  42  observeNative := DeltaProbability.prob
  43  observeDisplay := id
  44  commutes := by intro E; rfl
  45
  46theorem probability_display_valid_iff (N : ℕ) (E F : DeltaProbability.Event N) :
  47    ValidComparison.IsValidComparison (probabilityDisplayBridge N) E F
  48      ↔ DeltaProbability.prob E = DeltaProbability.prob F :=
  49  ValidComparison.validComparison_iff_native (probabilityDisplayBridge N) E F
  50
  51/-- Finite Hilbert display bridge, re-exported at the valid-comparison example
  52layer. -/
  53noncomputable def hilbertNormBridge (N : ℕ) :
  54    ValidComparison.Bridge
  55      (FRSComplexAmplitude.FRSIAmp N)
  56      (HilbertDisplayCompletion.FiniteHilbertDisplay N)
  57      ℝ :=
  58  HilbertDisplayCompletion.normBridge N
  59
  60theorem hilbert_display_valid_iff (N : ℕ)
  61    (ψ φ : FRSComplexAmplitude.FRSIAmp N) :
  62    ValidComparison.IsValidComparison (hilbertNormBridge N) ψ φ
  63      ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
  64        = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i) :=
  65  ValidComparison.validComparison_iff_native (hilbertNormBridge N) ψ φ
  66
  67/-- **Valid-comparison examples headline.** The doctrine has concrete bridges for
  68real display, finite probability display, and finite Hilbert display. -/
  69theorem valid_comparison_examples_headline :
  70    (∀ x y : DeltaReal.Protocol,
  71        ValidComparison.IsValidComparison realDisplayBridge x y ↔ x.value = y.value)
  72      ∧ (∀ (N : ℕ) (E F : DeltaProbability.Event N),
  73          ValidComparison.IsValidComparison (probabilityDisplayBridge N) E F
  74            ↔ DeltaProbability.prob E = DeltaProbability.prob F)
  75      ∧ (∀ (N : ℕ) (ψ φ : FRSComplexAmplitude.FRSIAmp N),
  76          ValidComparison.IsValidComparison (hilbertNormBridge N) ψ φ
  77            ↔ Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight ψ i)
  78              = Finset.univ.sum (fun i : Fin (N + 1) => FRSComplexAmplitude.bornWeight φ i)) :=
  79  ⟨real_display_valid_iff, probability_display_valid_iff, hilbert_display_valid_iff⟩
  80
  81end ValidComparisonExamples
  82end PrimitiveRecognitionCalculus
  83end Foundation
  84end IndisputableMonolith
  85