IndisputableMonolith.Physics.PhotoelectricEffectFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Photoelectric Effect from J-Cost — A1 SM Depth
   6
   7Photoelectric effect: electrons ejected when photon energy > work function.
   8In RS: work function W corresponds to J(W/E_photon).
   9
  10At threshold: J(W/hν) = 0 → hν = W (exact threshold frequency).
  11Below threshold: J > 0 → no ejection.
  12Above threshold: J > 0 on the energy remainder.
  13
  14Five canonical photoelectric materials (alkali metals Na/K/Cs/Rb,
  15and noble metals Au/Pt) = configDim D = 5.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Physics.PhotoelectricEffectFromJCost
  21open Cost
  22
  23inductive PhotoelectricMaterial where
  24  | sodium | potassium | cesium | rubidium | gold
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem photoelectricMaterialCount : Fintype.card PhotoelectricMaterial = 5 := by decide
  28
  29/-- At threshold: J(W/hν) = 0. -/
  30theorem photoelectric_threshold : Jcost 1 = 0 := Jcost_unit0
  31
  32/-- Below threshold (hν < W): J > 0. -/
  33theorem below_threshold {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  34    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  35
  36structure PhotoelectricCert where
  37  five_materials : Fintype.card PhotoelectricMaterial = 5
  38  threshold : Jcost 1 = 0
  39  below_threshold : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  40
  41def photoelectricCert : PhotoelectricCert where
  42  five_materials := photoelectricMaterialCount
  43  threshold := photoelectric_threshold
  44  below_threshold := below_threshold
  45
  46end IndisputableMonolith.Physics.PhotoelectricEffectFromJCost
  47