IndisputableMonolith.QFT.CasimirRecognitionBoundary

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.QFT.CasimirPlateModes
   4
   5/-!
   6# Casimir Recognition Boundary
   7
   8Recognition Science reads the Casimir effect as a boundary-mode inventory
   9imbalance.  Conducting plates restrict admissible modes inside the gap; the
  10renormalized cost-gradient of that restricted inventory is the pressure.
  11
  12This module proves the structural statements and keeps the electromagnetic
  13boundary identification as a named bridge hypothesis.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace QFT
  18namespace CasimirRecognitionBoundary
  19
  20open Cost
  21open CasimirPlateModes
  22
  23noncomputable section
  24
  25/-- A boundary-mode inventory compares the admissible interior mode weight with
  26an exterior/reference mode weight. -/
  27structure BoundaryModeInventory where
  28  interior : ℝ
  29  exterior : ℝ
  30  interior_pos : 0 < interior
  31  exterior_pos : 0 < exterior
  32
  33/-- The raw inventory deficit: exterior admissible weight minus interior
  34admissible weight.  Positive deficit is the parallel-plate Casimir case. -/
  35noncomputable def modeInventoryDeficit (I : BoundaryModeInventory) : ℝ :=
  36  I.exterior - I.interior
  37
  38/-- The positive exterior/interior ratio seen by the canonical reciprocal cost. -/
  39noncomputable def inventoryRatio (I : BoundaryModeInventory) : ℝ :=
  40  I.exterior / I.interior
  41
  42/-- Renormalized RS boundary cost for the inventory mismatch. -/
  43noncomputable def renormalizedBoundaryCost (I : BoundaryModeInventory) : ℝ :=
  44  Jcost (inventoryRatio I)
  45
  46/-- The inventory ratio is positive. -/
  47theorem inventoryRatio_pos (I : BoundaryModeInventory) :
  48    0 < inventoryRatio I := by
  49  unfold inventoryRatio
  50  exact div_pos I.exterior_pos I.interior_pos
  51
  52/-- Renormalized boundary cost is nonnegative. -/
  53theorem renormalizedBoundaryCost_nonneg (I : BoundaryModeInventory) :
  54    0 ≤ renormalizedBoundaryCost I := by
  55  unfold renormalizedBoundaryCost
  56  exact Jcost_nonneg (inventoryRatio_pos I)
  57
  58/-- Equal interior/exterior inventories have zero boundary cost. -/
  59theorem renormalizedBoundaryCost_eq_zero_of_balanced
  60    (I : BoundaryModeInventory) (h : I.exterior = I.interior) :
  61    renormalizedBoundaryCost I = 0 := by
  62  unfold renormalizedBoundaryCost inventoryRatio
  63  rw [h, div_self (ne_of_gt I.interior_pos)]
  64  exact Jcost_unit0
  65
  66/-- A positive inventory deficit is exactly `interior < exterior`. -/
  67theorem deficit_pos_iff (I : BoundaryModeInventory) :
  68    0 < modeInventoryDeficit I ↔ I.interior < I.exterior := by
  69  unfold modeInventoryDeficit
  70  constructor <;> intro h <;> linarith
  71
  72/-- If the exterior inventory is larger, the RS ratio exceeds one. -/
  73theorem inventoryRatio_gt_one_of_deficit_pos
  74    (I : BoundaryModeInventory) (h : 0 < modeInventoryDeficit I) :
  75    1 < inventoryRatio I := by
  76  have hlt : I.interior < I.exterior := (deficit_pos_iff I).mp h
  77  unfold inventoryRatio
  78  rw [one_lt_div I.interior_pos]
  79  exact hlt
  80
  81/-- A nonzero positive deficit gives a strictly positive recognition cost. -/
  82theorem renormalizedBoundaryCost_pos_of_deficit_pos
  83    (I : BoundaryModeInventory) (h : 0 < modeInventoryDeficit I) :
  84    0 < renormalizedBoundaryCost I := by
  85  have hratio_pos := inventoryRatio_pos I
  86  have hratio_gt : 1 < inventoryRatio I :=
  87    inventoryRatio_gt_one_of_deficit_pos I h
  88  unfold renormalizedBoundaryCost
  89  exact Jcost_pos_of_ne_one (inventoryRatio I) hratio_pos (ne_of_gt hratio_gt)
  90
  91/-- A pressure gradient is a positive outward cost-gradient with pressure
  92defined as minus that gradient. -/
  93noncomputable def pressureFromCostGradient (gradient : ℝ) : ℝ :=
  94  -gradient
  95
  96/-- Positive cost-gradient produces attractive pressure. -/
  97theorem attractive_of_positive_cost_gradient
  98    (gradient : ℝ) (hgradient : 0 < gradient) :
  99    pressureFromCostGradient gradient < 0 := by
 100  unfold pressureFromCostGradient
 101  exact neg_neg_of_pos hgradient
 102
 103/-- Bridge hypothesis: electromagnetic conducting-boundary admissibility is
 104represented by a boundary-mode inventory, and its regularized energy gradient
 105matches the RS boundary-cost gradient. -/
 106structure EMRecognitionBoundaryBridge where
 107  inventory : PlateSeparation → BoundaryModeInventory
 108  costGradient : PlateSeparation → ℝ
 109  inducedPressure : PlateSeparation → ℝ
 110  admissibility_matches_inventory : Prop
 111  regularized_energy_matches_cost_gradient :
 112    ∀ a : PlateSeparation, inducedPressure a = pressureFromCostGradient (costGradient a)
 113
 114/-- Under the bridge, a positive cost-gradient at a separation gives attractive
 115pressure at that separation. -/
 116theorem bridge_attractive_of_positive_gradient
 117    (B : EMRecognitionBoundaryBridge) (a : PlateSeparation)
 118    (hgradient : 0 < B.costGradient a) :
 119    B.inducedPressure a < 0 := by
 120  rw [B.regularized_energy_matches_cost_gradient a]
 121  exact attractive_of_positive_cost_gradient (B.costGradient a) hgradient
 122
 123/-- Structural certificate for the RS boundary interpretation. -/
 124structure RecognitionBoundaryCert where
 125  cost_nonnegative :
 126    ∀ I : BoundaryModeInventory, 0 ≤ renormalizedBoundaryCost I
 127  balanced_zero :
 128    ∀ I : BoundaryModeInventory,
 129      I.exterior = I.interior → renormalizedBoundaryCost I = 0
 130  deficit_positive_cost :
 131    ∀ I : BoundaryModeInventory,
 132      0 < modeInventoryDeficit I → 0 < renormalizedBoundaryCost I
 133  positive_gradient_attractive :
 134    ∀ gradient : ℝ, 0 < gradient → pressureFromCostGradient gradient < 0
 135
 136/-- Certificate for the theorem-level part of the boundary-mode reading. -/
 137def recognitionBoundaryCert : RecognitionBoundaryCert where
 138  cost_nonnegative := renormalizedBoundaryCost_nonneg
 139  balanced_zero := renormalizedBoundaryCost_eq_zero_of_balanced
 140  deficit_positive_cost := renormalizedBoundaryCost_pos_of_deficit_pos
 141  positive_gradient_attractive := attractive_of_positive_cost_gradient
 142
 143end
 144
 145end CasimirRecognitionBoundary
 146end QFT
 147end IndisputableMonolith
 148