import PhysicsLogic.Papers.Onsager1931

open PhysicsLogic.Papers.Onsager1931
open ChemicalTriangleFormulaReadout ReciprocalRelationsFramework.Countermodels

universe u
variable {Process : Type u}

example (r : ChemicalTriangleFormulaReadout Process) : r.FormulaDomainAt ↔
    0 < r.gasConstantValue ∧ 0 < r.temperatureValue ∧
    0 < r.amountAValue ∧ 0 < r.amountBValue ∧ 0 < r.amountCValue ∧
    0 < r.equilibriumAmountAValue ∧ 0 < r.equilibriumAmountBValue ∧ 0 < r.equilibriumAmountCValue := Iff.rfl

example (r : ChemicalTriangleFormulaReadout Process) (a b c : ℝ) : r.idealFreeEnergyAt a b c =
    r.freeEnergyMinimumValue + r.gasConstantValue * r.temperatureValue *
      (a * Real.log (a / r.equilibriumAmountAValue) +
       b * Real.log (b / r.equilibriumAmountBValue) +
       c * Real.log (c / r.equilibriumAmountCValue)) := rfl

example (r : ChemicalTriangleFormulaReadout Process) : r.EquationThreeSevenAt ↔
    r.freeEnergyValue = r.freeEnergyMinimumValue + r.gasConstantValue * r.temperatureValue *
      (r.amountAValue * Real.log (r.amountAValue / r.equilibriumAmountAValue) +
       r.amountBValue * Real.log (r.amountBValue / r.equilibriumAmountBValue) +
       r.amountCValue * Real.log (r.amountCValue / r.equilibriumAmountCValue)) := Iff.rfl

example (r : ChemicalTriangleFormulaReadout Process) : r.EquationThreeEightAt ↔
    r.displacementAValue = r.amountAValue - r.equilibriumAmountAValue ∧
    r.displacementBValue = r.amountBValue - r.equilibriumAmountBValue ∧
    r.displacementCValue = r.amountCValue - r.equilibriumAmountCValue ∧
    r.amountAValue + r.amountBValue + r.amountCValue =
      r.equilibriumAmountAValue + r.equilibriumAmountBValue + r.equilibriumAmountCValue ∧
    ∀ da db dc : ℝ, da + db + dc = 0 →
      r.freeEnergyVariationValueAt da db dc = -(r.forceAValue * da) - r.forceBValue * db - r.forceCValue * dc := Iff.rfl

example (r : ChemicalTriangleFormulaReadout Process) (amount reference : ℝ) :
    r.logarithmicForceAt amount reference = -(r.gasConstantValue * r.temperatureValue * Real.log (amount / reference)) := rfl

example (r : ChemicalTriangleFormulaReadout Process) (displacement reference : ℝ) :
    r.linearizedForceAt displacement reference = -(r.gasConstantValue * r.temperatureValue * displacement / reference) := rfl

example (r : ChemicalTriangleFormulaReadout Process) : r.EquationThreeNineAt ↔
    r.forceAValue = -(r.gasConstantValue * r.temperatureValue * Real.log (r.amountAValue / r.equilibriumAmountAValue)) ∧
    HasDerivAt (fun t => -(r.gasConstantValue * r.temperatureValue *
      Real.log ((r.equilibriumAmountAValue + t * r.displacementAValue) / r.equilibriumAmountAValue)))
      (-(r.gasConstantValue * r.temperatureValue * r.displacementAValue / r.equilibriumAmountAValue)) 0 ∧
    r.forceBValue = -(r.gasConstantValue * r.temperatureValue * Real.log (r.amountBValue / r.equilibriumAmountBValue)) ∧
    HasDerivAt (fun t => -(r.gasConstantValue * r.temperatureValue *
      Real.log ((r.equilibriumAmountBValue + t * r.displacementBValue) / r.equilibriumAmountBValue)))
      (-(r.gasConstantValue * r.temperatureValue * r.displacementBValue / r.equilibriumAmountBValue)) 0 ∧
    r.forceCValue = -(r.gasConstantValue * r.temperatureValue * Real.log (r.amountCValue / r.equilibriumAmountCValue)) ∧
    HasDerivAt (fun t => -(r.gasConstantValue * r.temperatureValue *
      Real.log ((r.equilibriumAmountCValue + t * r.displacementCValue) / r.equilibriumAmountCValue)))
      (-(r.gasConstantValue * r.temperatureValue * r.displacementCValue / r.equilibriumAmountCValue)) 0 := Iff.rfl

example (r : ChemicalTriangleFormulaReadout Process) (a b c : ℝ) : r.forceLawRatesAt a b c =
    ![((r.rateBAValue + r.rateCAValue) * r.equilibriumAmountAValue / (r.gasConstantValue * r.temperatureValue)) * a -
      (r.rateABValue * r.equilibriumAmountBValue / (r.gasConstantValue * r.temperatureValue)) * b -
      (r.rateACValue * r.equilibriumAmountCValue / (r.gasConstantValue * r.temperatureValue)) * c,
    -(r.rateBAValue * r.equilibriumAmountAValue / (r.gasConstantValue * r.temperatureValue)) * a +
      ((r.rateABValue + r.rateCBValue) * r.equilibriumAmountBValue / (r.gasConstantValue * r.temperatureValue)) * b -
      (r.rateBCValue * r.equilibriumAmountCValue / (r.gasConstantValue * r.temperatureValue)) * c,
    -(r.rateCAValue * r.equilibriumAmountAValue / (r.gasConstantValue * r.temperatureValue)) * a -
      (r.rateCBValue * r.equilibriumAmountBValue / (r.gasConstantValue * r.temperatureValue)) * b +
      ((r.rateACValue + r.rateBCValue) * r.equilibriumAmountCValue / (r.gasConstantValue * r.temperatureValue)) * c] := rfl

example (r : ChemicalTriangleFormulaReadout Process) (a b c : ℝ) : r.massActionRatesAt a b c =
    ![-(r.rateBAValue + r.rateCAValue) * a + r.rateABValue * b + r.rateACValue * c,
      r.rateBAValue * a - (r.rateABValue + r.rateCBValue) * b + r.rateBCValue * c,
      r.rateCAValue * a + r.rateCBValue * b - (r.rateACValue + r.rateBCValue) * c] := rfl

example (r : ChemicalTriangleFormulaReadout Process) : r.EquationThreeTenAt ↔
    r.massActionRatesAt r.equilibriumAmountAValue r.equilibriumAmountBValue r.equilibriumAmountCValue = (fun _ => 0) ∧
    ![r.displacementRateAValue, r.displacementRateBValue, r.displacementRateCValue] =
      r.forceLawRatesAt (r.linearizedForceAt r.displacementAValue r.equilibriumAmountAValue)
        (r.linearizedForceAt r.displacementBValue r.equilibriumAmountBValue)
        (r.linearizedForceAt r.displacementCValue r.equilibriumAmountCValue) := Iff.rfl

example (r : ChemicalTriangleFormulaReadout Process) : r.SourceFormulaAt ↔
    r.FormulaDomainAt ∧ r.EquationThreeSevenAt ∧ r.EquationThreeEightAt ∧
      r.EquationThreeNineAt ∧ r.EquationThreeTenAt := Iff.rfl

example : equilibriumChemicalTriangleFormula = { wrongChemicalTriangleFormula with freeEnergyValue := 0 } := rfl
example : wrongChemicalTriangleFormula = {
    selectedProcess := (), gasConstantValue := 1, temperatureValue := 1,
    freeEnergyMinimumValue := 0, freeEnergyValue := 1,
    amountAValue := 1, amountBValue := 1, amountCValue := 1,
    equilibriumAmountAValue := 1, equilibriumAmountBValue := 1, equilibriumAmountCValue := 1,
    displacementAValue := 0, displacementBValue := 0, displacementCValue := 0,
    freeEnergyVariationValueAt := fun _ _ _ => 0,
    forceAValue := 0, forceBValue := 0, forceCValue := 0,
    rateABValue := 1, rateBAValue := 1, rateACValue := 1, rateCAValue := 1, rateBCValue := 1, rateCBValue := 1,
    displacementRateAValue := 0, displacementRateBValue := 0, displacementRateCValue := 0 } := rfl

example (s : ℝ) : displacedChemicalTriangleFormula s = { equilibriumChemicalTriangleFormula with
    freeEnergyValue := (1 + s) * Real.log (1 + s) + (2 - s) * Real.log ((2 - s) / 2)
    amountAValue := 1 + s
    amountBValue := 2 - s
    equilibriumAmountBValue := 2
    displacementAValue := s
    displacementBValue := -s
    freeEnergyVariationValueAt := fun da db _ => Real.log (1 + s) * da + Real.log ((2 - s) / 2) * db
    forceAValue := -Real.log (1 + s)
    forceBValue := -Real.log ((2 - s) / 2)
    rateBAValue := 2
    rateBCValue := 2
    displacementRateAValue := -4 * s
    displacementRateBValue := 4 * s } := rfl

example (r : ChemicalTriangleFormulaReadout Unit) : PositiveChemicalRateLaw r ↔
    r.FormulaDomainAt ∧ 0 < r.rateABValue ∧ 0 < r.rateBAValue ∧ 0 < r.rateACValue ∧
      0 < r.rateCAValue ∧ 0 < r.rateBCValue ∧ 0 < r.rateCBValue := Iff.rfl