Obrad Kasum

Boban Veličković

Marginalia to a Theorem of Asperó and Schindler

We describe a general method for adding a model of an infinitary propositional formula by stationary set preserving forcing. As a consequence we obtain a somewhat different proof of the Asperó-Schindler theorem stating that MM ++ implies Woodin's axiom ( * ).

Introduction

Overview

An infinitary propositional formula differs from a finitary one in that one can use conjunctions and disjunctions of arbitrary length. One can then go on to adjust the Natural Deduction rules to get a proof theory for these longer formulas. Proofs will now be infinite wellfounded trees. In this way, we achieve a straightforward generalization of the notion of coherence: a formula is coherent iff it does not prove the contradiction. However, the usual completeness theorem requires a slight adjustment: a formula is coherent if and only if it has a model in some generic extension of the universe. We will not need this syntactic notion of coherence, so we will just focus on the notion of "having a model in a generic extension". Definition 1.1. Suppose that w is an infinitary propositional formula or a set thereof. Then w is consistent iff there exists a poset P such that V P |= "there exists a model for w".

What we want to study here is a strengthening of this notion, which we call the ssp1 consistency. The idea is that even if a model of a formula can be added to the universe by some forcing, it might not be possible to do so by a stationary set preserving poset. Definition 1.2. Suppose that ϕ is an infinitary propositional formula. Then ϕ is ssp consistent iff there exists a stationary set preserving poset P such that V P |= "there exists a model for ϕ".

In this paper, we give a sufficient condition for a formula to be ssp consistent (cf. Proposition 2.16). This condition is inspired by [START_REF] Asperó | Martin's maximum ++ implies woodin's axiom ( * )[END_REF] and we use it to reprove2 their main result. In the cited paper, the authors prove that the forcing axiom MM ++ of [START_REF] Foreman | Martin's maximum, saturated ideals, and nonregular ultrafilters[END_REF] implies the axiom ( * ) of [START_REF] Woodin | The axiom of determinacy, forcing axioms, and the nonstationary ideal[END_REF]. We will briefly describe what they do and how that relates to our result. Let us assume MM ++ . By [START_REF] Steel | PFA implies AD L(R)[END_REF], we have that L(R) |= AD, so to verify ( * ), we need to find (in V ) an L(R)-generic filter g for P max such that L(P(ω 1 )) = L(R) [g]. By standard facts from [START_REF] Woodin | The axiom of determinacy, forcing axioms, and the nonstationary ideal[END_REF], we know that if this is true, then for any A ⊆ ω 1 satisfying ω

L[A] 1 = ω 1 , the set g A := {p ∈ P max : ∃I, I M I ω 1 = NS ω1 ∩ M I ω1 , a M I ω 1 = A}
is an L(R)-generic filter for P max and satisfies L(R)[g A ] = L(P(ω 1 )). Here, I is intended to denote a generic iteration of p of length ω 1 + 1, M I α denotes the α th iterate in I, I M I α its ideal, and a M I α its distinguished set of ordinals (for all α ≤ ω 1 ).

This means that we may immediately fix a set A ⊆ ω 1 satisfying ω

L[A] 1
= ω 1 and work towards showing that g A is an L(R)-generic filter. It is again more or less standard to verify that g A is a filter, which leaves the L(R)-genericity as a hard part. To see this, we pick an arbitrary D ∈ L(R) which is a dense subset of P max and take upon ourselves to find p ∈ D so that there exists an (ω 1 + 1)-iteration I thereof satisfying

I M I ω 1 = NS ω1 ∩ M I ω1 and a M I ω 1 = A.
By generic absoluteness of the type of [START_REF] Bagaria | Bounded forcing axioms as principles of generic absoluteness[END_REF], we know that it suffices to find such a P max condition in a stationary set preserving generic extension3 of V . The point of this in our case is that we can approach the problem by first figuring out how to code what we need by an infinitary propositional formula and then figure out how to add a model for that formula by a stationary set preserving poset. We will give more details in Section 3. Our method is most likely sufficiently general to cover not only the construction of [START_REF] Asperó | Martin's maximum ++ implies woodin's axiom ( * )[END_REF], but also its variations that have already appeared in the literature (for example, [START_REF] Lietz | Forcing "NS ω1 is ω 1 -dense" from Large Cardinals[END_REF]). Ben De Bondt plans to include an application of the method in his forthcoming thesis [DBar]. In addition to this, the method has the advantage of using real models as side conditions for the poset, as opposed to "potential" models of [START_REF] Asperó | Martin's maximum ++ implies woodin's axiom ( * )[END_REF]. By virtue of this, it is possible to describe a local club of models for which the poset is semiproper (cf. Propositions 2.14 and 2.15). This information is relevant if one tries to iterate posets of this kind (cf. the iteration construction of [START_REF] Kasum | Iterating semi-proper forcing using virtual models[END_REF]).

Consistency

The consistency was defined as having a model in a generic extension and we observed that this is equivalent to not proving the contradiction. It is also possible to characterize the consistency in terms of a game. This characterization inspires the proof of our result on the ssp consistency.

Notation 1.3. Suppose that w is as set of infinitary propositional formulas. Then L(w) denotes the set of propositional letters appearing in w and w↓ denotes the set of subformulas of all formulas in w.

The following definition is based on [Vää11, Section 8.3]. We remind the reader that "negation normal form" of a formula is the form in which negations appear next to propositional letters. This is easily achieved in general since negations can always be pushed "all the way in". Definition 1.4. Suppose that w is a set of infinitary propositional formulas in negation normal form. Then G(w) is length ω game played as follows.

a. Set first w -1 := w.

b. In the round n < ω, Player I plays Q n and Player II answers by

w n ⊇ w n-1 . c. If Q n = ϕ ∈ w n-1 where ϕ ≡ i∈I ψ i , then for some i ∈ I, ψ i ∈ w n . d. If Q n = (ϕ, i) ∈ w n-1 × I, where ϕ ≡ i∈I ψ i , then ψ i ∈ w n .
e. The first player to break the rules loses.

f. Infinite plays according to the rules where n<ω w n

does not contain both an atomic formula and its negation, are won by Player II, while all other infinite plays are won by Player I.

Note that the above game is closed for Player II. In particular, which player wins the game is absolute between V and its generic extensions.

Proposition 1.5. Suppose that w is a set of infinitary propositional formulas in negation normal form. Then the following are equivalent. a. w is consistent. b. V Col(ω,w↓) |= "there exists a model for w".

c. Player II wins G(w).

Proof. This follows by the proof of [START_REF] Väänänen | Models and games[END_REF]Theorem 8.12]. The point is that once w↓ is collapsed to be countable, we are in the scenario of the quoted theorem. Since the game is closed, it is generically absolute whether or not Player II wins.

There is a canonical poset that adds a model of a consistent formula. We will later transform this poset into a stationary set preserving poset which adds a model of a formula (satisfying certain requirements).

Definition 1.6. Suppose that ϕ is an infinitary propositional formula in negation normal form. The poset H(ϕ) is defined as follows.

a. w ∈ H(ϕ) iff ϕ ∈ w ⊆ ϕ↓ and w is finite and consistent. b. w ≤ H(ϕ) z iff w ⊇ z.

Proposition 1.7. Suppose that ϕ is an infinitary propositional formula in negation normal form. Then ϕ is consistent if and only if H(ϕ) ̸ = ∅. In that case, if g is V -generic for H(ϕ) and

µ g : L({ϕ}) → 2 : p → 1, p ∈ g 0, p ̸ ∈ g , then µ g is a model for ϕ.
Proof. The first part is obvious. The second part follows by induction on the complexity of ϕ. We show that for a subformula ψ of ϕ, we have that µ g (ψ) = 1 if and only if ψ ∈ g.

SSP Consistency

Putative Poset

Let us immediately fix the scenario in which we work.

Declaration 2.1. Suppose that ϕ is a consistent infinitary propositional formula in negation normal form and that κ > rank(ϕ) is inaccessible.

We want to give a sufficient condition for ϕ to be ssp consistent. Furthermore, we want to find an ssp poset which adds a model for ϕ. A poset that might work was proposed by Ben De Bondt and Boban Veličković. For the rest of this subsection, we essentially reproduce their definition. f. For all M ≺ M |= ZFC -and for all λ ∈ Ord, we denote by M ↓λ the image of M under the transitive collapse of Hull(M, V λ ).

Notation 2.2. a. H := H(ϕ) b. E := {λ < κ : ϕ ∈ V λ ≺ V κ } c. For all λ ∈ E, C λ denotes the set of all countable M satisfying 4 i. M ≺ M |= ZFC -, ii. M = Hull(M, V λ ), iii. ϕ, V λ ∈ M .
Remark 2.3. If M ∈ C λ and if ξ ∈ λ ∩ E, then we do not know a priori that M ↓ξ ∈ C ξ .
The poset will be defined in two steps. The first step is to isolate the set P * λ of pre-conditions (for all λ ∈ E ∪ {κ}).

Definition 2.4. Suppose that p, q ∈ H × C [0,κ] and λ ∈ E ∪ {κ}. Then we define the following.

a. (w p , M p ) := p b. p↾λ := (w p , {M ∈ M p : λ M < λ}) c. p ∈ P * λ iff for all M, N ∈ M p , i. λ M < λ, ii. δ M = δ N =⇒ M = N , iii. δ M < δ N =⇒ M ∈ N ∧ λ M < λ N .
d. p ≤ q iff w p ⊇ w q and for all N ∈ M q , there exists M ∈ M p such that δ M = δ N , λ M = λ N , and M ⊇ N . Now that we have the sets of pre-conditions, we recursively define the family (P λ : λ ∈ E ∪ {κ}) of posets. The final poset P κ is the one that we are interested in.

Recursive Hypothesis 2.5. Suppose that

1. λ ∈ E ∪ {κ}, 2. (P ξ : ξ ∈ λ ∩ E) is defined, 3. for all ξ ∈ λ ∩ E, P ξ is a suborder of (P * ξ , ≤) and for all p ∈ P ξ , M p ⊆ C <ξ .
The following game is a modification of the game in Definition 1.4. It is used to pick the conditions among pre-conditions. c. If Q n = ϕ ∈ w pn-1 where ϕ ≡ i∈I ψ i , then for some i ∈ I, ψ i ∈ w pn .

d. If Q n = (ϕ, i) ∈ w pn-1 × I, where ϕ ≡ i∈I ψ i , then ψ i ∈ w pn . e. If Q n = (M, D) where M ∈ M pn-1 and D ∈ M is dense in P λ M , then
there exists q ∈ D such that δ(Hull(M, q)) = δ(M ) and p n ≤ p n-1 , q.

f. The first player to break the rules loses.

g. Infinite plays according to the rules where n<ω w pn does not contain both an atomic formula and its negation, are won by Player II, while all other infinite plays are won by Player I.

Definition 2.7. P λ is the suborder of (P * λ , ≤) consisting of those p ∈ P * λ for which Player II wins G λ (p).

Proposition 2.8. Recursive Hypothesis 2.5. is verified at λ.

AS goodness

The following criterion is implicit in [START_REF] Asperó | Martin's maximum ++ implies woodin's axiom ( * )[END_REF] (hence the name AS). In stating it, recall that we have already fixed a formula ϕ and an inaccessible κ > rank(ϕ). Definition 2.9. ϕ is AS good at κ iff for all stationary S ⊆ ω 1 , it holds in V Col(ω,<κ) that for all µ |= ϕ, there exist elementary τ :

V → W and μ |= τ (ϕ) such that crit(τ ) = ω V 1 ∈ τ (S)
and for all ψ ∈ ϕ↓, μ(τ (ψ)) = µ(ψ). We want to show that if ϕ is AS good, then it is ssp consistent. In fact, we will show that if ϕ is AS good, then the poset P κ is a stationary set preserving poset that adds a model for ϕ. We first list some basic properties of the posets introduced in the previous subsection. They are verified in a routine manner.

Proposition 2.10. Suppose that λ ∈ E ∪ {κ} and ξ ∈ λ ∩ E. Then P λ ∩ P * ξ = P ξ .

Proposition 2.11. Suppose that

1. λ ∈ E ∪ {κ}, 2. p ∈ P λ , 3. q ∈ P * λ , 4. q ≥ p.
Then q ∈ P λ .

Proposition 2.12. Suppose that

1. λ ∈ E ∪ {κ}, 2. g is V -generic for P λ , 3. µ g : L(ϕ) → 2,
4. for all l ∈ L(ϕ), µ g (l) = 1 iff there exists p ∈ g such that l ∈ w p . Then µ g |= ϕ.

Proof. By induction on complexity of subformulas ψ of ϕ, we show that µ g (ψ) = 1 if and only if there exists p ∈ g such that ψ ∈ w p .

We will now identify elementary submodels of H θ for which the poset P κ is semiproper. This is important because saying that P κ is semiproper is equivalent to saying that there is a local club of countable elementary submodels of H θ for which this poset is semiproper. Definition 2.13 (De Bondt, Veličković). Suppose that

1. θ ≫ κ is regular, 2. M ≺ (H θ , ∈, κ, ϕ) is countable.
Then M is good iff for all p ∈ P κ ∩ M , there exist q ∈ P κ and λ ∈ E such that

a. q ≤ p, b. κ ∩ M ⊆ λ, c. M ↓λ ∈ M q .
Proposition 2.14 (De Bondt, Veličković). Suppose that

1. θ ≫ κ is regular, 2. M ≺ H θ is good.
Then P κ is semiproper for M .

Proof.

1 • Let p ∈ P κ ∩ M .
We want to find q ∈ P κ such that q ≤ p and that q is semigeneric for (M, P κ ).

2 • There exist λ ∈ E and q ∈ P κ such that

a. q ≤ p, b. κ ∩ M ⊆ λ, c. M ↓λ ∈ M q .
We want to show that q is semigeneric for (M, P κ ).

3 • Let r ∈ P κ and D ⊆ P κ be such that

1. r ≤ q, 2. D ∈ M , 3. D is dense in P κ , 4. r ∈ D.
We want to find s ∈ D such that a. Thus, s is as required in 3 • .

s ∥ r is P κ , b. δ(Hull(M, s)) = δ(M ).
To verify that P κ is semiproper, it suffices to check that there exists a local club of good models (cf. [FJ89, Theorem 2.1]). This is where AS goodness comes in.

Proposition 2.15. Suppose that ϕ is AS good at κ and that θ ≫ κ is regular. Then the set of all good models M ≺ H θ is a local club.

Proof.

1 • Let R be a wellordering of H θ and let H := (H θ , ∈, R, κ, ϕ). We want to

show that for all X ≺ H satisfying ω 1 ⊆ X and |X| = ω 1 , we have that club many countable M ≺ X are good.

2 • Let X ≺ H satisfying ω 1 ⊆ X and |X| = ω 1 be arbitrary. We denote by X the structure on X inherited from H.

3 • Let us assume towards contradiction that there exists a stationary S ⊆ [X] ω such that for all M ∈ S, it holds that M ≺ X and that there exists p M ∈ P κ ∩ M witnessing that M is not good.

4

• By pressing down applied to S ∋ M → p M , there exist p ∈ P κ ∩ X and stationary S ′ ⊆ S such that for all M ∈ S ′ , p witnesses that M is not good.

5

• Let e : ω 1 → X be a bijection and let

T := {α < ω 1 : e[α] ∈ S ′ , δ(e[α]) = α}.
Then T is stationary in ω 1 .

6 • Let 1. λ ∈ E be such that for all for all η < λ, κ ∩ Hull H (V η ) ⊆ λ, 2. h be V -generic for Col(ω, < κ),

3. g ∈ V [h] be V -generic for P λ containing p, 4. µ := µ g |= ϕ.
We work in V [h].

7 • Since ϕ is AS good, there exist elementary τ : V → W and μ |= τ (ϕ) such that crit(τ

) = ω V 1 ∈ τ (T )
and for all ψ ∈ ϕ↓, μ(τ (ψ)) = µ(ψ).

8 • Let N := Hull τ (H) (ω V 1 ∪ {τ (p)}) ≺ τ (H). It holds that a. N ∈ W , b. |N | W = ω, c. N ≺ τ [X] ≺ τ (X ), d. δ N = ω V 1 ∈ τ (T ).
9 • Claim. In W , there exists q ∈ τ (P κ ) such that q ≤ τ (p) and N ↓τ (λ) ∈ M q .

Proof.

1 ′ We will verify that one can take

q := (τ (w p ), τ (M p ) ∪ {N ↓τ (λ)}).
To that end, it suffices to show that q ∈ τ (P λ ).

2 ′ Assume towards contradiction that q ̸ ∈ τ (P λ ). Then there exists a winning strategy σ for Player I in G W τ (λ) (q). We will defeat this strategy in V [g], reaching a contradiction. (We use in this step that the game G W τ (λ) (q) is closed for Player II.) 3 ′ Let Player I play according to σ and let us show that Player II can play by maintaining that for all n ∈ [-1, ω), there exist r, w, P such that a. r ∈ g, b. there exists finite

F ⊆ τ [V λ ] such that P = Hull τ (H) (ω V 1 ∪ F ), c. w ⊆ τ (ϕ)↓ is finite, μ |= w, and w ∩ τ [V ] = ∅, d. p n = (τ (w r ) ∪ w, τ (M r ) ∪ {P ↓τ (λ)}).
4 ′ The above conditions are satisfied for n = -1 and p -1 = q. Let us consider n ≥ 0 and the move Q n of Player I.

5 ′ Let r, w, P be such that a. r ∈ g, b. there exists finite

F ⊆ τ [V λ ] such that P = Hull τ (H) (ω V 1 ∪ F ), c. w ⊆ τ (ϕ)↓ is finite, μ |= w, and w ∩ τ [V ] = ∅, d. p n-1 = (τ (w r ) ∪ w, τ (M r ) ∪ {P ↓τ (λ)}). 6 ′ Case. Q n = ψ ∈ w pn-1 where ψ ≡ i∈I ψ i .
Proof.

1 ′′ We have that μ |= ψ, so there exists i ∈ I such that μ |= ψ i . 2 ′′ We set p n := (w pn-1 ∪ {ψ i }, M pn-1 ).

7 ′ Case. Q n = (ψ, i) ∈ w pn-1 × I where ψ ≡ i∈I ψ i .
Proof.

1 ′′ We can take p n := (w pn-1 ∪ {ψ i }, M pn-1 ).

8 ′ Case. Q n = (P ↓τ (λ), D) where D ∈ P ↓τ (λ) is dense P τ (λ) .
Proof.

1 ′′ Let ρ : Hull(P, τ (V λ )) → P ↓τ (λ) be the transitive collapse and let

D + := ρ -1 (D) ∈ P . Then D + is dense in τ (P κ ). 2 ′′ Since D + ∈ P , there exists D+ ∈ V such that τ ( D+ ) = D + . 3 ′′ Let D := D+ ∩ V λ .
By elementarity, we have that τ ( D) = D and D is dense in P λ .

4 ′′ There exists s ∈ D ∩ g such that s ≤ r.

5 ′′ We now have that a. τ (s) ∈ τ ( D) = D, b. P ′ := Hull τ (H) (ω V 1 ∪ F ∪ {τ (s)}) satisfies δ(P ′ ) = δ(P ), c. p n := (τ (s) ∪ w, τ (M s ) ∪ {P ′ ↓τ (λ)} ∈ τ (P * λ ), d. p n ≤ p n-1 , τ (s). 9 ′ Case. Q n = (M, D) where M ∈ τ (M r ) and D ∈ M is dense P λ M .
Proof.

1 ′′ We have that D ∈ P , so there exists D ∈ V such that τ ( D) = D. 2 ′′ Let M := τ -1 (M ) ∈ M r . By elementarity of τ , we have that D ∈ M ∈ M r and that D is dense in P λ M .
3 ′′ Claim. There exist s ∈ g and t ∈ D such that s ≤ r, t and δ(Hull( M, t)) = δ( M ).

Proof.

1 ′′′ It suffices to show that the set of all s ∈ P λ satisfying that s ≤ r and that there exists t ∈ D such that s ≤ t and δ(Hull( M, t)) = δ( M ), is dense below r. 2 ′′′ Let r ′ ∈ P λ be such that r ′ ≤ r. Then there exists

M ′ ∈ M r ′ such that δ( M ′ ) = δ( M ), λ M ′ = λ M , and M ⊆ M ′ .
3 ′′′ By the existence of the appropriate strategy for G λ (r ′ ), there exists s ∈ P λ such that s ≤ r ′ and such that there exists t ∈ D satisfying s ≤ t and δ(Hull( M ′ , t)) = δ( M ′ ).

4 ′′′ We have that δ( M ) ≤ δ(Hull( M, t)) ≤ δ(Hull( M ′ , t)) ≤ δ( M ′ ) = δ( M ),
which shows that all of the above values are equal and consequently, s ≤ r ′ is as required.

4 ′′ Let P ′ := Hull τ (H) (ω V 1 ∪ F ∪ {τ (s)})
and let

p n := (τ (w s ) ∪ w, τ (M s ) ∪ {P ′ ↓τ (λ)}) ∈ τ (P * λ ).
Note that δ

P ′ = ω V 1 . 5 ′′ We have τ (t) ∈ D and p n ≤ τ (t), while δ(Hull(M, τ (t))) = δ(τ (Hull( M, t))) = δ(Hull( M, t)) = = δ( M ) = δ(M ).
10 ′ We have shown that Player II can survive ω steps against the strategy σ, which is a contradiction. 10 • Having proven the claim, we conclude that in W , τ (p) cannot be a witness that N is not good.

11 • Since δ N = ω V 1 ∈ τ (T )
, we have that N ∈ τ (S ′ ), which contradicts the previous point.

Corollary 2.16. Suppose that ϕ is AS good at κ. Then P κ is spp and for all V -generic g ⊆ P κ , we have that µ g |= ϕ. In particular, ϕ is ssp consistent.

Forcing P max conditions

In this section, we aim to describe how our general method gives rise to another solution to the main problem of [START_REF] Asperó | Martin's maximum ++ implies woodin's axiom ( * )[END_REF]. In Declaration 3.2, we fix the background assumptions. Definition 3.1. Suppose that θ is a cardinal and Γ ⊆ P(R). Then Γ is θ-well behaved iff a. for all A ∈ Γ, A is θ-universally Baire, b. for all A ∈ Γ, for all formulas ϕ(x, Ȧ) projective in Ȧ, we have

B := {x ∈ R : ϕ(x, A)} ∈ Γ and V Col(ω,θ) |= B Ġ = {x ∈ R Ġ : ϕ(x, A Ġ)}. Declaration 3.2. Suppose that 1. NS ω1 is saturated, 2. 2 ω1 = ω 2 , 3. MA ω1 holds, 4. D is dense in P max ,
5. for all θ, there exists θ-well behaved Γ such that D is coded by a set in Γ,

6. A ⊆ ω 1 satisfies ω L[A] 1 = ω 1 .
Our goal is to construct an ssp poset P such that in V P , there exist generic iterations I and J of P max conditions of length ω 1 + 1 such that a.

M J 0 ∈ D Ġ, b. I↾ω M J 0 1 witnesses that M J 0 < M I 0 , c. π J (I↾ω M J 0 1 ) = I, d. M I ω1 = (H ω2 , ∈, NS ω1 , A) V , e. NS ω1 ∩ P(ω 1 ) M J ω 1 = I M J ω 1 .
We will start by forgetting for a moment about the requirement e and recasting the rest of the problem as adding a model to an infinitary propositional formula by an ssp forcing. It will turn out that we get e for free.

Notation 3.3. Suppose M = (ω, . . . ) is a structure in a recursively enumerable language. Then ϑ(M) : ω → 2 is defined in such a way that for all n < ω, for ψ denoting the formula in the language of (M, m : m < ω)

satisfying ⌜ψ⌝ = n, it holds that ϑ(M)(n) = 1 ⇐⇒ (M, m : m < ω) |= ψ. Notation 3.4. a. If E ⊆ X × Y and x ∈ X, we denote E x := {y ∈ Y : (x, y) ∈ E}.
b. If a : X → Y and x ∈ X, then a x := a(x).

We also need to fix two trees before proceeding. We are now ready to restate the goal in a way that makes it clear that we actually want to add a model to an infinitary propositional formula.

Goal 3.6. Construct an ssp poset P such that in V P , there exist E, F , I, J, a, b, u, v, π, σ, , r satisfying

a. E, F ⊆ ω 1 × (ω × ω), b. I, J ⊆ ω 1 × ω, c. a, b : ω 1 → ω, d. u, v : ω → ω 2 ,
e. for all n < ω, (ϑ(ω, E 0 , I 0 , a 0 )↾n, u↾n) ∈ T , f. for all n < ω, (ϑ(ω,

F 0 , J 0 , b 0 )↾n, v↾n) ∈ U , g. π, σ ⊆ {(α, β) : α ≤ β < ω 1 } × (ω × ω), h. for all α ≤ β < ω 1 , π α,β : (ω, E α , I α , a α ) --→ Σω (ω, E β , I β , a β ), i. for all α ≤ β ≤ γ < ω 1 , π β,γ • π α,β = π α,γ , j. for all α < ω 1 , there exists k < ω such that i. (ω, E α+1 ) |= k < ω1 ,
ii. for all q < ω, there exists < ω such that (ω, E α ) |= : ω1 → V and such that for x := π α,α+1 (), (ω, E α+1 ) |= ẋ(k) = q, iii. for g α := {w < ω : (ω, E α , I α ) |= ẇ ∈ I + α , k E α+1 π α,α+1 (w)}, we have that (ω, E α , I α , g α ) |= "g α is generic for I + α ", k. for all limit γ < ω 1 , for all n < ω, there exist α < γ and m < ω such that

π α,γ (m) = n, l. for all α ≤ β < ω 1 , σ α,β : (ω, F α , J α , b α ) --→ Σω (ω, F β , J β , b β ), m. for all α ≤ β ≤ γ < ω 1 , σ β,γ • σ α,β = σ α,γ ,
n. for all α < ω 1 , there exists k < ω such that i.

(ω, F α+1 ) |= k < ω1 ,
ii. for all q < ω, there exists < ω such that (ω, F α ) |= : ω1 → V and such that for x := σ α,α+1 (), (ω,

F α+1 ) |= ẋ(k) = q, iii. for h α := {w < ω : (ω, F α , J α ) |= ẇ ∈ J + α , k F α+1 σ α,α+1 (w)}, we have that (ω, F α , J α , h α ) |= "h α is generic for J + α ",
o. for all limit γ < ω 1 , for all n < ω, there exist α < γ and m < ω such that σ α,γ (m) = n,

p. ⊆ ω 1 × (ω × H V ω2 ),
q. for all α < ω 1 , α : (ω, E α , I α , a α ) --→

Σω (H ω2 , ∈, NS ω1 , A) V , r. for all α ≤ β < ω 1 , α = β • π α,β ,
s. for all x ∈ H V ω2 , there exist α < ω 1 and q < ω such that α (q) = x, t. r : ω 1 → (ω → ω 1 ),

u. for all α < ω 1 , r α is the ranking function of (ω, F α ).

Note that if |P| > ω 2 , then every element of p[T ] in V P will be of the form ϑ(M) for some M isomorphic to a P max -condition, but the converse might not hold. A similar remark holds for U . Now, we said that Goal 3.6 can be expressed as adding via an ssp poset a model of a certain infinitary propositional formula ϕ. Here are some examples of how to go about obtaining this ϕ.

a. Let Ėα,m,n , Ḟα,m,n , İα,m , Jα,m , ȧα,m , ḃα,m , um,ξ , vm,ξ , πα,β,m,n , σα,β,m,n , α,m,x , ṙα,m,γ be propositional letters, for all α

≤ β < ω 1 , γ < ω 1 , m, n < ω, ξ < ω 2 , x ∈ H ω2 .
b. If ψ is the language of some (ω, E α , I α , a α ), we can express (ω, E α , I α , a α ) |= ψ as a propositional formula by induction on complexity of ψ. Similarly for (ω, F α , J α , b α ).

c. We can now express requirement e as n<ω s∈T, |s|=n i<n θ s,i where i. for s(i) = (1, ξ) and for ψ i being the formula with code i, θ s,i is defined as the propositional formula asserting

"(ω, E α , I α , a α ) |= ψ i " ∧ ui,ξ ,
ii. for s(i) = (0, ξ) and for ψ i being the formula with code i, θ s,i is defined as the propositional formula asserting

"(ω, E α , I α , a α ) |= ¬ψ i " ∧ ui,ξ .
Similarly for the requirement f. d. One can proceed to successfully code all of the requirements of Goal 3.6 and obtain the formula ϕ, which will have ω 2 propositional letters and whose every conjuction and disjunction will have length at most ω 2 .

Definition 3.7. We denote by ϕ AS the negation normal form of the formula sketched just above.

The following lemma simply states that the formula ϕ AS codes that which it is designed to code. Lemma 3.8. Suppose that µ |= ϕ AS belongs to an outer model. Then in the outer model, there exist unique generic iterations I and J of P max conditions of length ω

V 1 + 1 such that a. I↾ω M J 0 1 witnesses that M J 0 < M I 0 , b. π J (I↾ω M J 0 1 ) = I, c. M I ω1 = (H ω2 , ∈, NS ω1 , A) V , d. M J 0 ∈ D g , e. for all α < ω V 1 , (ω, E α , I α , a α ) ≃ M I α and (ω, F α , J α , b α ) ≃ M J α , f. for all α ≤ β < ω V 1 , the diagrams (ω, E α , I α , a α ) (ω, E β , I β , a β ) M I α M I β π α,β ≃ ≃ π I α,β (ω, E α , I α , a α ) (H ω2 , ∈, NS ω1 , A) V M I α (H ω2 , ∈, NS ω1 , A) V α ≃ = π I α,ω V 1 (ω, F α , J α , b α ) (ω, F β , J β , b β ) M J α M J β σ α,β ≃ ≃ π J α,β commute.
Notation 3.9. In the case of the above proposition, we denote I µ := I and J µ := J . We also denote

E µ := {(α, m, n) ∈ ω V 1 × (ω × ω) : µ( Ėα,m,n ) = 1}, F µ := {(α, m, n) ∈ ω V 1 × (ω × ω) : µ( Ḟα,m,n ) = 1}, I µ := {(α, m) ∈ ω V
1 × ω : µ( İα,m ) = 1}, and so on.

We now want to show that ϕ AS is AS good. By the results of Section 2, this will give us the ssp consistency of ϕ AS . In fact, it will give us the actual poset witnessing this ssp consistency, thus allowing us to achieve Goal 3.6. We now know that the poset P κ (of Section 2) is stationary set preserving and adds a model for ϕ AS . Let g be a V -generic for P κ and let µ g := µ, I := I µ , and J := J µ . The P max -iterations I and J are like what we wanted, except the thing that we forgot about. Namely, recall that we did not code into ϕ AS the requirement that NS ω1 ∩ P(ω 1 ) M J ω 1 = I M J ω 1 .

However, we get this requirement for free, which we show in the following proposition.

Proposition 3.12. It holds in V Pκ that NS ω1 ∩ P(ω 1 ) M J µ ġ

ω 1 = I M J µ ġ ω 1 .
Proof.

1 • Let us assume otherwise. Since (⊇) clearly holds, the other inclusion must fail. More precisely, there exist p ∈ P κ , Ċ ∈ V Pκ , α < ω 1 , and m < ω such that p forces that a. (ω, F

µ ġ α ) |= " ṁ is a subset of ω 1 which is not in J µ ġ α ", b. Ċ is a club in ω V
1 , c. the image of m in the final iterate of J µ ġ has an empty intersection with Ċ ⊆ V κ . 5. h be V -generic for Col(ω, < κ), 6. g ∈ V [h] be V -generic for P λ containing p, 7. µ := µ g |= ϕ.

We work in V [h].

3 • Let S 0 be the image of m under the transitive collapse of (ω, F µ α ) and let S := π J µ α,ω V 1 (S 0 ). 4 • Let Î, Ĵ , K, τ , W , and μ be obtained as in the proof of Proposition 3.11.

(The reason why we cannot simply quote this proposition is because now S is not necessarily in V .) We have that

  d. For all S ⊆ Ord, we denote C S := λ∈S∩E C λ .e. For all M ∈ C [0,κ] , we denote by λ M the unique λ such that M ∈ C λ .

Definition 2. 6 .

 6 Suppose that p ∈ P * λ . Then G λ (p) is the game of length ω played as follows. a. Set first p -1 := p. b. In the round n < ω, Player I plays Q n and Player II answers by p n ∈ P * λ satisfying p n ≤ p n-1 .

4•

  Let ρ : Hull(M, V λ ) → M ↓λ be the transitive collapse. We have thata. ρ(D) = D ∩ V λ = D ∩ P λ , b. ρ(D) is dense in P λ , c. ρ(D) ∈ M ↓λ. 5 • Let Player I play Q 0 := (M ↓λ, ρ(D)) in G κ (r) and let Player II answer according to his strategy by p 0 . We have that for some s ∈ ρ(D), a. p 0 ∈ P κ , b. p 0 ≤ r, c. p 0 ≤ s, d. δ(Hull(M ↓λ, s)) = δ(M ↓λ). 6 • This means that a. s ∈ D, b. s ∥ p in P κ (as witnessed by p 0 ), c. δ(Hull(M, s)) = δ(Hull(M ↓λ, s)) = δ(M ↓λ) = δ(M ).

Declaration 3. 5 .

 5 Let T, U be ω 2 -absolutely complemented trees on ω × ω 2 such that a. p[T ] is the set of all ϑ(ω, E, I, a) for which there exists p ∈ P max satisfying (ω, E, I, a) ≃ p, b. p[U ] is the set of all ϑ(ω, E, I, a) for which there exists p ∈ D satisfying (ω, E, I, a) ≃ p.

  Lemma 3.10. ϕ AS is consistent.Proof. This is shown as [AS21, Lemma 3.6].Proposition 3.11. ϕ AS is AS good.Proof.1 • Let h be V -generic for Col(ω, < κ) and let us work in V [h].We fix an arbitrary valuation µ |= ϕ and an arbitrary stationary S ⊆ ω V 1 and we are going to produce elementary τ :V → W and μ |= τ (ϕ) such that crit(τ ) = ω V 1 ∈ τ (S)and for all ψ ∈ ϕ↓, μ(τ (ψ)) = µ(ψ).

  2 • Let 1. θ ≫ κ be regular, 2. R be a wellordering of H θ , 3. H := (H θ , ∈, R, κ, Ċ, T, U, A), 4. λ ∈ E be such that a. p ∈ P λ , b. for all η < λ, κ ∩ Hull H (V η ) ⊆ λ, c. V λ ≺ (V κ , ∈, P κ , Ċ).

"stationary set preserving"

Strictly speaking, our construction uses an inaccessible cardinal, while theirs does not. We believe that this additional assumption is not essential.

The set D is coded by universally Baire set of reals, so it has a canonical interpretation in any generic extension.

We use M to denote the transitive collapse of M . Models M satisfying M ≺ M |= ZFC - were called virtual models by Veličković when he used them to iterate forcing (see e.g.[START_REF] Kasum | Iterating semi-proper forcing using virtual models[END_REF])

* Mr. Kasum has received funding from the European Union's Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No. 945322

4

• For all α < ω 1 , let e α : ω → M Î α be a bijection such that if α < ω V 1 , then e α is the transitive collapse of (ω, E α ). We define for all α < ω 1 ,

In the case α < ω V 1 , we get the old Êα = E α .

5 • In the similar fashion, we extended other sets from Goal 3.6, producing the "hat versions" of them. Then the valuation μ is defined according to these "hat versions".

Proof. This requires a tedious verification. Suppose for example that ψ comes from the part s. of Goal 3.6. Then ψ might of the formula

In this case, µ(ψ) = 1, τ (ψ) is the formula

and we need to verify that τ (ψ) is evaluated as true by μ. However, this is trivial, since

). We leave it to the reader to convince herself of the rest. 7 • Thus, τ and μ are as required.

Proof. This is shown like Claim 9 • of the proof of Proposition 2.15.

7

• By elementarity, it holds in V that there exist r ∈ P λ , δ < ω 1 , and

Pκ "δ belongs to both the image of the set coded by m along the J -iteration embedding and to the club Ċ".

Proof.

1 ′ Since δ ∈ w r , it is immediate that r ⊩"δ belongs to both the image of the set coded by m along the J -iteration embedding". It remains to verify that r ⊩ δ ∈ Ċ.

2 ′ The proof of Proposition 2.14. shows that in V , r is semigeneric for (P, P κ ).

3 ′ Let g be an arbitrary V -generic for P κ containing r. We have that δ(P [ g]) = δ(P ) = δ. 4 ′ Since Ċg ∈ P [ g] is a club in ω 1 , we have that δ ∈ C, as required. 9

• The previous claim is in contradiction with 1 • c.

Finally, we arrive at the conclusion.

Corollary 3.13. The poset P κ is stationary set preserving. In V Pκ , there exist generic iterations I and J of P max conditions of length ω 1 + 1 such that a. M J 0 ∈ D Ġ, b. I↾ω


Vincent Magnin
email: vincent.magnin@univ-lille.fr

José Alves
email: jose.alves@transvalor.com

Antoine Arnoud
email: antoine.arnoud@gmail.com

Markus § Arjen
email: arjen.markus895@gmail.com

Michele Esposito
email: michele.espositomarzino@uliege.be

Modern Fortran is a standardized language that includes object-oriented and parallel programming paradigms. The Fortran-lang community, created at the end of 2019, is actively working to modernize its ecosystem. New compilers are under development. And the fourth Fortran standard of the 21st century is due to be published in autumn 2023 1 .

Genesis and classical period 1.The first optimizing compiler

With his Master's degree in mathematics, the young John Backus was hired by IBM in 1950 to work on the company's calculators. To lighten his machinelanguage programming load, he first designed an interpreter called Speedcoding for the IBM 701, featuring floating-point emulation. Then, in December 1953, he proposed the FORTRAN2 (mathematical FORmula TRANslating system) project. Machine language programming requires experts, and at least half the cost of a scientific calculation is due to their salaries (programming, testing, debugging). A high-level language would drastically reduce the amount of work required. This economic argument enabled Backus to rapidly obtain a team to work on a language and its compiler [START_REF] Backus | The FORTRAN Automatic Coding System[END_REF]. Everything had yet to be invented. While the idea of a compiled language was already in the air with Grace Hopper's work on the A-0 language, the FORTRAN compiler3 is considered to be the first optimizing compiler. The team was indeed aware that, for it to be accepted, optimal code had to be generated whatever the application. At the time, few people were prepared to believe that a machine could generate machine code as fast as that written by a human being. And von Neumann himself saw no need for a high-level language [START_REF] Jones | Abstracting Away the Machine: The History of the FORTRAN Programming Language (FORmula TRANslation)[END_REF].

The target machine was the future IBM 704, and Backus insisted that it should be the first machine to work directly with floating-point reals4 . After three years' work, the compiler was finally deployed in April 1957. It was a revolution. Mary Tsingou, physicist and mathematician at Los Alamos National Laboratory, describes the situation: "When Fortran came, it was almost like paradise" [START_REF] Grant | We thank Miss Mary Tsingou[END_REF]. Its syntax is indeed simple and adapted to scientific calculations, as its name implies. The programmer's reference manual, ready in October 1956, is 54 pages long [START_REF]Fortran -Programmer's reference manual[END_REF], so the basics of the language can be learned in a few hours. Frances Elizabeth Allen, hired at the age of 24 in July 1957, was in charge of teaching FORTRAN to IBM scientists, and the hardest part was convincing them of its usefulness and efficiency. But reading the compiler's 20,000 lines of code would guide her career. She was awarded the 2006 Turing Award "for pioneering contributions to the theory and practice of optimizing compiler techniques that laid the foundation for modern optimizing compilers and automatic parallel execution." [START_REF] Frances ; Fran") Elizabeth Allen | Turing Award[END_REF] Designed with only the IBM 704 in mind, the FORTRAN compiler quickly proved adaptable to other machines, starting with IBM's own, making it the first portable programming language. The programmer could now abstract from machine language, and the scientist could improvise as a programmer [START_REF] Jones | Abstracting Away the Machine: The History of the FORTRAN Programming Language (FORmula TRANslation)[END_REF]. So it's hardly surprising that, according to an article in the journal Nature published in 2021, this compiler is one of the ten computer codes that have most transformed science [START_REF] Perkel | Ten computer codes that transformed science[END_REF].

The first standardized language

On the downside, standardization soon became necessary to maintain the language's portability, with each compiler writer adding their own extensions. It therefore became the first language to be standardized with the FORTRAN 66 standard (ANSI X3.9-1966), which includes two versions of the language: the full language and a simplified version called Basic FORTRAN. An intermediate version, ECMA-9, was even standardized a year earlier by the ECMA (European Computer Manufacturers Association).

FORTRAN 77

The FORTRAN 77 standard (ANSI X3.9-1978), supplemented by the U.S. Department of Defense's MIL-STD-1753 extension, is a major development that facilitates structured programming in particular.

The military extension also introduces the IMPLICIT NONE instruction, which is now systematically used, to disable implicit variable typing. Indeed, by default, variables whose names start with I, J, K, L, M or N are of integer type, while all others are of real type. These are the classic loop counters i, j, k that we still use!

The language remained dominant until the late 1970s. So much so, in fact, that many artists used it to explore the new possibilities offered by the computer: for example, to create algorithmic music (Iannis Xenakis and Pierre Barbaud), graphic works (Hiroshi Kawano), poem generators and so on. And FORTRAN 77 would remain a benchmark for a long, long time to come!

A Turing Award

Among other honors, John Backus received the 1977 Turing Award "for profound, influential, and lasting contributions to the design of practical highlevel programming systems, notably through his work on FORTRAN, and for seminal publication of formal procedures for the specification of programming languages." [START_REF] Backus | [END_REF] Once the FORTRAN project was completed, he quickly moved on to other adventures. His participation in ALGOL 58 and 60 led him to work on what came to be known as the Backus-Naur Form (BNF), a formal notation for describing a programming language. Appointed IBM Fellow in 1963, he went on to work on his vision of what a functional programming style could be, his Turing reading being entitled Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs..

Modern Fortran

The expression Modern Fortran, often used in the titles of Anglo-Saxon books over the last twenty years or so [START_REF] Curcic | Modern Fortran: Building efficient parallel applications[END_REF][START_REF] Markus | Modern Fortran in Practice[END_REF][START_REF] Metcalf | Modern Fortran explained: incorporating Fortran[END_REF], has nothing official about it: some will use it from Fortran 90/95 onwards, others from Fortran 2003 onwards. It could be perceived as an oxymoron, a figure of speech common in our times, but it's not!

Fortran 90

The Fortran 90 standard, which arrived several years late, is a major revision, as suggested by the change of case from FORTRAN to Fortran. This is also its first ISO standard, managed by the international committee ISO/IEC JTC1/SC22/WG5 and the American technical committee X3J3. Among the many new features is the free form source code format, which at last makes it possible to write code without worrying about the role of certain columns inherited from punched cards (fixed form format, generally associated with the extension .f). Note that the most commonly used extension for the free format is .f90, which can be confusing for beginners, as the code can conform to any subsequent standard! Rather than defining new types, the concept of kind was introduced to define potential variants of all basic types (real, complex, integer, logical, character). For integer and real, intrinsic functions can be used to select a variant, if supported by the compiler, according to the desired numerical characteristics.

The division of source code into modules enables an embryo of objectoriented programming, with each module embedding its own data and routines, and facilitates compiler diagnostics. The public (default) and private attributes can be used to indicate whether or not an entity will be accessible outside the module. In addition, the concept of derived type allows users to define their own data structures: type person character [START_REF] Magoulès | Calcul scientifique parallèle[END_REF] :: name integer :: age real :: weight end type type ( person ) :: him = person ( " Jean " , 50 , 70.5) print * , " His name is : " , him % name Note the use of the % character instead of the classic dot to access a field in the structure. The introduction of derived types is all the more important as they will form the basis for the introduction of object-oriented programming in the Fortran 2003 standard.

Array-oriented syntax simplifies code by avoiding numerous loops. In the example below, three vectors with three components are defined5 , the sum is calculated and displayed, and a vector is calculated whose components are the square roots of the components of the first. Fortran 90 indeed introduced so-called elemental functions and procedures, which can be applied to both scalars and arrays. In addition, arrays can now be dynamically allocated. In this case, they are declared with the attribute allocatable and their dimensions are then defined later using the instruction allocate(). Occupied space can be freed with the instruction deallocate().

Pointers (attribute pointer) made their appearance in Fortran, facilitating the use of lists, trees, graphs and so on. But whereas in the C language a pointer is a memory address, the Fortran concept of a pointer is more akin to an alias. Moreover, an entity can only be pointed to if it has been declared with the attribute target or if it is itself a pointer. These properties enable compilers to generate robust, optimized code.

Finally, two new sections appear in Fortran standards: the list of obsolescent features and the list of deleted features. In practice, the latter are generally still supported by compilers, so that older code can continue to function without change.

Fortran 95

This is a minor standard that complements the previous one. Fortran 90 had introduced the possibility of allocating memory and using pointers to arrays. But these features had their limits, as the programmer had to manage memory explicitly. Fortran 95 offers much greater freedom and flexibility: automatic deallocation frees the programmer from much of the memory management, limiting memory leakage problems and allowing them to concentrate even more on what they want to do rather than on the technical details of getting there.

A function can be given the attribute pure, indicating that it produces no side effects (modification of a global variable or an argument, input/output realization, etc.) and can therefore be used without problem in a parallel computation. The programmer can also define their own elemental functions, a particular form of pure function.

As a side note, one of the methods used to evolve the language is therefore to add attributes such as elemental, pure, intent, allocatable, pointer, target. . . They also ensure the robustness of the code, enabling the compiler to perform the necessary checks for each.

Finally, the first attempt to introduce parallel computing into the language itself, forall loops will eventually be declared obsolescent in the Fortran 2018 standard, their complexity having made it difficult for compilers to implement them efficiently.

Fortran 2003

Just like Fortran 90, Fortran 2003 is a major release, as evidenced by its 585 pages, 55 % more than the previous standard. In particular, it introduces object-oriented programming (OOP) [START_REF] Rouson | Scientific software design: the object-oriented way[END_REF], based on the modules and derived types introduced by Fortran 90. A class is thus a derived type containing both data and methods, called type-bound procedures, as in this simple example: The introduction of classes makes true OOP possible: more or less inspired by the concept of class in languages such as C++ and Java, a Fortran class can be abstract (attribute abstract) or not, and can be extended (attribute extends). But one can also customize the methods of objects belonging to the same class by using procedure pointers, the syntax being similar, and thus achieve a prototype-oriented programming style [START_REF]Prototype-based programming[END_REF].

To further facilitate the construction of abstract data types such as linked lists, we can also use so-called unlimited polymorphic variables. These can be described as chameleonic, as they take on the value assigned to them, while retaining the initial type, thus maintaining safe typing [START_REF] Markus | Modern Fortran in Practice[END_REF].

Another major novelty concerns the long awaited standardization of the interoperability with the C language. This makes it easy to call C libraries in a portable way, for example to create graphical interfaces with GTK [START_REF] Vincent Magnin | gtkfortran: a GTK+ binding to build Graphical User Interfaces in Fortran[END_REF] or manage databases with SQLite [START_REF] Markus | Modern Fortran in Practice[END_REF]. Conversely, it makes it easier to write Fortran libraries for other languages, such as Python, enabling them to benefit from its computational speed and numerical precision. In practice, the new intrinsic module iso_c_binding contains constants for mapping between the data types of the two languages, as well as functions for mapping between their pointers. As the order in which multi-dimensional arrays are stored in memory is different in the two languages, the programmer must take care to reverse the order of indices when such an array is passed from one language to the other.

Both the move_alloc() procedure and implicit allocation on assignment simplify the dynamic management of allocatable objects, including reallocation.

Among the many other new features are I/O improvements (asynchronous transfers, for example), three intrinsic modules providing access to IEEE 754 standard functions (e.g. changing the microprocessor rounding mode), optional support for Unicode characters (ISO/IEC 1064619 1:2000 UCS-4), access to command-line arguments and environment variables.

Parallel Computing

Some Fortran codes are designed to run on personal computers, while others are intended to be run on supercomputers. Parallelism must therefore be managed at different scales and on different types of architectures [START_REF] Magoulès | Calcul scientifique parallèle[END_REF]: multi-core microprocessors, vectorization 6 , graphics processors (GPUs), multi-processor machines of various architectures, networked machines, etc. Setting up parallel computing standards and implementing them efficiently is therefore a difficult task.

The first attempts date back to the second half of the 80s, at a time when supercomputers were evolving from a vector model to a multi-processor model, and network computing was becoming more widespread. In 1989, PVM (Parallel Virtual Machine) [START_REF]PVM[END_REF] was one of the first solutions for parallel computing in C or Fortran on a network of heterogeneous machines (Unix/Windows).

At the end of 1991, work began on standardizing High Performance Fortran (HPF) [START_REF] Kennedy | The rise and fall of High Performance Fortran: an historical object lesson[END_REF]. With everything still to be invented, this version of the language failed to convince and never reached maturity, except in Japan, which developed its HPF/JA dialect and used it on the Earth Simulator supercomputer, the most powerful in the world from 2002 to 2004 [START_REF]Earth Simulator[END_REF]. But HPF helped to lay the foundations, and a number of seeds were sown. For example, the addition of compiler directives in comments to ensure that the program remains compilable on non-parallel machines will be found in OpenMP or OpenACC, as will the forall loops and pure attribute in Fortran 95.

The inclusion of parallel computing paradigms in the Fortran standards themselves would require an enormous amount of time and experimentation. This would have to wait until Fortran 2008 and 2018, with the considerable effort this would entail in compiler development.

External Standards

Two external standards emerged in the 90s for the C, C++ and Fortran languages [START_REF] Kennedy | The rise and fall of High Performance Fortran: an historical object lesson[END_REF]. Released in 1994, MPI (Message Passing Interface) enables parallel programming by passing messages between processes. It is designed to work with both shared-memory and distributed-memory systems. The latter may involve computers in a network, nodes in a computing cluster, etc. Powerful, but requiring the user to control inter-process communications, MPI is sometimes referred to as the assembler of parallel computing. Released in 1997, OpenMP (Open Multi-Processing) is designed for shared memory systems. Using comment directives, it enables existing code to be parallelized quite easily, if the algorithms are suitable.

The rise of GPU computing power in the 2000s led to the emergence of various systems enabling calculations to be offloaded to the many cores of these processors, including NVIDIA's CUDA (Compute Unified Device Architecture) in 2007, OpenCL 1.0 (Open Computing Language) in 2009, and OpenACC 2.0 (Open Accelerators) in 2012.

But these standards are external to Fortran. The next two standards would introduce parallel computing paradigms into the language itself.

Fortran 2008

Initially developed as an extension to Fortran 95, coarrays are officially included in the Fortran 2008 standard. Several copies of a program can be executed in parallel, either on a multi-core processor or a supercomputer. Each copy, called an image, holds its own data7 .

The intrinsic functions num_images() and this_image() provide the number of images and the number of the current image (named co-index). The syntax is simple and inspired by tensorial notations [START_REF] Numrich | Parallel numerical algorithms based on tensor notation and Co-Array Fortran syntax[END_REF]. While Fortran array indexes are within parentheses, the co-index is within brackets. Without explicit brackets, reference is made to the co-array of the current image. Using brackets, co-arrays of other images are accessed transparently. When needed, it is possible to synchronize images using, for example, the sync all instruction.

Here is a simple example to compute an approximation of π using a Monte Carlo method (an inefficient algorithm but suitable for this example!). We declare a co-array k[*] of 64-bit integers 8 which is zero initialized in each image and incremented when a random point drawn inside a square of side length 2 falls into the inscribed circle of unit radius. The star within the brackets means that the number of co-dimensions will not be known until execution. Once all the images reach the sync all instruction, image 1 is responsible for retrieving and adding the results of all images, and finally print the approximation of π. Fortran 2008 also introduces do concurrent loops which tell the compiler that the code inside the loop does not make use of data coming from previous iterations, and so it can be parallelized if the compiler considers it beneficial. For example the NVIDIA compiler nvfortran is capable of offloading execution of such a loop on their NVIDIA GPUs. These loops will eventually replace forall parallel loops that Fortran 95 standard tried to introduce.

Two new features allow for a better code structuring. Large modules can be split into submodules. Also, if originally all declarations had to come before the first executable statement, the block...end block construct allows for local declaration of variables (or module imports) at any point of the code. Hence, the code structure of a long procedure can be made more readable.

Among other additions in the Fortran 2008 standard, we find the intrin-sic module iso_fortran_env which provides standardized kind constants clearly identifying the types of data (for example real64 and int64), the maximum number of dimensions of an array (named rank) going from 7 to 15, the possibility of launching another program through the command line (execute_command_line), and the contiguous attribute which tells the compiler that an array received as a procedure argument will occupy a contiguous memory area 9 . Finally, many intrinsic functions are added, particularly for scientific computation: inverse trigonometric functions with complex arguments, inverse hyperbolic functions, Bessel functions, error and gamma functions, etc.

Fortran 2018

Fortran

Fortran and its communities 4.1 From the origins

Recent programming languages often have an organized community on the internet. But Fortran did not wait for computer networks to have its communities. In 1955, IBM created the SHARE user group for its IBM 704 machines. Backus and his team presented and discussed through this group their work on the language and its first compiler. The following paragraph describes the situation after its distribution [START_REF] Heising | The Emergence of FORTRAN IV from FORTRAN II[END_REF]:

Nonetheless, the technical basis of FORTRAN was sufficiently sound that usage was like a snowball going downhill. Soon there were hundreds of customers making hundreds of suggestions for improvements. They would find bugs and send them in -not only error reports, but in many cases the fixes would come in along with the reports. Many suggestions applied to such matters as improvement of diagnostics -little practical things -and it was as if there were hundreds of people working on improving FORTRAN. The suggestions just poured in, and we put them in as fast as we could.

In 1970 the Fortran Specialist Group of the British Computer Society10 was founded, which continues today its missions consisting in promoting the language, working to its evolutions and fostering exchanges and meetings between users.

Usenet

Following the creation of the Usenet network, a discussion group net.lang.f77 was created and later renamed comp.lang.fortran in 1986. It would remain for a long time the main place online where Fortran is discussed. It is still used, with typically ten new discussion topics per month. Nowadays, Usenet servers are scarce, including in universities, but one can also access these discussion groups via Google Groups.

Some reference websites

The Fortran Wiki 11 , created in 2008, has become an important source of information on the language, by allowing everyone to enrich it.

The Fortran French Wikipedia page is kept up to date and offers a lot of information and references on the language and its ecosystem.

A site 12 created in 2012 by Ondřej Čertík will long remain a reference in the Fortran world. Its content began to be transferred to the Fortran-lang community site.

The Fortran-lang community

Despite all these tools, it must be recognized that the galaxy of Fortran users remained rather scattered and poorly organized (except in standardization committees), compared to more recent languages. For a long time, there were many researchers or engineers publishing their libraries and programs in isolation on their websites.

At the end of 2019, a handful of developers decided to remedy this situation. They came together and created the Fortran-lang community using the GitHub platform to centralize developments [START_REF] Kedward | John Urban, and Jeremie Vandenplas[END_REF]. They thus created a central site 13 to provide all the information and resources needed by both the beginner and the expert programmer alike. To federate the community, they also set up a modern forum, the Fortran Discourse 14 , which now has over 1,100 registered users (from students to Fortran Standards Committee members). The most involved in the organization meet to discuss at monthly videoconferences 15

The stdlib standard library

Having made a diagnosis of the weaknesses of the language ecosystem, the founders of the community quickly launched two flagship projects. Unlike many languages (C, C++ , Python. . . ), Fortran did not have a standard library. The development of a standard (de facto) library named stdlib was therefore launched. One goal is to prevent language users from reinventing the wheel each of them on their own, and on the other hand to serve as a laboratory to propose new functionalities to the standardization committee. Its version 0.2.1 already contains hundreds of utility functions (strings, files, operating system integration, unit tests, logging. . . ), various algorithms (search, sort, fusion. . . ) and mathematical functions (linear algebra, special functions, 11 http://fortranwiki.org/ 12 https://www.fortran90.org/ 13 https://fortran-lang.org/ 14 https://fortran-lang.discourse.group/ 15 The community began to grow at the time of the first COVID lockdowns.

Fast Fourier Transform, random numbers, statistics, numerical integration, optimization. . . ).

The fpm package manager

Another problem in the Fortran ecosystem was the dispersion of libraries, developed independently and using different building tools. The Fortran Package Manager fpm solves it [START_REF]Fortran Package Manager fpm[END_REF]. It is largely inspired by Cargo, the utility of the Rust language serving both as package and build system manager. Creating a Hello World project, compiling it and launching it becomes as simple as typing in a terminal:

$ fpm new myproject $ cd myproject $ fpm run
The project options are defined in its manifest, a file in TOML format present at its root. The fpm package manager manages dependencies, which it downloads from GitHub. Associated with the git clone command, testing a Fortran project available on GitHub can be done in thirty seconds. Project tests can be started with the fpm test command. The community indeed promotes current good practices in programming: automatic testing, usage of a version manager, etc.

Fpm, whose version 0.9 was released in June 2023, is now a popular tool in the community and gradually legacy libraries are modernized using the latest language features and transformed into fpm packages. As a cherry on top of the cake, fpm is essentially written in Fortran, showing it is also a general purpose language. This bold choice allows in particular to attract more contributors from the community and promotes the sustainability of the project.

A new flagship project, the fpm registry will offer an official repository for fpm packages. The user will be able to easily discover, install or publish Fortran packages, as he can do in Python with PyPI.

The interactive LFortran compiler

One of the community founders, Ondřej Čertík16 , has been developing since 2019 a new open source compiler LFortran [START_REF]LFortran compiler[END_REF], one of whose key features is that it can be used interactively, for example with Jupyter. It also has several backends: LLVM, C, C++, Julia, WASM and x86-64. It is not yet in beta version but its development is advancing rapidly.

Financial support

The effort to develop all these tools is carried out partly within the professional framework of some members, as part of student members' studies, or as a hobby for others. But it is also possible to fund additional efforts. Thus, since 2021, the Fortran-lang organization participates every year in the Google Summer of Code (GSoC) where several students paid by Google were working on its projects [START_REF]Fortran-lang at the Google Summer of Code[END_REF]. At the end of 2022, the German organization Sovereign Tech Fund, under Federal Ministry for Economic Affairs and Climate Action, gave the organization the equivalent of three full-time jobs to work six months on the fpm package manager and the LFortran compiler [4]. It thus recognizes the importance of the language in climate modeling.

The FortranCon international conference

There have been conferences on High-Performance Computing (HPC) but the community lacked a conference dedicated solely to the Fortran language. A first International Fortran Conference (FortranCon) took place at the University of Zurich from 2 to 4 July 2020, but virtually because of the COVID pandemic. It allowed actors and language users to meet and discuss their work and projects. The second edition, FortranCon 2021, was held again virtually in Zurich on 23 and 24 September 2021, with typically 70 to 80 participants present simultaneously on the Zoom video conferencing platform. The videos of these conferences are freely accessible online [7].

5 And what's next?

Fortran 2023

The Fortran 2023 standard is expected to be released in fall 2023, almost 70 years after John Backus' letter to his superior. With many compilers not yet fully implementing Fortran 2018, the new standard does not intentionally provide major features but simply many improvements in different parts of the language: new functions for string handling, in particular to facilitate C to Fortran string interoperability, trigonometric functions in degrees, longer source lines, new format descriptors, some improvements for parallel computing, conditional expressions (same syntax as in C), etc. The simple attribute allows to define pure functions that do not access any external data except through its arguments. do concurrent loops are now able to use reduction variables. All the new features are summarized in the The New Features of Fortran 202x document [START_REF] Reid | The New Features of Fortran 202[END_REF].

We could regret that the language does not evolve faster, and that it is necessary to wait a long time for certain improvements to come, while newer languages have generally a more rapid development. However being a standardized language has its pros and cons, and the Fortran Standards Committee pays particular attention to the backward compatibility when new features are added. Thus, compilers incorporating the latest developments are generally still capable of compiling the so-called legacy codes, that are sometimes 40 or more years old. These legacy codes are still actively used in large organizations or companies.

As a side note, ISO standards are paid documents. But the working document Fortran 2023 Working Draft is still available on the J3 committee website [3]. All committee's working drafts are indeed in open access.

Fortran 202Y

The development of the next standard, voluntarily loosely named Fortran 202Y, is underway. It should notably develop the concept of generic programming, in particular with templates as in C++. This is certainly the most awaited novelty by Fortran developers, as evidenced by the dedicated directory on the GitHub repository [START_REF]J3 committee[END_REF] of the J3 standards committee, where since the end of 2019 anyone can propose and discuss new features for the language. The LFortran compiler also serves as an experimental platform for the implementation of this major future evolution.

As an important change at the symbolic level, we should finally see declared obsolescent the historic default implicit typing! Among the other innovations whose study is recommended by the J3, we can note the possibility of defining within the code itself the types used by default for each type of data, a Fortran preprocessor, and asynchronous task management.

Conclusion

As languages have been proliferating, Fortran has become a niche language. To caricature (because it is also a general language), one could say that it only does one thing, but it does it well: numerical computation 17 ! That is why it is still widely used in meteorological computations, climate modeling, fluid dynamics, computational chemistry, materials modeling [START_REF]Software FORGE® for simulation of hot and cold forming processes[END_REF], nuclear energy, aerospace, and many other areas. It is even used in economics and finance [START_REF] Fehr | Introduction to Computational Economics Using Fortran[END_REF][START_REF] Arnoud | Benchmarking Global Optimizers[END_REF]. It has adapted to all generations and architectures of computer hardware. The 2021 Turing Award was moreover awarded to the American Jack Dongarra 1: Some online Fortran compilers libraries that enabled high performance computational software to keep pace with exponential hardware improvements for over four decades." [START_REF] Dongarra | [END_REF] In the scientific computing domain, Fortran is now competing 19 with numerous languages and softwares: C, C++, Python, Julia, MATLAB, R, etc. Does labeling it as an old language really make sense? The 1956 textbook was 54 pages long, the Fortran 2023 standard is 681 pages long. The language has continuously incorporated new programming paradigms. It is thus one of the rare standardized languages to integrate parallel computing paradigms 20 . Standardized for nearly six decades, its foundations are stable while allowing it to evolve, which is a guarantee of durability for the engineer and the researcher [START_REF] Hinsen | Dealing With Software Collapse[END_REF]. On the compiler side, not all include the latest standards, and some have recently disappeared as Lahey and Absoft, but others appear. Intel's engineers worked five years to completely overhaul their compiler for LLVM. The open source Flang compiler is also being redesigned to integrate LLVM, driven in particular by NVIDIA. And another new open source compiler already mentioned, LFortran, is in development.

Finally, Fortran now has a dynamic and organized community, full of projects to improve its ecosystem and seasoned with current good practices of software development. Ten years after coming out of the top 20 on the TIOBE index [14] of most "popular" programming languages, Fortran has been returning periodically since April 2021, even reaching 11th place in July 2023. Interested readers will find online some good French courses [START_REF]in Intensive Scientific Computing) Fortran course in French[END_REF][START_REF]polycopié de Master de Jacques Lefrère[END_REF] to approach learning the language or learn its latest features, at least up to Fortran 2008. For Fortran 2018, it will be necessary for the moment to refer to the English books quoted previously [START_REF] Curcic | Modern Fortran: Building efficient parallel applications[END_REF][START_REF] Metcalf | Modern Fortran explained: incorporating Fortran[END_REF]. It is also possible to learn codes with the greatest impact on science [START_REF] Perkel | Ten computer codes that transformed science[END_REF]. 19 While hiding in the computing libraries of some of them, for example NumPy or SciPy! 20 Ada 83 was a forerunner in this regard, but Ada's reliability and safety goals take precedence over performance. True to its original impetus, Fortran's approach to parallelism focuses on numerical performance.

modern Fortran using one of the online compilers listed in Table 1.

  print * , " Sum of vectors u and v : " , w print * , " Square roots vector of u ( i ): " , sqrt ( u ) end program arrays

  Intel compilers were the first to fully implement Fortran 2018 and since 2020 they are freely available, as all the other Intel oneAPI Toolkits. With the 2023 version, the classic ifort compiler is giving way to the new ifx compiler, based on the LLVM compiler infrastructure. The Cray compiler also supports Fortran 2018.On the side of open source compilers, GFortran (GCC) is the most used. It still does not fully implement Fortran 2018 and relies on the OpenCoarrays library for parallel computing, yet it has the essentials and its development progresses.

  2018 brings numerous improvements, for example concerning C interoperability, but more importantly new concepts for parallel computing. Images can be grouped into teams working in parallel on different tasks. The concept of events allows images to communicate easily. And collective subroutines allow performing, in a simple way, reduction operations such as computing the sum of the values of a variable in each image. The previous example on the Monte Carlo computation of π can thus be rewritten more concisely:

	program p i _ m o n t e_c arlo _co_s um
	use , intrinsic :: iso_fortran_env , only : wp = > real64 , int64
	implicit none
	real ( wp )	:: xy (2)
	integer ( int64 ) :: i , k =0
	integer ( int64 ) , parameter :: n =1000000000
	do i = 1 , n / num_images ()
	call random_number ( xy )
	if ( sum ( xy **2) < 1) k = k + 1
	end do
	call co_sum (k , result_image = 1)
	if ( this_image () == 1) print * , (4.0 _wp * k ) / n
	end program p i _mo nte_ carl o_co_ sum

  18 "for his pioneering contributions to numerical algorithms and

	Name	URL	Characteristics
	Fortran Play-	https://play.fortran-lang.org/	From Fortran-lang community; GFor-
	Ground		tran compiler; stdlib standard library
			directly accessible
	Compiler Ex-	https://godbolt.org/	Multi-language; possibility to compare
	plorer		execution results and generated assem-
			bly code generated by different compil-
			ers; sharing option. . .
	tutorialspoint	https://www.tutorialspoint.com/	Multi-language with didactic material;
			GNU compiler; possibility to publicly
			share the code
	LFortran	https://dev.lfortran.org/	Compiler in alpha version; graphical dis-
			play; internal compiler representations
			and C++ generated code
		Table

The name was chosen at the end of 1954, the initial proposal being for an "automatic coding system". Note that FORTRAN is written for the period prior to Fortran 90.

In fact, the articles of the time use the word translator, rather than compiler.

In PCs, it wasn't until 1989 with the Intel i486 32-bit microprocessor that the floatingpoint arithmetic coprocessor (FPU) was no longer optional.

The strict syntax for initializing an array in Fortran 90 is (/ /), but Fortran 2003 introduced the more readable and intuitive syntax of square brackets.

SIMD instructions (single instruction, multiple data) such as FMA, SSE, AVX, etc. Modern compilers are able to vectorize certain loops automatically, and standards such as OpenMP include SIMD directives enabling the developer to guide the compiler in complex cases.

Single program, multiple data (SPMD).

These are scalars to simplify the example, but a co-array can also be declared from a classic array.

Which could potentially improve the performances.

https://fortran.bcs.org/

Now engineer at GSI Technology, a manufacturer of SRAM.

In the 2000s, the slogan of the late g95 compiler was it's free crunch time and GFortran's one was free number crunching FORALL!.

He had worked in particular on Fortran libraries such as EISPACK (1974), LINPACK, BLAS, LAPACK (1992) and ScaLAPACK (1993), etc. BLAS is also among the ten computer

Acknowledgements

We thank Pierre Hugonnet and Jeremie Vandenplas for their manuscript review and their precious remarks, as well as all the members of the Fortran-lang community for the rich and high-quality discussions we have on the Fortran Discourse, for the vision of its founders and for the efforts made to improve the language ecosystem.

//j3-fortran.org/doc/year


M T Hartman

X Lin

B Pointard

R Le Targat

B Fang

Y Le Coq

P Goldner

S Seidelin

First Measurements of Spectral Hole Line Shifts at Dilution Temperatures for Laser Stabilization

Keywords: Spectral Hole Burning, Laser Frequency Stabilization, Metrology, Spectroscopy

Here we report on the status of the Spectral-Hole Burning (SHB) laser-stabilization experiment at LNE-SYRTE, focusing on our first measurements of thermally induced frequency shifts of spectral holes at dilution temperatures (T0 < 1 K). The effect, which is predicated to scale as T 4 , produces shifts of order 1 -10 Hz over its ≈ 517 THz center at these temperatures. To meet this challenge, we introduced a novel temperaturemodulation based approach to spectral-hole line shift measurements, allowing integration time of the small signals. We find a preliminary value for the line-shift constant of Eu 3+ :Y2SiO5, α = 107 Hz K -4 , a first at dilution temperatures.

I. INTRODUCTION

The spectral-hole burning (SHB) experiment at LNE-SYRTE aims to produce an ultra frequency-stable laser by spectroscopic methods. The current state of the art ultrastable lasers involve locking to a length-stable optical cavity as a frequency reference [START_REF] Häfner | 8 × 10 -17 fractional laser frequency instability with a long room-temperature cavity[END_REF] [START_REF] Matei | 1.5 µm lasers with sub-10 mhz linewidth[END_REF]; however, this approach is reaching a fundamental materials limit, Brownian noise in the cavity mirrors. The SHB experiment explores a different approach to laser stabilization by utilizing, as its frequency reference, a transmissive spectral line (spectral hole) which we imprint (burn) at one of two absorption sites (homogeneously broadened about 580.039 nm and 580.211 nm) in a rare-earthion doped crystal, Eu 3+ :Y 2 SiO 5 [START_REF] Oswald | Characteristics of long-lived persistent spectral holes in Eu 3+ :Y 2 SiO 5 at 1.2 K[END_REF].

The SHB group has previously demonstrated the technique, stabilizing a laser to a pulse tube cooled crystal (T 0 = 3.7 K) achieving a fractional frequency stability of 1.7 × 10 -15 over 1 s [START_REF] Galland | Doubleheterodyne probing for an ultra-stable laser based on spectral hole burning in a rare-earth-doped crystal[END_REF], as well as studying the effects of mechanical stress [START_REF] Galland | Mechanical tunability of an ultranarrow spectral feature of a rare-earth-doped crystal via uniaxial stress[END_REF] [6] and external electric fields [START_REF] Zhang | Precision measurements of electric-fieldinduced frequency displacements of an ultranarrow optical transition in ions in a solid[END_REF]. Further characterizations of our experimental detection noise floor [START_REF] Galland | Doubleheterodyne probing for an ultra-stable laser based on spectral hole burning in a rare-earth-doped crystal[END_REF] and of the spectral hole thermal line shifts in the 3 -6 K range [Manuscript in Press, Phys Rev A] suggest that these are performance limiting effects. The T 4 scaling of the thermal shifts motivates our move to a dilution refrigerator to cool our sample below 1 K.

Here we present our initial measurements of spectral-hole line shifts at dilution temperatures.

II. EXPERIMENTAL SETUP

The setup, illustrated in Fig. 1, uses two tunable 1160 nm diode lasers. An infrared pre-stabilized laser (PSL) is locked to an optical cavity. The infrared probe laser (PRB) is locked to the PSL transferring its initial stability through an offset phaselock-loop (PLL). The PLL offset is sourced by an FPGA based software defined radio (SDR) system (Ettus USRP X310) upmixed by a function generator. A portion of the infrared light is sent to the frequency comb at LNE-SYRTE, providing a stable and robust frequency count of the PRB.

The PRB is frequency doubled to interrogate the spectroscopic sites near 580 nm. The yellow 580 nm beam completes a double-pass through a high-speed AOM where the light is frequency shifted by a custom spectrum, also generated by the SDR at a second output. As we implement a multispectral-hole interrogation scheme, several probe modes are imprinted at this point. The resulting spectrum of beat signals is split: a reference beam is measured by photodetector PD1, and the other beam probes the crystal where each probe mode experiences a phase delay proportional to the difference frequency between the laser and the spectral hole. PD2 measures the dephased beat notes. The signals from PD1 and PD2 are digitized by the SDR which produces the error signal. The PRB is actuated toward the center of the spectral hole by controlling the PLL offset.

III. METHODS

Similar to our own previous thermal line shift measurements [Manuscript in Press, Phys

Rev A], two groups have made earlier measurements of thermal line shifts in Eu 3+ :Y 2 SiO 5 by measuring the change in the absorption profile for increasing crystal temperatures from 2.5 K and above [START_REF] Könz | Temperature and concentration dependence of optical dephasing, spectral-hole lifetime, and anisotropic absorption in Eu 3+ :Y 2 SiO 5[END_REF] [START_REF] Thorpe | Frequency stabilization to 6 × 10 -16 via spectral-hole burning[END_REF] where temperature sensitives at spectroscopic site 1 are on the order of 10 000 Hz K -1 and higher. For dilution temperatures, where the sensitivities are on order 10 -100 Hz K -1 , we implement a different approach.

We lock the PRB laser to a spectral hole burned in the crystal held at 700 mK. The crystal temperature is controlled by a resistive heater in an active loop driven by a commercial cryogenic temperature controller (Lakeshore 350). A custom control program modulates the temperature set-point, simultaneously recording 0) the registered set-point (the system's driving signal), 1) the measured actual temperature (the system's input signal) and 2) the PRB-frequency comb beat (the system's output signal). Care is taken in optimizing the feedback PID gain, selecting appropriate modulation depths (m = 0.01, 0.02) and frequency (f mod = 31.6 mHz) to ensure that the temperature tracks the set-point. An example data point is shown in Fig. 2. A fit to the system driving signal provides the reference sinusoid. The amplitude and phase of the temperature (A 1 , ϕ 1 ) and beat note signal (A 2 , ϕ 2 ) modulation are determined through I-Q demodulation with the fitted reference sinusoid. The temperature sensitivity of the frequency is then calculated directly, df dT = A2 A1 .

- Staying locked to the spectral hole over a period of several hours, we actuate the mean crystal temperature to each measurement point, stopping to modulate for 24 periods. The resulting plot of temperature dependent temperature sensitivities is shown in Fig. 3. At temperatures below the Debye Temperature, the absolute shift in the spectral line center frequency is given in terms of the line shift constant, α: ∆f = αT 4 . Over the temperature range 0.5-0.9 K, we fit this constant to be α = 107 Hz K -4 at site 1 from our preliminary data. By comparison, at site 1 others have measured this constant to be α 1 = 168 ± 25 Hz K -4 fitting over 70 -100 K [START_REF] Könz | Temperature and concentration dependence of optical dephasing, spectral-hole lifetime, and anisotropic absorption in Eu 3+ :Y 2 SiO 5[END_REF] and α 1 = 76 ± 15 Hz K -4 measuring over the range 2.5 -5.5 K [START_REF] Thorpe | Frequency stabilization to 6 × 10 -16 via spectral-hole burning[END_REF].

V. DISCUSSION

These early results support our expected 3 order of magnitude reduction in temperature sensitivity by moving from pulse-tube to dilution temperatures. Considering measured cryostat temperature fluctuations of order 100 µK over 1 s, this reduces the temperature-induced limit to fractional laser frequency stability from order 10 -15 down to 10 -18 . This measurement, a first in spectral-hole spectroscopy, marks a major step towards achieving our goal realizing an ultra-stable laser with a fractional frequency stability of 10 -18 at 1 s.

  This project is funded by Ville de Paris Emergence Programme, Agence Nationale de la Recherche, LABEX FIRST-TF (ANR-10-LABX-48-01); H2020 Excellent Science (EMPIR 20FUN08 NEXTLASERS -EMPIR programme cofinanced by the Participating States and from the EU Horizon 2020 Research and Innovation Programme).

Fig. 1 .

 1 Fig. 1. Illustration of the SHB setup at LNE-SYRTE.

Fig. 2 .

 2 Fig. 2. An example data point of recorded temperature set-point, measured temperature, and frequency data. Left: Raw time series segment covering 1 modulation period. Right: Signals after averaging and removing offset

Fit ( alpha= 107. 2 )Fig. 3 .

 23 Fig.3. Preliminary measurements of temperature spectral line sensitivity of spectral holes in Eu 3+ :Y 2 SiO 5 for temperatures from 0.5 -0.9 K, and a fit of the spectroscopic site 1 line shift constant α.


Moustafa Eid

Pierre Maréchal

Ahmed Benamar

Ultrasonic characterization of solid suspensions in a viscous fluid

Ultrasonic Characterization of Solid Suspensions in a Viscous Fluid

Moustafa Eid 1 , Pierre Maréchal 1 , Ahmed Benamar 1 1 LOMC, UMR 6294 CNRS, University Le Havre Normandy, France Morning Session II, January 18, 2024, 11:20 -13:00 This research focuses on the characterization of a random distribution of solid particles suspended in a viscous fluid. As an investigation tool, the ultrasonic waves in the MHz frequency range and their propagation through such suspensions and bringing some information on the effective properties of the suspensions. In this context, the objective of this work is to establish the relationship between ultrasonic signals and suspended particles properties, considering their geometry, dimensions, concentration and distribution.

Currently, ultrasonic methods are yet omnipresent in several fields of applications:

• Sedimentation: Evaluation of characteristics such as concentration, average particle size, particle size distribution (PSD)… •

Polluted fluids: Treatment of wastewater and regulation.

•

Food products: Characterization of lipids, proteins, and other components… Within this framework, in order to achieve those objectives, the objectives are divided in two parts: Numerical and experimental. The objective of the numerical study is to consolidate previous numerical results with new configurations and develop a numerical model dedicated to our case of study involving ultrasonic, suspended microparticles, and viscous fluid. The usually considered models are involving strong assumptions such as spherical particles, low concentrations, small average wavenumber-radius product ka, constant temperature, suspensions without fluid flow. In the developed approach, such models are implemented, involving known spherical particles with a very narrow distribution density, low concentration c, viscosity , and regulated temperature T. Using Matlab, the numerical implementation of those models and their limits are compared and discussed: ECAH, Waterman and Truell, Forester and Pinfield. In a complementary approach, the experimental work consists in designing and constructing a practical experimental setup for ultrasonic measurements for the characterization of suspensions in a dynamic flow. In this aim, a specific instrumentation was developed to measure the effective ultrasonic properties (attenuation and velocity). The emission and reception of ultrasonic waves in the MHz frequency range was investigated for the characterization of suspended particles using a circulating pump in a temperature-regulated aquarium. Using Python, the acquisition of temporal signals was realized. A postprocessing of the acquired signals was carried out using FFT, in order to determine attenuation and phase velocity as well as their frequency dependence. As a summarize, the obtained results include: • Numerical validation (Matlab) of a model adapted for the studied solid suspensions in a given viscous fluid.

•

Development of an experimental setup and measurement protocol, outlining signal acquisition procedures (Python), FFT processing, and determination of attenuation and velocity curves as a function of frequency.

•

Quantification of the influence of the flow rate, temperature, concentration and frequency.