fix: Trying to fix Canonica Ensemble Two State

[NicolaBernini]

Fixing TODO in PhysLean/StatisticalMechanics/CanonicalEnsemble/TwoState.lean

1. Generalization: Updated the twoState definition and IsFinite instance to accept two energy parameters, $E_{0}$ and $E_{1}$.

2. Partition Function:

• Replaced twoState_partitionFunction_apply_eq_one_add_exp with twoState_partitionFunction_apply, reflecting the new sum $e^{-\beta E_0} + e^{-\beta E_1}$.
• Generalized twoState_partitionFunction_apply_eq_cosh to derive the form involving $\cosh(\beta(E_1-E_0)/2)$.

3. Energy Lemmas: Updated twoState_energy_fst and twoState_energy_snd to return E₀ and E₁ respectively.

4. Probabilities:

• Added twoState_probability_fst for the ground state probability.
• Generalized twoState_probability_snd for the excited state probability.
• Implemented robust proofs using variable substitution ($x = \beta(E_1-E_0)/2$, $C = \beta(E_0+E_1)/2$) to cleanly handle the algebraic simplification of exponential and hyperbolic functions.

5. Mean Energy: Updated twoState_meanEnergy_eq to the general form: $\frac{E_0+E_1}{2} - \frac{E_1-E_0}{2} \tanh(\beta \frac{E_1-E_0}{2})$.

6. Cleanup: Removed the TODO item.

[jstoobysmith]

Many thanks for this and your other PRs, really appreciate seeing them :). I've approved and will merge in a bit.

[jstoobysmith]

Merged.

[NicolaBernini]

Many thanks for this and your other PRs, really appreciate seeing them :). I've approved and will merge in a bit.

My pleasure to be able to help on such a great project