Defining State_I as the state at energy level \epsilon(I)

[marta zhango]

How can I define State_I as the state at energy level \epsilon(I)} ?

State_I \in {energy_level : energy_level = \epsilon(I)}

[marta zhango]

Energy_Condition == \A I \in 1..n, k \in 1..m, l \in 1..L :
State_I \in {energy_level : energy_level = \epsilon(I)} => N[I][k] >= 0
/\ Microstates[I][k] \subseteq {microstate : microstate at energy level I}

I The energy level
k The macrostate
l The microstate

[Stephan Merz]

TLA+ has bounded set comprehension:

{ x \in S : P(x) }

Unbounded comprehension is disallowed: this helps making the definition of Russell’s “set” illegal. 

Stephan

--

Stephan Merz

On 29 Apr 2024, at 03:23, marta zhango <marta...@gmail.com> wrote:

How can I define State_I as the state at energy level \epsilon(I)} ?

State_I \in {energy_level : energy_level = \epsilon(I)}

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/643c7e96-552f-4ae5-ba67-84a2f2c390d3n%40googlegroups.com.

[marta zhango]

Would that translate to something like

{ s \in S :  \A i \in 1..n, k \in 1..m, j \in 1..p : E_i = \epsilon(i)} }

to mean the state s in S such that the energy of s is \epsilon(i)

for m macrostates and p microstates.

[Stephan Merz]

I presume that should be E_i(s)? But then, I don’t understand the quantifiers, and the bound variables k and j appear nowhere in your definition?

Stephan

On 29 Apr 2024, at 10:09, marta zhango <marta...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81197891-9342-4c88-867b-b47d47ad1068n%40googlegroups.com.

[marta zhango]

Correct, energy level i of some particular state.  E_i(s)

Each state has n energy levels.  There are also m macrostates at each

energy level i, and each macrostate can have p possible microstates.

How would I define them ?

[Stephan Merz]

It sounds like the macro- and microstates should also be parameters of the relevant operators (E and possibly epsilon). In formal mathematics, you cannot leave parameters implicit as it is sometimes done on a whiteboard or perhaps on paper: the machine is unforgiving and will not figure out what is implicit. This is not specific to TLA+ but also true of Coq, Isabelle or Lean. 

I am not sure about the quantifiers, however: do you really mean E(i,s,…) to be the same value for all parameters? Of course, a definition is never wrong: it may simply not represent what you have in mind, and the good thing about formal mathematics is that you can play with your definitions and find out if they say what you mean. 

Stephan

On 29 Apr 2024, at 15:58, marta zhango <marta...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4ba993d8-c1cc-4a65-9e9e-c2328bd9f138n%40googlegroups.com.

[marta zhango]

I want to define the number of particles N at energy level E_i for a given microstate

p within macrostate k.

[marta zhango]

Specifically I compute the average number of particles at energy level i.

Here, Sum(k, ...) represents the summation over all possible values of k.

N[i][k] represents the number of particles at energy level i in macrostate k.

W[i][k] represents a weight associated with macrostate k at energy level i.

C[j] represents an arbitrary microstate j within macrostate k.

N[i][g] == LET numerator == Sum(k, N[i][k] * W[i][k] * C[j]) denominator == Sum(k, W[i][k] * C[j]) IN numerator / denominator

[marta zhango]

N[i][g] ==

LET

numerator == Sum(k, N[i][k] * W[i][k] * C[j])

denominator == Sum(k, W[i][k] * C[j])

IN

numerator / denominator

[marta zhango]

Basically what I have is this

macrostates == {k \in 1..m} \* macrostate k,
microstates[k] == {j \in 1..p} \* Microstates for macrostate k

energy_levels == 1..n \* Set of energy levels

macrostate_energy[k] == i \in energy_levels \* Energy level of macrostate k

Finally I want to define the number of occurrences of microstate j having
macrostate_energy[k]. Nij