feat(CondensedMatter): add the thermoelectric figure of merit#1440
feat(CondensedMatter): add the thermoelectric figure of merit#1440gbarbalinardo wants to merge 3 commits into
Conversation
…nductivity, figureOfMerit with positivity and monotonicity lemmas Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.8 <no-reply+claude-opus-4-8@anthropic.com>
|
Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally. If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks. If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip. Important: If a reviewer adds an |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Many thanks for this first pull request. It looks great. I just left a comment that will hopefully make it better and hopefully make it easier going forward to do things with this.
|
It may be worth defining a structure which contains the basic properties of a theormelectric material, which, from what you've written here, looks like the seedback coefficient, the electrical conductivity, and the lattice and electronic contributions to the conductivity. It would be good if you could make a structure and base everything else in this file on that structure, and then ideally, if you can justify why those parameters need to be in that structure. Are they somehow fundamental to an thermoelectric material? I think that would really illuminate what's in this file. |
jstoobysmith
added
the
awaiting-author
Collect the four linear-response transport coefficients (S, sigma, kappa_l, kappa_e) into a ThermoelectricMaterial structure with their physical sign constraints as fields, following the HarmonicOscillator idiom. Restate powerFactor, totalThermalConductivity, figureOfMerit and all lemmas on the structure; temperature stays an argument since it is a state variable, not a material property. The module docstring records why exactly these four coefficients characterize a thermoelectric material. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Monotonicity in the lattice thermal conductivity needs only a nonnegative numerator: drop the Seebeck nonzeroness hypothesis and weaken 0 < T to 0 <= T, with the docstring noting why. Record in the module docstring that a ThermoelectricMaterial is a material at an operating point, since real transport coefficients are themselves temperature-dependent. Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
|
@gbarbalinardo Welcome to physlib!! FYI if you are ready for your PR to be reviewed once again please comment (-)(awaiting-author) (without the brackets) |
3 participants
This PR adds the thermoelectric figure of merit zT, together with the two quantities needed to state it, all in the new
Physlib/CondensedMatter/Thermoelectric/Basic.lean:powerFactor: the power factor PF = sigma S^2 of a material with Seebeck coefficient S and electrical conductivity sigma.totalThermalConductivity: kappa_l + kappa_e, lattice plus electronic contributions.figureOfMerit: zT = PF * T / (kappa_l + kappa_e).Lemmas:
powerFactor_pos: PF > 0 for a conductor with a nonzero Seebeck coefficient.totalThermalConductivity_pos: positivity when the lattice part is positive and the electronic part nonnegative.figureOfMerit_eq: the standard flat form zT = sigma S^2 T / (kappa_l + kappa_e).figureOfMerit_pos: zT > 0 under the physical hypotheses above at positive temperature.figureOfMerit_le_of_le: lowering the lattice thermal conductivity raises zT, all else fixed (the phonon-glass electron-crystal design principle).References: Ioffe, Semiconductor Thermoelements and Thermoelectric Cooling (1957); Snyder and Toberer, Complex thermoelectric materials, Nature Materials 7, 105-114 (2008).