IndisputableMonolith.Physics.OpticsSnellsLawFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Snell's Law from RS — B14 Optics Depth
   6
   7Snell's law: n₁ sin θ₁ = n₂ sin θ₂.
   8In RS: refraction ratio r = n₂/n₁ ↔ J(r) cost.
   9
  10At r = 1 (same medium): J = 0, no bending.
  11At r ≠ 1 (different media): J > 0, light bends.
  12
  13Five canonical optical phenomena (reflection, refraction, diffraction,
  14interference, polarisation) = configDim D = 5.
  15
  16Lean: 5 phenomena, J = 0 at equal media.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith.Physics.OpticsSnellsLawFromRS
  22open Cost
  23
  24inductive OpticalPhenomenon where
  25  | reflection | refraction | diffraction | interference | polarisation
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem opticalPhenomenonCount : Fintype.card OpticalPhenomenon = 5 := by decide
  29
  30/-- Same medium: J = 0 (no bending). -/
  31theorem same_medium : Jcost 1 = 0 := Jcost_unit0
  32
  33/-- Different media: J > 0 (bending occurs). -/
  34theorem different_media {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  35    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  36
  37/-- Refraction is symmetric: J(n₂/n₁) = J(n₁/n₂). -/
  38theorem refraction_symmetric {r : ℝ} (hr : 0 < r) :
  39    Jcost r = Jcost r⁻¹ := Jcost_symm hr
  40
  41structure OpticsCert where
  42  five_phenomena : Fintype.card OpticalPhenomenon = 5
  43  same_medium_zero : Jcost 1 = 0
  44  bending_positive : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  45
  46def opticsCert : OpticsCert where
  47  five_phenomena := opticalPhenomenonCount
  48  same_medium_zero := same_medium
  49  bending_positive := different_media
  50
  51end IndisputableMonolith.Physics.OpticsSnellsLawFromRS
  52