IndisputableMonolith.Chemistry.OxidationStatesDerived

   1import Mathlib
   2import IndisputableMonolith.Chemistry.OxidationStateFromConfigDim
   3
   4/-!
   5# Derived Oxidation-State Targets
   6
   7This module is Phase 8B of the periodic-table closure plan.
   8
   9The existing `OxidationStateFromConfigDim` module proves the count-law spine.
  10This file installs the chemistry-facing target table for accessible oxidation
  11states, starting with the acceptance cases in the plan: Fe and Mn.
  12
  13The definitions are still target-level for the selected elements. The next
  14theorem must derive these lists from valence occupation plus J-cost removal.
  15-/
  16
  17namespace IndisputableMonolith.Chemistry.OxidationStatesDerived
  18
  19open IndisputableMonolith.Chemistry
  20
  21/-- Target accessible oxidation states for selected elements. -/
  22def accessibleOxidationStates (Z : Nat) : List Int :=
  23  if Z = 26 then [0, 2, 3, 6]
  24  else if Z = 25 then [-1, 0, 2, 3, 4, 6, 7]
  25  else []
  26
  27/-- Iron's accessible oxidation states in the Phase 8 target table. -/
  28theorem iron_oxidation_states :
  29    accessibleOxidationStates 26 = [0, 2, 3, 6] := by
  30  native_decide
  31
  32/-- Manganese reaches +7. -/
  33theorem manganese_max_seven :
  34    (7 : Int) ∈ accessibleOxidationStates 25 := by
  35  native_decide
  36
  37/-- The manganese target list has the canonical seven common states. -/
  38theorem manganese_state_count :
  39    (accessibleOxidationStates 25).length = 7 := by
  40  native_decide
  41
  42/-- Iron's target list has no duplicate oxidation states. -/
  43theorem iron_oxidation_states_nodup :
  44    (accessibleOxidationStates 26).Nodup := by
  45  native_decide
  46
  47/-- Manganese's target list has no duplicate oxidation states. -/
  48theorem manganese_oxidation_states_nodup :
  49    (accessibleOxidationStates 25).Nodup := by
  50  native_decide
  51
  52/-- The count-law oxidation certificate remains available. -/
  53theorem oxidation_count_law_available :
  54    Nonempty OxidationStateFromConfigDim.OxidationStateCert :=
  55  OxidationStateFromConfigDim.cert_inhabited
  56
  57/-- Phase 8B certificate: oxidation-state targets are installed. -/
  58structure OxidationStatesDerivedCert : Prop where
  59  iron_exact : accessibleOxidationStates 26 = [0, 2, 3, 6]
  60  manganese_reaches_seven : (7 : Int) ∈ accessibleOxidationStates 25
  61  manganese_count : (accessibleOxidationStates 25).length = 7
  62  iron_nodup : (accessibleOxidationStates 26).Nodup
  63  manganese_nodup : (accessibleOxidationStates 25).Nodup
  64  count_law : Nonempty OxidationStateFromConfigDim.OxidationStateCert
  65
  66/-- The Phase 8B oxidation-state target layer is certified. -/
  67theorem oxidation_states_derived_certified :
  68    OxidationStatesDerivedCert where
  69  iron_exact := iron_oxidation_states
  70  manganese_reaches_seven := manganese_max_seven
  71  manganese_count := manganese_state_count
  72  iron_nodup := iron_oxidation_states_nodup
  73  manganese_nodup := manganese_oxidation_states_nodup
  74  count_law := oxidation_count_law_available
  75
  76end IndisputableMonolith.Chemistry.OxidationStatesDerived
  77