IndisputableMonolith.Chemistry.ElectrochemicalSeriesFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Electrochemical Series from φ-ladder — Chemistry Depth
   6
   7Five canonical half-cell categories (= configDim D = 5):
   8  strong oxidizing, weak oxidizing, neutral reference (SHE),
   9  weak reducing, strong reducing.
  10
  11Standard reduction potentials span five orders of magnitude, forming a
  12φ-ladder under canonical RS rescaling.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Chemistry.ElectrochemicalSeriesFromPhiLadder
  18open Constants
  19
  20inductive HalfCellCategory where
  21  | strongOxidizing
  22  | weakOxidizing
  23  | sheReference
  24  | weakReducing
  25  | strongReducing
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem halfCellCategory_count :
  29    Fintype.card HalfCellCategory = 5 := by decide
  30
  31noncomputable def reductionPotential (k : ℕ) : ℝ := phi ^ k
  32
  33theorem potential_ratio (k : ℕ) :
  34    reductionPotential (k + 1) / reductionPotential k = phi := by
  35  unfold reductionPotential
  36  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  37  rw [div_eq_iff hpos.ne', pow_succ]
  38  ring
  39
  40theorem potential_pos (k : ℕ) : 0 < reductionPotential k :=
  41  pow_pos phi_pos k
  42
  43structure ElectrochemicalSeriesCert where
  44  five_categories : Fintype.card HalfCellCategory = 5
  45  phi_ratio : ∀ k, reductionPotential (k + 1) / reductionPotential k = phi
  46  potential_always_pos : ∀ k, 0 < reductionPotential k
  47
  48noncomputable def electrochemicalSeriesCert : ElectrochemicalSeriesCert where
  49  five_categories := halfCellCategory_count
  50  phi_ratio := potential_ratio
  51  potential_always_pos := potential_pos
  52
  53end IndisputableMonolith.Chemistry.ElectrochemicalSeriesFromPhiLadder
  54