IndisputableMonolith.Physics.CasimirEffectCertV2

   1import Mathlib
   2import IndisputableMonolith.Physics.CasimirEffectFromRS
   3import IndisputableMonolith.QFT.CasimirPlateModes
   4import IndisputableMonolith.QFT.CasimirRecognitionBoundary
   5
   6/-!
   7# Casimir Effect Certificate V2
   8
   9This is the master certificate for the formal Casimir lane.  It upgrades the
  10older numerology/J-cost certificates by bundling:
  11
  12* the ideal parallel-plate pressure law,
  13* the RS boundary-mode cost interpretation,
  14* the RS-native `ℏ = φ^(-5)` substitution,
  15* the existing `720 = 8 * 90` structural provenance,
  16* explicit falsifier hooks for pressure and sign tests.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Physics
  21namespace CasimirEffectCertV2
  22
  23open QFT.CasimirPlateModes
  24open QFT.CasimirRecognitionBoundary
  25
  26noncomputable section
  27
  28/-- Claim hygiene tags for this module's components. -/
  29inductive ClaimStatus where
  30  | theorem
  31  | model
  32  | hypothesis
  33  | openProblem
  34  deriving DecidableEq, Repr
  35
  36/-- Falsifier hook for the ideal pressure law: a measurement falsifies the ideal
  37model when it lies outside a declared tolerance around the predicted pressure. -/
  38structure PressureLawFalsifier where
  39  measuredPressure : ℝ
  40  predictedPressure : ℝ
  41  tolerance : ℝ
  42  tolerance_pos : 0 < tolerance
  43  falsifies : Prop := |measuredPressure - predictedPressure| > tolerance
  44
  45/-- Falsifier hook for the attraction claim: a positive pressure at positive
  46separation contradicts the ideal attractive parallel-plate model. -/
  47structure SignFalsifier where
  48  separation : PlateSeparation
  49  measuredPressure : ℝ
  50  falsifies : Prop := 0 < measuredPressure
  51
  52/-- Geometry status used by the certificate.  Only ideal parallel plates are
  53theorem-level in this first formalization pass. -/
  54def geometryStatus (cfg : CasimirEffectFromRS.CasimirConfig) : ClaimStatus :=
  55  match cfg with
  56  | CasimirEffectFromRS.CasimirConfig.parallelPlates => ClaimStatus.theorem
  57  | CasimirEffectFromRS.CasimirConfig.spherePlate => ClaimStatus.model
  58  | CasimirEffectFromRS.CasimirConfig.cylinderPlate => ClaimStatus.model
  59  | CasimirEffectFromRS.CasimirConfig.corrugated => ClaimStatus.model
  60  | CasimirEffectFromRS.CasimirConfig.sphereSphere => ClaimStatus.model
  61
  62/-- The legacy five-configuration taxonomy is retained. -/
  63theorem geometry_count_retained :
  64    Fintype.card CasimirEffectFromRS.CasimirConfig = 5 :=
  65  CasimirEffectFromRS.casimirConfigCount
  66
  67/-- The legacy structural `720 = 8 * 90` provenance is retained, but it is not
  68used as the analytic derivation of the pressure coefficient. -/
  69theorem factor_720_as_8tick_times_fermion_dof :
  70    (720 : ℕ) = 8 * 90 :=
  71  CasimirEffectFromRS.casimir_factor_8tick
  72
  73/-- The parallel-plate geometry is theorem-level in the V2 certificate. -/
  74theorem parallel_plate_status :
  75    geometryStatus CasimirEffectFromRS.CasimirConfig.parallelPlates =
  76      ClaimStatus.theorem := rfl
  77
  78/-- Corrugated geometries are model-level once the roughness algebra is
  79formalized; material response remains a separate hypothesis. -/
  80theorem corrugated_status :
  81    geometryStatus CasimirEffectFromRS.CasimirConfig.corrugated =
  82      ClaimStatus.model := rfl
  83
  84/-- Master Casimir certificate. -/
  85structure CasimirV2Cert where
  86  ideal_plate : IdealPlateCert
  87  recognition_boundary : RecognitionBoundaryCert
  88  geometry_count : Fintype.card CasimirEffectFromRS.CasimirConfig = 5
  89  factor_8tick : (720 : ℕ) = 8 * 90
  90  parallel_plate_theorem :
  91    geometryStatus CasimirEffectFromRS.CasimirConfig.parallelPlates =
  92      ClaimStatus.theorem
  93  corrugated_model :
  94    geometryStatus CasimirEffectFromRS.CasimirConfig.corrugated =
  95      ClaimStatus.model
  96
  97/-- The V2 certificate instance. -/
  98def cert : CasimirV2Cert where
  99  ideal_plate := idealPlateCert
 100  recognition_boundary := recognitionBoundaryCert
 101  geometry_count := geometry_count_retained
 102  factor_8tick := factor_720_as_8tick_times_fermion_dof
 103  parallel_plate_theorem := parallel_plate_status
 104  corrugated_model := corrugated_status
 105
 106/-- The V2 certificate is inhabited without new axioms. -/
 107theorem cert_inhabited : Nonempty CasimirV2Cert := ⟨cert⟩
 108
 109/-- Projection: the V2 certificate recovers the attractive ideal pressure law. -/
 110theorem cert_recovers_attraction (a : PlateSeparation) :
 111    idealPressure a < 0 :=
 112  cert.ideal_plate.attractive a
 113
 114/-- Projection: the V2 certificate recovers the RS boundary cost nonnegativity. -/
 115theorem cert_recovers_boundary_cost_nonneg (I : BoundaryModeInventory) :
 116    0 ≤ renormalizedBoundaryCost I :=
 117  cert.recognition_boundary.cost_nonnegative I
 118
 119/-- Projection: the V2 certificate recovers the `ℏ = φ^(-5)` pressure form. -/
 120theorem cert_recovers_phi_hbar_pressure (a : PlateSeparation) :
 121    idealPressure a =
 122      -Real.pi ^ 2 * (Constants.phi ^ (-(5 : ℝ))) * Constants.c /
 123        (240 * a.value ^ 4) :=
 124  cert.ideal_plate.hbar_phi_form a
 125
 126end
 127
 128end CasimirEffectCertV2
 129end Physics
 130end IndisputableMonolith
 131