Gilles Dowek
email: gilles.dowek@inria.fr

The Stratified Foundations as a theory modulo

The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory. Deduction modulo is a formulation of first-order logic with a general notion of cut. It is known that proofs normalize in a theory modulo if it has some kind of many-valued model called a pre-model. We show in this paper that the Stratified Foundations can be presented in deduction modulo and that the method used in the original normalization proof can be adapted to construct a pre-model for this theory.

The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. This theory is consistent [START_REF] Jensen | On the consistency of a slight (?) modification of Quine's new foundations[END_REF] while naive set theory is not and the consistency of the Stratified Foundations together with the extensionality axiom -the so-called New Foundations -is open.

The Stratified Foundations extend simple type theory and, like in simple type theory, proofs strongly normalize in The Stratified Foundations [START_REF] Crabbé | Stratification and cut-elimination[END_REF]. These two normalization proofs, like many, have some parts in common, for instance they both use Girard's reducibility candidates. This motivates the investigation of general normalization theorems that have normalization theorems for specific theories as consequences. The normalization theorem for deduction modulo [START_REF] Dowek | Proof normalization modulo[END_REF] is an example of such a general theorem. It concerns theories expressed in deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF] that are first-order theories with a general notion of cut. According to this theorem, proofs normalize in a theory in deduction modulo if this theory has some kind of many-valued model called a pre-model. For instance, simple type theory can be expressed in deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | HOL-λσ an intentional first-order expression of higher-order logic[END_REF] and it has a pre-model [START_REF] Dowek | Proof normalization modulo[END_REF][START_REF] Dowek | HOL-λσ an intentional first-order expression of higher-order logic[END_REF] and hence it has the normalization property. The normalization proof obtained this way is modular: all the lemmas specific to type theory are concentrated in the pre-model construction while the theorem that the existence of a premodel implies normalization is generic and can be used for any other theory in deduction modulo.

The goal of this paper is to show that the Stratified Foundations also can be presented in deduction modulo and that the method used in the original normalization proof can be adapted to construct a pre-model for this theory. The normalization proof obtained this way is simpler than the original one because it simply uses the fact that proofs normalize in the Stratified Foundations if this theory has a pre-model, while a variant of this proposition needs to be proved in the original proof.

It is worth noticing that the original normalization proof for the Stratified Foundations is already in two steps, where the first is the construction of a socalled normalization model and the second is a proof that proofs normalize in the Stratified Foundations if there is such a normalization model. Normalization models are, more or less, pre-models of the Stratified Foundations. So, we show that the notion of normalization model, that is specific to the Stratified Foundations, is an instance of a more general notion that can be defined for all theories modulo, and that the lemma that the existence of a normalization model implies normalization for the Stratified Foundations is an instance of a more general theorem that holds for all theories modulo.

The normalization proof obtained this way differs also from the original one in other respects. First, to remain in first-order logic, we do not use a presentation of the Stratified Foundations with a binder, but one with combinators. To express the Stratified Foundations with a binder in first-order logic, we could use de Bruijn indices and explicit substitutions along the lines of [START_REF] Dowek | HOL-λσ an intentional first-order expression of higher-order logic[END_REF]. The pre-model construction below should generalize easily to such a presentation. Second, our cuts are cuts modulo, while the original proof uses Prawitz' folding-unfolding cuts. It is shown in [START_REF] Dowek | About folding-unfolding cuts and cuts modulo[END_REF] that the normalization theorems are equivalent for the two notions of cuts, but that the notion of cut modulo is more general that the notion of folding-unfolding cut. Third, we use untyped reducibility candidates and not typed ones as in the original proof. This quite simplifies the technical details.

A last benefit of expressing the Stratified Foundations in deduction modulo is that we can use the method developed in [START_REF] Dowek | Theorem proving modulo[END_REF] to organize proof search. The method obtained this way, that is an analog of higher-order resolution for the Stratified Foundations, is much more efficient than usual first-order proof search methods with the comprehension axioms, although it remains complete as the Stratified Foundations have the normalization property.

1 Deduction modulo

Identifying propositions

In deduction modulo, the notions of language, term and proposition are that of first-order logic. But, a theory is formed with a set of axioms Γ and a congruence ≡ defined on propositions. Such a congruence may be defined by a rewrite systems on terms and on propositions (as propositions contain binders -quantifiers -, these rewrite systems are in fact combinatory reduction systems [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]). Then, the deduction rules take this congruence into account. For instance, the modus ponens is not stated as usual

A ⇒ B A B B Excluded middle if A ≡ B ∨ (B ⇒ ⊥) Γ ⊢≡ A Fig. 1. Natural deduction modulo
All the rules of intuitionistic natural deduction may be stated in a similar way. Classical deduction modulo is obtained by adding the excluded middle rule (see figure 1).

For example, in arithmetic, we can define a congruence with the following rewrite system 0 + y → y S(x) + y → S(x + y)

0 × y → 0 S(x) × y → x × y + y
In the theory formed with a set of axioms Γ containing the axiom ∀x x = x and this congruence, we can prove, in natural deduction modulo, that the number 4 is even

axiom Γ ⊢ ≡ ∀x x = x (x, x = x, 4) ∀-elim Γ ⊢ ≡ 2 × 2 = 4 (x, 2 × x = 4, 2) ∃-intro Γ ⊢ ≡ ∃x 2 × x = 4
Substituting the variable x by the term 2 in the proposition 2 × x = 4 yields the proposition 2 × 2 = 4, that is congruent to 4 = 4. The transformation of one proposition into the other, that requires several proof steps in usual natural deduction, is dropped from the proof in deduction modulo.

In this example, all the rewrite rules apply to terms. Deduction modulo permits also to consider rules rewriting atomic propositions to arbitrary ones. For instance, in the theory of integral domains, we have the rule

x × y = 0 → x = 0 ∨ y = 0
that rewrites an atomic proposition to a disjunction.

Notice that, in the proof above, we do not need the axioms of addition and multiplication. Indeed, these axioms are now redundant: since the terms 0 + y and y are congruent, the axiom ∀y 0+y = y is congruent to the axiom of equality ∀y y = y. Hence, it can be dropped. Thus, rewrite rules replace axioms.

This equivalence between rewrite rules and axioms is expressed by the the equivalence lemma that for every congruence ≡, we can find a theory T such that Γ ⊢ ≡ A is provable in deduction modulo if and only if T Γ ⊢ A is provable in ordinary first-order logic [START_REF] Dowek | Theorem proving modulo[END_REF]. Hence, deduction modulo is not a true extension of first-order logic, but rather an alternative formulation of first-order logic. Of course, the provable propositions are the same in both cases, but the proofs are very different.

Model of a theory modulo

A model of a congruence ≡ is a model such that if A ≡ B then for all assignments, A and B have the same denotation. A model of a theory modulo Γ, ≡ is a model of the theory Γ and of the congruence ≡. Unsurprisingly, the completeness theorem extends to classical deduction modulo [START_REF] Dowek | La part du calcul[END_REF] and a proposition is provable in the theory Γ, ≡ if and only if it is valid in all the models of Γ, ≡.

Normalization in deduction modulo

Replacing axioms by rewrite rules in a theory changes the structure of proofs and in particular some theories may have the normalization property when expressed with axioms and not when expressed with rewrite rules. For instance, from the normalization theorem for first-order logic, we get that any proposition that is provable with the axiom A ⇔ (B ∧ (A ⇒ ⊥)) has a normal proof. But if we transform this axiom into the rule A → B ∧ (A ⇒ ⊥) (Crabbé's rule [START_REF] Crabbé | Non-normalisation de ZF[END_REF]) the proposition B ⇒ ⊥ has a proof, but no normal proof.

We have proved a normalization theorem: proofs normalize in a theory modulo if this theory has a pre-model [START_REF] Dowek | Proof normalization modulo[END_REF]. A pre-model is a many-valued model whose truth values are reducibility candidates, i.e. sets of proof-terms. Hence we first define proof-terms, then reducibility candidates and at last pre-models.

Definition 1 (Proof-term).

Proof-terms are inductively defined as follows.

π ::= α | λα π | (π π ′ ) | ⟨π, π ′ ⟩ | f st(π) | snd(π) | i(π) | j(π) | (δ π 1 απ 2 βπ 3 ) | (botelim π) | λx π | (π t) | ⟨t, π⟩ | (exelim π xαπ ′ )
Each proof-term construction corresponds to an intuitionistic natural deduction rule: terms of the form α express proofs built with the axiom rule, terms of the form λα π and (π π ′ ) express proofs built with the introduction and elimination rules of the implication, terms of the form ⟨π, π ′ ⟩ and f st(π), snd(π) express proofs built with the introduction and elimination rules of the conjunction, terms of the form i(π), j(π) and (δ π 1 απ 2 βπ 3 ) express proofs built with the introduction and elimination rules of the disjunction, terms of the form (botelim π) express proofs built with the elimination rule of the contradiction, terms of the form λx π and (π t) express proofs built with the introduction and elimination rules of the universal quantifier and terms of the form ⟨t, π⟩ and (exelim π xαπ ′ ) express proofs built with the introduction and elimination rules of the existential quantifier.

Definition 2 (Reduction). Reduction on proof-terms is defined by the following rules that eliminate cuts step by step.

(λα π 1 π 2 ) ▷ [π 2 /α]π 1 f st(⟨π 1 , π 2 ⟩) ▷ π 1 snd(⟨π 1 , π 2 ⟩) ▷ π 2 (δ i(π 1 ) απ 2 βπ 3 ) ▷ [π 1 /α]π 2 (δ j(π 1 ) απ 2 βπ 3 ) ▷ [π 1 /β]π 3 (λx π t) ▷ [t/x]π (exelim ⟨t, π 1 ⟩ αxπ 2 ) ▷ [t/x, π 1 /α]π 2
Definition 3 (Reducibility candidates). A proof-term is said to be neutral if it is a proof variable or an elimination (i.e. of the form (π π ′ ), f st(π), snd(π), (δ π 1 απ 2 βπ 3 ), (botelim π), (π t), (exelim π xαπ ′ )), but not an introduction. A set R of proof-terms is a reducibility candidate if

-if π ∈ R, then π is strongly normalizable, -if π ∈ R and π ▷ π ′ then π ′ ∈ R, -if π is neutral and if for every π ′ such that π ▷ 1 π ′ , π ′ ∈ R then π ∈ R.
We write C for the set of all reducibility candidates. Definition 4 (Pre-model). A pre-model N for a language L is given by: a set N , for each function symbol f of arity n a function f from N n to N , for each predicate symbol P a function P from N n to C. Definition 5 (Denotation in a pre-model). Let N be a pre-model, t be a term and φ an assignment mapping all the free variables of t to elements of N . We define the object t N φ by induction over the structure of t.

-

x N φ = φ(x), -f (t 1 , . . . , t n ) N φ = f ( t 1 N φ , . . . , t n N φ ).
Let A be a proposition and φ an assignment mapping all the free variables of A to elements of N . We define the reducibility candidate A N φ by induction over the structure of A.

-If A is an atomic proposition P (t 1 , . . . , t n ) then A N φ = P ( t 1 N φ , . . . , t n N φ ). -If A = B ⇒ C then A N
φ is the set of proofs π such that π is strongly normalizable and whenever it reduces to λα π 1 then for every

π ′ in B N φ , [π ′ /α]π 1 is in C N φ . -If A = B ∧ C then A N
φ is the set of proofs π such that π is strongly normalizable and whenever it reduces to

⟨π 1 , π 2 ⟩ then π 1 is in B N φ and π 2 is in C N φ . -If A = B ∨ C then A N
φ is the set of proofs π such that π is strongly normalizable and whenever it reduces to i(π 1 ) (resp. j(π 2 )) then π 1 (resp.

π 2 ) is in B N φ (resp. C N φ ). -If A = ⊥ then A N φ is the set of strongly normalizable proofs. -If A = ∀x B then A N
φ is the set of proofs π such that π is strongly normalizable and whenever it reduces to λx π 1 then for every term t and every element a of

N [t/x]π 1 is in B N φ+a/x . -If A = ∃x B then A N
φ is the set of proofs π such that π is strongly normalizable and whenever it reduces to ⟨t, π 1 ⟩ then there exists an element a in N such that π 1 is in B N φ+a/x . Definition 6. A pre-model is said to be a pre-model of a congruence ≡ if when A ≡ B then for every assignment φ, A N φ = B N φ .

Theorem 1 (Normalization). [START_REF] Dowek | Proof normalization modulo[END_REF] If a congruence ≡ has a pre-model all proofs modulo ≡ strongly normalize.

2 The Stratified Foundations

(Stratifiable proposition)

A proposition A in the language ∈ is said to be stratifiable if there exists a function S mapping every variable (bound or free) of A to a natural number in such a way that every atomic proposition of A, x ∈ y is such that S(y) = S(x)+1.

For instance, the proposition

∀v (v ∈ x ⇔ v ∈ y) ⇒ ∀w (x ∈ w ⇒ y ∈ w) is stratifiable (take, for instance, S(v) = 4, S(x) = S(y) = 5, S(w) = 6) but not the proposition ∀v (v ∈ x ⇔ v ∈ y) ⇒ x ∈ y
Definition 8. (The stratified comprehension scheme) For every stratifiable proposition A whose free variables are among x 1 , . . . , x n , x n+1 we take the axiom ∀x 1 . . . ∀x n ∃z ∀x n+1 (x n+1 ∈ z ⇔ A) Definition 9. (The skolemized stratified comprehension scheme) When we skolemize this scheme, we introduce for each stratifiable proposition A in the language ∈ and sequence of variables x 1 , . . . , x n , x n+1 such that the free variables of A are among x 1 , . . . , x n , x n+1 , a function symbol f x1,...,xn,xn+1,A and the axiom

∀x 1 . . . ∀x n ∀x n+1 (x n+1 ∈ f x1,...,xn,xn+1,A (x 1 , . . . , x n ) ⇔ A)

The Stratified Foundations as a theory modulo

Now we want to replace the axiom scheme above by a rewrite rule, defining a congruence on propositions, so that the Stratified Foundations are defined as an axiom free theory modulo.

Definition 10. (The rewrite system R)

t n+1 ∈ f x1,...,xn,xn+1,A (t 1 , . . . , t n ) → [t 1 /x 1 , . . . , t n /x n , t n+1 /x n+1 ]A Proposition 1.
The rewrite system R is confluent and terminating. Proof. The system R is an orthogonal combinatory reduction system, hence it is confluent [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF].

For termination, if A is an atomic proposition we write ∥A∥ for the number of function symbols in A and if A is a proposition containing the atomic propositions A 1 , . . . , A p we write A • for the multiset {∥A 1 ∥, . . . , ∥A p ∥}. We show that if a proposition A reduces in one step to a proposition B then B • < A • for the multiset ordering.

If the proposition A reduces in one step to B, there is an atomic proposition of A, say A 1 , that has the form t n+1 ∈ f x1,...,xn,xn+1,C (t 1 , . . . , t n ) and reduces to

B 1 = [t 1 /x 1 , . . . , t n /x n , t n+1 /x n+1 ]C. Every atomic proposition b of B 1 has the form [t 1 /x 1 , . . . , t n /x n , t n+1 /x n+1 ]c
where c is an atomic proposition of C. The proposition c has the form x i ∈ x j for distinct i and j (since C is stratifiable) x i ∈ y, y ∈ x i or y ∈ z. Hence b has the form t i ∈ t j for distinct i and j, t i ∈ y, y ∈ t i or y ∈ z and ∥b∥ < ∥A 1 ∥. Therefore B • < A • . Proposition 2. A proposition A is provable from the skolemized comprehension scheme if and only if it is provable modulo the rewrite system R.

Consistency

We want now to construct a model for the Stratified Foundations.

If M is a model of set theory we write M for the set of elements of the model, ∈ M for the denotation of the symbol ∈ in this model, ℘ M for the powerset in this model, etc. We write also A M φ for the denotation of a proposition A for the assignment φ.

The proof of the consistency of the Stratified Foundations rests on the existence of a model of Zermelo's set theory, such that there is a bijection σ from M to M and a family v i of elements of M , i ∈ Z such that

a ∈ M b if and only if σa ∈ M σb σv i = v i+1 v i ⊆ M v i+1 ℘ M (v i ) ⊆ M v i+1
The existence of such a model is proved in [START_REF] Jensen | On the consistency of a slight (?) modification of Quine's new foundations[END_REF].

Using the fact that M is a model of the axiom of extensionality, we prove that a ⊆ M b if and only if σa ⊆ M σb, σ{a, b} M = {σa, σb} M , σ⟨a, b⟩ M = ⟨σa, σb⟩ M , σ℘(a) = ℘(σa), etc.

For the normalization proof, we will further need that M is an ω-model. We define 0 = ∅ M , n + 1 = n∪ M {n} M . An ω-model is a model such that a ∈ M N M if and only if there exists n in N such that a = n. The existence of such a model is proved in [START_REF] Jensen | On the consistency of a slight (?) modification of Quine's new foundations[END_REF] (see also [START_REF] Crabbé | Stratification and cut-elimination[END_REF]).

Using the fact that M is a model of the axiom of extensionality, we prove that σ∅ M = ∅ M and then, by induction on n that σn = n.

Notice that since ℘ M (v i ) ⊆ M v i+1 , ∅ M ∈ M v i and for all n, n ∈ M v i . Hence as the model is an ω-model N M ⊆ M v i .
In an ω-model, we can identify the set N of natural numbers with the set of objects a in M such that a ∈ M N M . To each proof-term we can associate a natural number n (its Gödel number) and then the element n of M. Proof-terms, their Gödel number and the encoding of this number in M will be identified in the following.

We are now ready to construct a model U for the Stratified Foundations. The base set is the set U of elements a of M such that a ∈ M v 0 . The relation ∈ U is defined by a ∈ U b if and only if a ∈ M σb. This permits to define the denotation of propositions built without Skolem symbols. To be able to define the denotation of Skolem symbols, we prove the following proposition. Proposition 3. For every stratifiable proposition A in the language ∈ whose free variables are among x 1 , . . . , x n , x n+1 and for all a 1 , . . . , a n in U , there exists an element b in U such that for every a n+1 in U , a n+1 ∈ M σb if and only if A U a1/x1,...,an/xn,an+1/xn+1 = 1

Proof. Let |A| be the proposition defined as follows.

-

|A| = A if A is atomic, -|A ⇒ B| = |A| ⇒ |B|, |A ∧ B| = |A| ∧ |B|, |A ∨ B| = |A| ∨ |B|, |⊥| = ⊥, -|∀x A| = ∀x ((x ∈ E S(x) ) ⇒ |A|), -|∃x A| = ∃x ((x ∈ E S(x) ) ∧ |A|).
Notice that the free variables of |A| are among E 0 , . . . , E m , x 1 , . . . , x n , x n+1 . Let φ = a 1 /x 1 , . . . , a n /x n , a n+1 /x n+1 ψ = v 0 /E 0 , . . . , v m /E m , σ k1 a 1 /x 1 , . . . , σ kn a n /x n , σ kn+1 a n+1 /x n+1

where k 1 = S(x 1 ), . . . , k n+1 = S(x n+1 ). We check, by induction over the structure of A, that if A is a stratifiable proposition in the language ∈, then

|A| M ψ = A U φ -If A is an atomic proposition x i ∈ x j , then k j = k i + 1, |A| M ψ = 1 if and only if σ ki a i ∈ M σ kj a j if and only if a i ∈ M σa j , if and only if A U φ = 1. -if A = B ⇒ C then |A| M ψ = 1 if and only if |B| M ψ = 0 or |C| M ψ = 1 if and only if B U φ = 0 or C U φ = 1 if and only if A U φ = 1. -if A = B ∧ C then |A| M ψ = 1 if and only if |B| M ψ = 1 and |C| M ψ = 1 if and only if B U φ = 1 and C U φ = 1 if and only if A U φ = 1. -if A = B ∨ C then |A| M ψ = 1 if and only if |B| M ψ = 1 or |C| M ψ = 1 if and only if B U φ = 1 and C U φ = 1 if and only if A U φ = 1. -|⊥| M ψ = 0 = ⊥ U φ . -if A = ∀x B then |A| M ψ = 1 if and only if for every c in M such that c ∈ M v k , |B| M ψ+c/x =
U φ = 1.
Then, the model M is a model of the comprehension scheme. Hence, it is a model of the proposition

∀E 0 . . . ∀E m ∀x 1 . . . ∀x n ∀y ∃z ∀x n+1 (x n+1 ∈ z ⇔ (x n+1 ∈ y ∧ |A|))
Thus, for all a 1 , ..., a n , there exists an object b 0 such that for all a n+1

(x n+1 ∈ z ⇔ (x n+1 ∈ y ∧ |A|)) M ψ+v k n+1 /y+b0/z = 1
We have

σ kn+1 a n+1 ∈ M b 0 if and only if σ kn+1 a n+1 ∈ M v kn+1 and |A| M ψ = 1 thus a n+1 ∈ M σ -kn+1 b 0 if and only if a n+1 is in U and A U φ = 1. We take b = σ -(kn+1+1) b 0 . For all a n+1 in U , we have a n+1 ∈ M σb if and only if A U φ = 1. Notice finally that b 0 ∈ M ℘ M (v kn+1 ), thus b 0 ∈ M v kn+1+1 , b ∈ M v

Normalization

We want now to construct a pre-model for the Stratified Foundations.

Let

u i = v 3i and τ = σ 3 . The function τ is an automorphism of M, τ u i = u i+1 , u i ⊆ M u i+1 and ℘ M (℘ M (℘ M (u i ))) ⊆ M u i+1 .
As M is an ω-model of set theory, for each recursively enumerable relation R on natural numbers, there is an object r in M such that R(a 1 , . . . , a n ) if and only if ⟨a 1 , . . . , a n ⟩ M ∈ M r. In particular there is an object P roof such that π ∈ M P roof if and only if π is (the encoding in M of the Gödel number of) a proof, an object T erm such that t ∈ M T erm if and only if t is (the encoding of the Gödel number of) a term, an object Subst such that ⟨π, π 1 , α, π 2 ⟩ M ∈ M Subst if and only if π, π 1 and π 2 are (encodings of Gödel numbers of) proofs, α is (the encoding of the Gödel number of) a proof variable and π = [π 1 /α]π 2 , an object Subst ′ such that ⟨π, t, x, π 1 ⟩ M ∈ M Subst ′ if and only if π and π 1 are (encodings of the Gödel numbers of) proofs, x is (the encoding of the Gödel number of) a term variable and t (the encoding of the Gödel number of) a term and π = [t/x]π 1 , an object Red such that ⟨π, π 1 ⟩ M ∈ M Red if and only if π and π 1 are (encodings of Gödel numbers of) proofs and π ▷ * π 1 , an object Sn such that π ∈ M Sn if and only if π is (the encoding of the Gödel number of) a strongly normalizable proof, an object ImpI such that ⟨π, α, π 1 ⟩ M ∈ M ImpI if and only if π and π 1 are (encodings of Gödel numbers of) proofs, α is (the encoding of the Gödel number of) a proof variable and π = λα π 1 , an object AndI such that ⟨π, π 1 , π 2 ⟩ M ∈ M AndI if and only if π, π 1 and π 2 are (encodings of Gödel numbers of) proofs and

π = ⟨π 1 , π 2 ⟩, -an object OrI1 (resp. OrI2) such that ⟨π, π 1 ⟩ M ∈ M OrI1 (resp. ⟨π, π 2 ⟩ M ∈ M
OrI2) if and only if π and π 1 (resp. π and π 2 ) are (encodings of Gödel numbers of) proofs and π = i(π 1 ) (resp. π = j(π 2 )), an object F orallI such that ⟨π, α, π 1 ⟩ M ∈ M F orallI if and only π and π 1 are (encodings of Gödel numbers of) proofs, α is (the encoding of the Gödel number of) a proof variable, and π = λαπ 1 , an object ExistsI such that ⟨π, t, π 1 ⟩ M ∈ M ExistsI if and only if π and π 1 are (encodings of Gödel numbers of) proofs, t is (the encoding of the Gödel number of) a term and π = ⟨t, π 1 ⟩.

Notice also that, since M is a model of the comprehension scheme, there is an object Cr such that α ∈ M Cr if and only if α is a reducibility candidate (i.e. the set of objects β such that β ∈ M α is a reducibility candidate).

Definition 12 (Admissible). An element α of M is said to admissible at level i if α is a set of pairs ⟨π, β⟩ M where π is a proof and β an element of u i and for each β in u i the set of π such that ⟨π, β⟩ M ∈ M α is a reducibility candidate.

Notice that if R is any reducibility candidate then the set R × M u i is admissible at level i. Hence there are admissible elements at all levels. Proposition 5. There is an element A i in M such that α ∈ M A i if and only if α is admissible at level i.

Proof. An element α of M admissible at level i if and only if

α ∈ M ℘ M (P roof × M u i ) ∧∀β (β ∈ M u i ⇒ ∃C (C ∈ M Cr ∧ (⟨π, β⟩ M ∈ M α ⇔ π ∈ M C)))
Hence, as M is a model of the comprehension scheme, there is an element A i in M such that α ∈ M A i if and only if α is admissible at level i.

Notice that α ∈ τ A i if and only if α ∈ A i+1 . Hence as M is a model of the extensionality axiom, τ A i = A i+1 .

Notice, at last, that

A i ⊆ M ℘ M (P roof × M u i ) ⊆ M ℘ M (u i × M u i ) ⊆ M ℘ M (℘ M (℘ M (u i ))) ⊆ M u i+1 . Proposition 6. If β ∈ M A i and α ∈ M A i+1 then the set of π such that ⟨π, β⟩ ∈ M α is a reducibility candidate. Proof. As α ∈ M A i+1 and β ∈ M A i ⊆ M u i+1 , the set of π such that ⟨π, β⟩ ∈ M α is a reducibility candidate.
We are now ready to construct a pre-model N of the Stratified Foundations. The base set of this pre-model is the set N of elements of M that are admissible at level 0. We take ∈ N (α, β) = {π | ⟨π, α⟩ M ∈ M τ β}. This permits to define the denotation of propositions built without Skolem symbols. To define the denotation of Skolem symbols, we prove the following proposition. Proposition 7. For every stratifiable proposition A in the language ∈ whose free variables are among x 1 , . . . , x n , x n+1 and for all a 1 , . . . , a n in N , there exists an element b in N such that for every a n+1 in N , ⟨π, a n+1 ⟩ M ∈ M τ b if and only if π is in A N a1/x1,...,an+1/xn+1 . Proof. Let |A| be the proposition (read p realizes A) defined as follows.

- Notice that the free variables of |A| are among term, subst, subst ′ , red, sn, impI, andI, orI1, orI2, f orallI, existsI, p, E 0 , . . . , E m , x 1 , . . . , x n , x n+1 . Let φ = a 1 /x 1 , . . . , a n /x n , a n+1 /x n+1 ψ = T erm/term, Subst/subst, Subst ′ /subst ′ , Red/red, Sn/sn, ImpI/impI, AndI/andI, OrI1/orI1, OrI2/orI2, F orallI/f orallI, ExistsI/existsI, A 0 /E 0 , . . . , A m /E m , τ k1 a 1 /x 1 , . . . , τ kn a n /x n , τ kn+1 a n+1 /x n+1

|x i ∈ x j | = ⟨p, x i ⟩ ∈ x j , -|A ⇒ B| = p ∈
We check, by induction over the structure of A, that if A is a stratifiable proposition in the language ∈, then the set of proofs π such that |A| M ψ+π/p = 1 is A N φ .

-If A is an atomic proposition x i ∈ x j , then k j = k i +1, we have |A| M ψ+π/p = 1 if and only if ⟨π, τ ki a i ⟩ M ∈ M τ kj a j if and only if ⟨τ ki π, τ ki a i ⟩ M ∈ M τ kj a j if and only if τ ki ⟨π, a i ⟩ M ∈ M τ kj a j if and only if ⟨π,

a i ⟩ M ∈ M τ a j if and only if π is in A N φ . -if A = B ⇒ C then we have |A| M
ψ+π/p = 1 if and only if π is strongly normalizable and whenever π reduces to λα π 1 then for all π ′ such that |B| M ψ+π ′ /p = 1 we have |C| M ψ+[π ′ /α]π1/p = 1 if and only if π is strongly normalizable and whenever π reduces to λx π 1 then for all

π ′ in B N φ , [π ′ /α]π 1 is in C N φ if and only if π is in A N φ . -If A = B ∧ C then we have A M ψ+π/p = 1 if
, π 2 ⟩ then π 1 is in B N φ and π 2 is in C N φ if and only if π is in A N φ . -If A = B ∨ C then we have A M
ψ+π/p = 1 if and only if π is strongly normalizable and whenever π reduces to i(π 1 ) (resp. j(π 2 )) then B M ψ+π1/p = 1 (resp. C M ψ+π2/p = 1) if and only if π is strongly normalizable and whenever π reduces to i(π 1 ) (resp. j(π

2 )) then π 1 is in B N φ (resp. C N φ ) if and only if π is in A N φ . -If A = ⊥ then A M ψ+π/p = 1 if and only if π is strongly normalizable if and only if π is in A N φ . -if A = ∀x B, then |A| M ψ+π/p = 1 if
0 . . . ∀E m ∀x 1 . . . ∀x n ∃z ∀p ∀x n+1 ⟨p, x n+1 ⟩ ∈ z ⇔ ⟨p, x n+1 ⟩ ∈ proof ×U ∧|A|
Thus, for all a 1 , ..., a n , there exists an object b 0 such that for all a n+1 ⟨p,

x n+1 ⟩ ∈ z ⇔ ⟨p, x n+1 ⟩ ∈ N M × U ∧ |A| M ψ+P roof /proof,b0/z,u k n+1 +1 /U,π/p = 1 We have ⟨π, τ kn+1 a n+1 ⟩ M ∈ M b 0 if and only if π is a proof, τ kn+1 a n+1 ∈ M u kn+1+1 and |A| M ψ+π/p = 1. Thus ⟨π, a n+1 ⟩ M ∈ M τ -kn+1 b 0 if and only if a n+1 ∈ M u 1 and π is in A N φ .
We take b = τ -(kn+1+1) b 0 and for all a n+1 in N we have ⟨π, a n+1 ⟩ M ∈ M τ b if and only if π is in A N φ . Finally, notice that b 0 is a set of pairs ⟨π, β⟩ M where π is a proof and β an element of u kn+1+1 and for each β in u kn+1+1 the set of π such that ⟨π, β⟩ Corollary 2. All proofs strongly normalize in the Stratified Foundations.

M ∈ M b 0 is |A| M ψ+β/x k n+1 ,π/p =
Remark 1. As already noticed in [START_REF] Crabbé | Stratification and cut-elimination[END_REF], instead of constructing the a pre-model of the Stratified Foundations within an automorphic ω-model of Zermelo's set theory, we could construct it within an ω-model of the Stratified Foundations.

In such a model U, we can define recursively enumerable relations, because the Stratified Foundations contains enough arithmetic and comprehension. Then we can take the sequence u i to be the constant sequence equal to w where w is a universal set, i.e. a set such that a ∈ U w for all element a of the model. Such an object obviously verifies ℘ U (℘ U (℘ U (w))) ⊆ U w. In other words, we say that an element of U is admissible if it is a set of pairs ⟨π, β⟩ U where π is a proof and for each β in U , the set of π such that ⟨π, β⟩ ∈ U α is a reducibility candidate. Proposition 6 becomes trivial, but we need to use the existence of a universal set to prove that there are admissible elements in the model and that there is a set A of admissible elements in the model. Hence, the difficult part in this pre-model construction (the part that would not go through for Zermelo's set theory for instance) is the construction of the base set.

Conclusion

In this paper, we have have shown that the Stratified Foundations can be expressed in deduction modulo and that the normalization proof for this theory be decomposed into two lemmas: one expressing that it has a pre-model and the other that proof normalize in this theory if it has a pre-model. This second lemma is not specific to the Stratified Foundations, but holds for all theories modulo. The idea of the first lemma is to construct a pre-model within an ω-model of the theory with the help of formal realizability. This idea does not seems to be specific to the Stratified Foundations either, but, its generality remains to be investigated. Thus, this example contributes to explore of the border between the theories modulo that have the normalization property and those that do not.

2. 1

 1 The Stratified Foundations as a first-order theory Definition 7.

  sn ∧ ∀q ∀w ∀r (⟨p, q⟩ ∈ red ∧ ⟨q, w, r⟩ ∈ impI) ⇒ ∀s [s/p]|A| ⇒ ∀t ⟨t, s, w, r⟩ ∈ subst ⇒ [t/p]|B|), -|A ∧ B| = p ∈ sn ∧ ∀q ∀r ∀s ((⟨p, q⟩ ∈ red ∧ ⟨q, r, s⟩ ∈ andI) ⇒ [r/p]|A| ∧ [s/p]|B|), -|A ∨ B| = p ∈ sn ∧ ∀q ∀r ((⟨p, q⟩ ∈ red ∧ ⟨q, r⟩ ∈ orI1) ⇒ [r/p]|A|) ∧ ∀q ∀r ((⟨p, q⟩ ∈ red ∧ ⟨q, r⟩ ∈ orI2) ⇒ [r/p]|B|), -|⊥| = p ∈ sn, -|∀x A| = p ∈ sn ∧ ∀q ∀w ∀r (⟨p, q⟩ ∈ red ∧ (⟨q, w, r⟩ ∈ f orallI) ⇒ ∀x ∀y (x ∈ E S(x) ∧ y ∈ term) ⇒ ∀s (⟨s, w, y, r⟩ ∈ subst ′ ⇒ [r/p, x/x]|A|)), -|∃x A| = p ∈ sn ∧ ∀q ∀t ∀r (⟨p, q⟩ ∈ red ∧ (⟨q, t, r⟩ ∈ existsI) ⇒ ∃x x ∈ E S(x) ⇒ [r/p, x/x]|A|)).

  1, if and only if for every e in U , |B| M ψ+σ k e/x = 1 if and only if for every e in U , B U φ+e/x = 1 if and only if A U φ = 1. if A = ∃x B then |A| M ψ = 1 if and only if there exists c in M such that c ∈ M v k and |B| M ψ+c/x = 1, if and only if there exists e in U such that |B| M ψ+σ k e/x = 1 if and only if there exists e in U such that B U φ+e/x = 1 if and only if A

  0 and hence b is in U . Definition 11 (Jensen's model). The model U = ⟨U, ∈ U , fx1,...,xn,y,A ⟩ is defined as follows. The base set is U . The relation ∈ U is defined above. The function fx1,...,xn,xn+1,A maps (a 1 , . . . , a n ) to an object b such that for all a n+1 in U , a n+1 ∈ M σb if and only if A U a1/x1,...,an/xn,an+1/xn+1 = 1. Proposition 4. The model U is a model of the Stratified Foundations.Proof. If A is a stratifiable proposition in the language ∈, then t n+1 ∈ f x1,...,xn,xn+1,A (t 1 , . . . , t n ) U /x 1 , . . . , t n /x n , t n+1 /x n+1 ]A U φ = 1 Hence, if A ≡ B then A and B have the same denotation.

			φ = 1
	if and only if
	t n+1	U φ ∈ M σ fx1,...,xn,xn+1,A ( t 1	U φ , . . . , t n	U φ )
	if and only if
	[t 1 Corollary 1. The Stratified Foundations are consistent.

  and only if π is strongly normalizable and whenever π reduces to ⟨π 1 , π 2 ⟩ then B M ψ+π1/p = 1 and C M ψ+π2/p = 1 if and only if π is strongly normalizable and whenever π reduces to ⟨π 1

  and only if π is strongly normalizable and whenever π reduces to λx π 1 , for all term t and for all c in M such that c∈ M A k , |B| M ψ+c/x,[t/x]π1/p = 1 if and only if π is strongly normalizable and whenever π reduces to λx π 1 , for all t and for all e in N , |B| M ψ+τ k e/x+[t/x]π1/p = 1 if and only if π is strongly normalizable and whenever π reduces to λx π 1 , for all t and for all e in N , [t/x]π 1 is in B N φ+e/x if and only if π is in A N φ . if A = ∃x B, then |A| M ψ+π/p = 1 if and only if π is strongly normalizable and whenever π reduces to ⟨t, π 1 ⟩, there exists a c in M such that c ∈ M A k and |B| M ψ+c/x,[t/x]π1/p = 1 if and only if π is strongly normalizable and whenever π reduces to ⟨t, π 1 ⟩, there exists a e in N such that |B| M ψ+τ k e/x+[t/x]π1/p = 1 if and only if π is strongly normalizable and whenever π reduces to ⟨t, π 1 ⟩, there exists a e in N such that [t/x]π 1 is in B N φ+e/x if and only if π is in A N φ . Then, the model M is a model of the comprehension scheme. Hence, it is a model of the proposition ∀E

  1, hence it is a reducibility candidate. Hence b 0 ∈ M A kn+1+1 and b is in N . Definition 13 (Crabbé's pre-model). The pre-model N = ⟨N, ∈ N , fx1,...,xn,y,A ⟩ is defined as follows. The base set is N . The function ∈ N is defined above. The function fx1,...,xn,xn+1,A maps (a 1 , . . . , a n ) to the object b such that for all a n+1 in N , ⟨π, a n+1 ⟩ M ∈ M τ b if and only if π is in A N a1/x1,...,an/xn,an+1/xn+1 . Proposition 8. The pre-model N is a pre-model of the Stratified Foundations. Proof. If A is a stratifiable proposition in the language ∈, then π is in t n+1 ∈ f x1,...,xn,xn+1,A (t 1 , . . . , t n ) N

φ if and only if ⟨π, t n+1 N φ ⟩ M ∈ M τ fx1,...,xn,xn+1,A ( t 1 N φ , . . . , t n N φ ) if and only if π is in [t 1 /x 1 , . . . , t n /x n , t n+1 /x n+1 ]A N φ

Hence, if A ≡ B then A and B have the same denotation.

as the first premise need not be exactly A ⇒ B but may be only congruent to this proposition, hence it is statedC A if C ≡ A ⇒ B B axiom if A ∈ Γ and A ≡ B Γ ⊢≡ B Γ, A ⊢≡ B ⇒-intro if C ≡ (A ⇒ B) Γ ⊢≡ C Γ ⊢≡ C Γ ⊢≡ A ⇒-elim if C ≡ (A ⇒ B) Γ ⊢≡ B Γ ⊢≡ A Γ ⊢≡ B ∧-intro if C ≡ (A ∧ B) Γ ⊢≡ C Γ ⊢≡ C ∧-elim if C ≡ (A ∧ B) Γ ⊢≡ A Γ ⊢≡ C ∧-elim if C ≡ (A ∧ B) Γ ⊢≡ B Γ ⊢≡ A ∨-intro if C ≡ (A ∨ B) Γ ⊢≡ C Γ ⊢≡ B ∨-intro if C ≡ (A ∨ B) Γ ⊢≡ C Γ ⊢≡ D Γ, A ⊢≡ C Γ, B ⊢≡ C ∨-elim if D ≡ (A ∨ B) Γ ⊢≡ C Γ ⊢≡ B ⊥-elim if B ≡ ⊥ Γ ⊢≡ A Γ ⊢≡ A (x, A) ∀-intro if B ≡ (∀x A) and x ̸ ∈ F V (Γ ) Γ ⊢≡ B Γ ⊢≡ B (x, A, t) ∀-elim if B ≡ (∀x A) and C ≡ [t/x]A Γ ⊢≡ C Γ ⊢≡ C (x, A, t) ∃-intro if B ≡ (∃x A) and C ≡ [t/x]A Γ ⊢≡ B Γ ⊢≡ C Γ, A ⊢≡ B (x, A) ∃-elim if C ≡ (∃x A) and x ̸ ∈ F V (Γ B) Γ ⊢≡ B


Nizar Ouarti
email: nizar.ouarti@irisa.fr

Gabriel Peyré
email: gabriel.peyre@ceremade.dauphine.fr

BEST BASIS DENOISING WITH NON-STATIONARY WAVELET PACKETS

Keywords: wavelet, wavelet packet, best basis, denoising

This article introduces a best basis search algorithm in a nonstationary (NS) wavelet packets dictionary. It computes an optimized labeled quad-tree that indexes the filters used for the NS wavelet packets decomposition. This algorithm extends the classical best basis search by exploring in a hierarchical manner the set of NS wavelet packets coefficients. The scale-by-scale variation of the filters adapts the transform to the frequency content of complex textures. The resulting denoising method is made translation invariant by cycle spinning. Numerical results show that NS wavelet packets give better results than wavelet packets and waveatoms for the denoising of natural images, in particular in textured areas. Moreover, the cycle spinning method increases significantly the denoising abilities of our algorithm 1 .

INTRODUCTION

Fixed basis denoising. Wavelet bases capture efficiently transient parts of signals and images. In particular, orthogonal wavelet bases are optimal for the approximation and denoising of piecewise smooth signals and images with bounded variations [START_REF] Mallat | A Wavelet Tour of Signal Processing[END_REF].

Natural images contain complex structures such as regular edges and oscillating textures. In the image setting, wavelets are sub-optimal to represent both textures and edges. Elongated oriented atoms such as curvelets [START_REF] Candès | New tight frames of curvelets and optimal representations of objects with piecewise C 2 singularities[END_REF] should be used to capture efficiently cartoon edges. Locally oscillating atoms such as local DCT [START_REF] Mallat | A Wavelet Tour of Signal Processing[END_REF], brushlets [START_REF] Meyer | Brushlets: A tool for directional image analysis and image compression[END_REF] or waveatoms [START_REF] Demanet | Wave atoms and sparsity of oscillatory pat-Fig. 4. Curves showing the PSNR (in dB) as a function of σ/||f || ∞ for Barbara (top) and Fingerprint (bottom). Solid curves: NS wavelet packets, dashed: WaveAtoms, dotted: wavelet packets. terns[END_REF] should be preferred to process oscillating oriented textures,.

Best basis denoising. Each of these fixed bases are well suited to process a specific kind of structures in images. A best basis algorithm computes an adapted orthogonal basis within a structured dictionary. This best basis selection is applied to a noisy image to perform an adaptive denoising. This adaptive processing can alleviate some of the difficulties that faces a fixed representation. For instance, a best wavelet packet denoising [START_REF] Coifman | Entropy-based algorithms for best basis selection[END_REF] is useful to denoise oscillating textures such as fingerprints by performing an adapted segmentation of the frequency domain.

Contribution. This paper extends the best wavelet packet adaptivity for image denoising by using non-stationary (NS) wavelet packets introduced by Cohen and Séré [START_REF] Cohen | Time-frequency localization by non-stationary wavelet packets[END_REF]. We show that the set of all bases is parameterized by a set of labeled quadtrees. We propose a new best basis selection method that extends classical dynamical programming method to the non-stationary setting. This algorithm shares similarities with the search in multi-tree dictionaries [START_REF] Huang | Fast search for best representations in multitree dictionaries[END_REF]. A translation invariant extension of the best NS wavelet packets thresholding further enhances the denoising quality by reducing denoising artifacts. Numerical results show that the resulting adaptive NS denoising method improves over wavelet packets and waveatoms denoising over textured areas.

NON-STATIONARY WAVELET PACKETS

Quadtree parameterization. A 2D NS wavelet packet basis B(λ) is parameterized by a quad-tree λ. The nodes (j, i) of λ are indexed by a scale 0 j J = log 2 (n)/2 representing the depth in the tree, and a position 0 i < 4 j . Each node (j, i) is assigned a label λ j,i ∈ {0, . . . , S -1} ∪ ∅. A leaf node is such that λ j,i = ∅, and it has no child node. We denote by L(λ) the set of leaves. An interior node (j, i) is such that λ j,i ∈ {0, . . . , S -1} and it has 4 children nodes indexed as (j + 1, 4i), . . . , (j + 1, 4i + 3). We denote by I(λ) the set of interior nodes. Figure 1 shows an example of such a quadtree λ.

Wavelet filters. Each label λ j,i indexes a 1D low pass filter chosen in a set {h ℓ } S-1 ℓ=0 . For each index ℓ, the corresponding high pass quadrature filter is g ℓ , and 2D orthogonal tensorial filters {h η ℓ } 3 η=0 are computed as

h 0 ℓ = h ℓ ⊗ h ℓ , h 1 ℓ = h ℓ ⊗ g ℓ , h 2 ℓ = g ℓ ⊗ h ℓ , h 3 ℓ = g ℓ ⊗ g ℓ .
NS wavelet packet transform. The forward NS wavelet packet transform computes coefficients of a discrete image f ∈ R n of n pixels, that are stored on the leaves L(λ) of the tree λ. The computation is performed with an iterative algorithm that follows the edges of the tree λ. It starts at scale j = 0, where f 0,0 = f . For each scale 0 < j < J = log 2 (n)/2, for each interior node (j, i) ∈ I(λ), the signals on the children nodes is defined as

W λ (f ) = {f j,i } (j,i)∈L(λ)
∀ 0 η < 4, f j+1,4i+η = (f j,i * h η ℓ ) ↓ 2 (1)
where ℓ = λ j,i is the index of the filter, and ↓ 2 is the operator that subsamples an image by a factor 2 along each direction. The backward NS wavelet packet transforms retrieves an image f = W * λ (F ) ∈ R n from a set of coefficients F = {f j,i } (j,i)∈L(λ) . For each scale J > j > 0, the signal on the interior node (j, i) ∈ I(λ) is recovered as

f j,i = 3 η=0 (f j+1,4i+η ↑ 2) * hη ℓ (2)
where h[n] = h[-n] and ↑ 2 is the upsampling operator that inserts a zero at each odd location along each direction. The image is recovered on the root node as f = f 0,0 . Both the forward and the backward transform are computed in O(n log 2 (n)) operations.

BEST NS WAVELET PACKET BASIS

Processing an image f ∈ R n is performed by modifying the coefficients of f in an optimized NS wavelet packet basis B(λ ⋆ ). The quadtree λ ⋆ is selected by minimizing a Lagrangian

L(f, B(λ)) = (j,i)∈L(λ) ρ + n/4 j -1 m=0 Φ(f j,i [m]) (3)
where {f j,i } (j,i)∈L(λ) = W λ (f ) and where Φ : R → R is a cost function that depends on the application (denoising, compression, . . . ). The parameter ρ 0 is a penalization that reduces the complexity of the best basis tree.

The tree λ ⋆ adapted to an image f is computed by exploiting the hierarchical structure of the wavelet packet coefficients.

Step 1 -Computing all the coefficients. The set of all possible NS wavelet packets coefficients is obtained by a top to bottom filtering process. The coefficients on the root node are F 0,0 = f . For each scale 0 < j < J, for each index 0 k < (4S) j , the coefficients on the 4S children nodes of F j,i are obtained by computing all possible filterings

∀ 0 ℓ < S, ∀ 0 η < 4, F j+1,4Sk+4ℓ+η = (F j,i * h η ℓ ) ↓ 2.
Step 2 -best filters selection. A bottom to top recursive selection process selects the best filters for each scale j and index 0 k < (4S) j . The Lagrangian is evaluated for each index k at the finest scale j = J

∀ 0 k < (4S) J , L J,k = n/4 J -1 m=0 Φ(F J,i [m]).
For each J < j 0, the cumulated Lagrangian is computed for each application of a filter indexed by

0 ℓ < S L ℓ j,k = ρ + 3 η=0 L j+1,4Sk+4ℓ+η .
The best filter index defines the Lagrangian at the next scale for each 0 k < (4S) j that minimizes the cumulative Lagrangian

L j,k = min min 0 ℓ<S L ℓ j,k , n/4 j m=0 Φ(F j,k [m]) .
If L j,k = L ℓ j,k for some 0 ℓ < S, the best filter choice is set to ℓ j,k = ℓ, otherwise, the filtering is stopped and ℓ j,k = ∅.

Step 3 -Best tree construction. Once the best filter choices ℓ j,k are computed for all j and all 0 k < (4S) j , the best tree λ ⋆ with indexes λ ⋆ j,i is computed for all j and all 0 i < 4 j . The initial tree is initialized with a single root node L(λ ⋆ ) = {(0, 0)}, together with a filter choice λ ⋆ 0,0 = ℓ 0,0 and with a link π 0,0 = 0.

For each 0 j < J, for each node (j, i) such that ℓ = λ ⋆ j,i = ∅, we retrieve the link k = π j,i , and add the children nodes to the leaves of the optimal tree λ ⋆ ,

L(λ ⋆ ) ← L(λ ⋆ ) ∪ {(j + 1, 4i + η)} 3 η=0 .
The label for each new node is set to

∀ 0 η < 4, λ j+1,4i+η = ℓ j+1,4Sk+4ℓ+η
and the link is defined as π j+1,4i+η = 4Sk + 4ℓ + η.

Complexity. The numerical complexity of this best basis algorithm is dominated by the computation of the set of coefficients {F j,k } (j,k) for all possible 0 j < J = log 2 (n)/2 and 0 k < (4S) j . For each scale j = 1, . . . , J, one needs to compute (4S) j filterings of vectors of size n/4 j , where n is the size of the input vector f . The overall complexity is thus

log 2 (n)/2 j=0 (4S) j n 4 j = O(n log 2 (n)) if S = 1, O(n 1+log 2 (S)/2 ) if S > 1.
(4)

BEST NS WAVELET PACKET DENOISING

We consider an additive noise model, where a noisy image is obtained as f = f 0 + ε where ε is a Gaussian white noise of variance σ 2 .

Thresholding estimator. Following Donoho and Johnstone [START_REF] Donoho | Ideal spatial adaptation via wavelet shrinkage[END_REF], an estimator fλ of f 0 is obtained by hard thresholding at T > 0 the coefficients of the decomposition of f in a NS wavelet packet basis B(λ)

fλ = W * λ S T (W λ (f )) , (5)
where the hard thresholding operator S T applies to each coefficient the non-linearity S T (x) = x if |x| > T and S T (x) = 0 otherwise. Asymptotically minimax optimal estimators are obtained by choosing T = σ 2 log e (P ) where P is number of atoms in all NS wavelet packets basis, see [START_REF] Donoho | Ideal spatial adaptation via wavelet shrinkage[END_REF]. For NS wavelet packet bases, this number is of the order of P = O(n 1+log 2 (S)/2 ). In practice, good numerical results are obtained with T ≈ 3σ, and in the numerical results, we select in an oracle manner the T value that minimizes ||f 0 -fλ ||.

Best basis for denoising. The best average denoising result is obtained by selecting the basis B(λ) that minimizes the risk E ε (||f 0 -fλ || 2 ). Following Krim et al. [START_REF] Krim | On denoising and best signal representation[END_REF], an approximation of the risk is obtained by considering the Lagrangian L(f, B(λ)) defined in (3), with the cost function

Φ(x) = x 2 -σ 2 if |x| T, σ 2 if |x| > T. (6)
In the numerical experiments, we set ρ = T 2 to penalize the complexity of the basis. The best NS wavelet packet denoising is defined as fλ ⋆ where λ ⋆ is the tree that minimizes L(f, B(λ)) with the cost [START_REF] Cohen | Time-frequency localization by non-stationary wavelet packets[END_REF].

Translation invariant denoising. Once λ ⋆ is computed, the denoising quality is greatly improved by using a cycle spinning scheme to reduce thresholding artifacts. For each translation vector τ = (τ 1 , τ 2 ), we denote as θ τ f [n] = f [n -τ ] the translated image, with periodic boundary conditions. The cycle spinning denoising is obtained with

fλ ⋆ = 1 K 2 K-1 τ1=0 K-1 τ2=0 θ -τ (θ τ f ) λ ⋆
For the numerical results, we use K = 4, which increases by K 2 = 16 the numerical complexity of the last step of our method.

Original PSNR=19.6dB WaveAtoms PSNR=24.4dB

WavePackets PSNR=23.7dB NSWP PSNR=25.4dB

Fig. 2. Comparison of denoising methods on Barbara image.

NUMERICAL RESULTS

For the numerical experiments, we use S = 6 Daubechies orthogonal filters {h ℓ } S-1 ℓ=0 , where h ℓ is a filter of length 2ℓ + 2.

Figure 2 shows denoising results on a natural image that contains oscillating textures, that is degraded with a noise level σ = 0.15||f || ∞ . The translation invariant NS wavelet packets improves both over a translation invariant wavelet packet denoising [START_REF] Coifman | Entropy-based algorithms for best basis selection[END_REF] and over the WaveAtoms denoising [START_REF] Demanet | Wave atoms and sparsity of oscillatory pat-Fig. 4. Curves showing the PSNR (in dB) as a function of σ/||f || ∞ for Barbara (top) and Fingerprint (bottom). Solid curves: NS wavelet packets, dashed: WaveAtoms, dotted: wavelet packets. terns[END_REF], that are both known for their efficiency to restore oscillating textures. Figure 3 shows an example of denoising of a fingerprint texture, for σ = .2||f || ∞ . Switching from orthogonal NS wavelet denoising to translation invariant denoising leads to a PSNR improvement of 2dB on this texture. This shows the importance of this cycle spinning extension. Original PSNR=18.0dB NSWP PSNR=24.5dB Fig. 3.

Denoising of a fingerprint texture using the NS wavelet packet algorithm with cycle spinning.

CONCLUSION

This article has presented a new algorithm to compute a best basis in a non-stationary wavelet packets dictionary. Thresholding the NS wavelet packets coefficients in a best basis computed from a noisy observation performs an adaptive denoising of the image. The translation extension of this thresholding is competitive with the state of the art methods to denoise oscillating textures.

Fig. 1 .

 1 Fig. 1. Example of quadtree λ that defines a 2D NS wavelet packet basis B(λ).

This work is supported by ANR grant NatImages ANR-08-EMER-009.


Georges Gras
email: g.mn.gras@wanadoo.fr

NEW CHARACTERIZATION OF THE NORM OF THE FUNDAMENTAL UNIT OF Q( √ M )

Keywords: Mathematics Subject Classification. Primary 11R11, 11R27, 11R29, 11R37 Real quadratic fields, Fundamental unit, Norm of units, Class field theory, PARI programs

We give an elementary criterion for the norm of the fundamental unit ε

Introduction -Main result

Let K =: Q( √ M ), M ∈ Z ≥2 square-free, be a real quadratic field and let Z K be its ring of integers. Recall that M is called the "Kummer radical" of K, contrary to any "radical" R = M r 2 giving the same field K. We will write the elements of Z K under the form α = 1 2 (u + v √ M ), with u, v of same parity. We denote by T K/Q =: T and N K/Q =: N, the trace and norm maps in K/Q, so that T(α) = u and N(α) = 1 4 (u 2 -M v 2 ). We denote by ε K > 1 the fundamental unit of K and by S K =: S := N(ε K ) ∈ {-1, 1} its norm. An obvious necessary condition for S = -1 is to have -1 ∈ N(K × ), equivalent to the fact that any odd prime ramified in K/Q is congruent to 1 modulo 4.

The starting point of our result is the following observation proved by means of elementary applications of class field theory (see Theorem 2.1 assuming -1 ∈ N(K × ) and Remark 2.2 (iii) in the case -1 / ∈ N(K × )):

Set M = q|M q for the prime divisors q of M and let q | q be the prime ideal of

K = Q( √ M
) over q. The fundamental unit ε K of K is of norm -1 if and only if the relation q = ( √ M ) is the unique non-trivial relation of principality (in the ordinary sense) between the ramified prime ideals of K (that is to say, the q's dividing ( √ M ) and q 2 | 2 if 2 ∤ M ramifies, whence if M ≡ 3 (mod 4)).

Of course, when -1 / ∈ N(K × ) and when 2 ∤ M ramifies, one can verify the existence of a relation of principality, either of the form q eq (distinct from (1) and ( √ M )) with exponents in {0, 1}, or else q 2 principal (e.g., M = 3 × 17 with q 2 principal, the ideals q 3 and q 17 being non-principal; for more examples and comments, see Remark 2.2 (iii)).

Then we can state the main result, under the assumption -1 ∈ N(K × ) (see Theorem 2.4 for more details and informations):

Theorem 1.1. Let ε K = a + b √ M > 1, a, b ∈ Z or 1 2
Z, be the fundamental unit of K. We consider the integers A + B √ M and A ′ + B ′ √ M , defined as follows:

ε K + 1 = a + 1 + b √ M =: g (A + B √ M ), where g := gcd (a + 1, b) ∈ Z >0 , ε K -1 = a -1 + b √ M =: g ′ (A ′ + B ′ √ M )
, where g ′ := gcd (a -1, b) ∈ Z >0 .

Let m := gcd (A, M ) and m ′ := gcd (A ′ , M ). Then we have:

(i) If M is odd, ε K is of norm -1 if and only if m = m ′ = 1. (ii) If M is even, ε K is of norm -1 if and only if m = m ′ = 2.
Let D ≤X be the set of discriminants D ≤ X corresponding to quadratic fields K such that -1 ∈ N(K × ) and let D - ≤X the subset of discriminants such that S := N(ε K ) = -1, and put ∆ - disc := lim for the density ∆ - disc = 0.5805..., has been proved from techniques developed by [START_REF] Koymans | On Stevenhagen's conjecture[END_REF], in relation with that of Smith [Sm], based on estimations of the 2 k -ranks of the class groups of the K's, k ≥ 2. It raises the question of whether our point of view can constitute a way to define another notion of density since it does not seem compatible with the common principle of classification of the fields via their discriminants; this will be discussed in Section 3.

Characterizations of N(ε

K ) = -1
In this Section, we give (Theorems 2.1, 2.4) a new characterization of the norm S of the fundamental unit ε K of K = Q( √ M ) when -1 ∈ N(K × ), in particular for the case S = -1 giving the solvability of the norm equation u 2 -M v 2 = -4, u, v ∈ Z >0 .

2.1. Class field theory results involving N(ε K ). We will use the classical class field theory context given by the Chevalley-Herbrand formula and by the standard exact sequence defining the group of invariant classes (for simplicity, we refer to our book [Gra1], but any classical reference book may agree). Of course, in the case of quadratic fields, the theory is equivalent to that of quadratic forms and goes back to Gauss and, after that in a number field context, to Kummer, Hilbert, Takagi, Hasse, Chevalley-Herbrand, Frölich, Furuta, Ishida, Leopoldt, for particular formulas in the area of genus theory, but we are convinced that the general framework may be used, for instance, in relative quadratic extensions K/k, since the index (E k : NE K ) of groups of units, when

E k ⊂ N(K × ), is as mysterious as (E Q : NE K ) for K = Q( √ M ), when -1 ∈ N(K × ) (for some examples in this direction, see [Gra2, Théorème 3.2, Corollaires 3.3, 3.4]). Theorem 2.1. Consider Kummer radicals M = q 1 • • • q r or M = 2 • q 2 • • • q r , r ≥ 1, with odd primes q i ≡ 1 (mod 4) (r = 1 gives M = q 1 or M = 2) and let K = Q( √ M ).
If the prime q (odd or not) divides M we denote by q the prime ideal of K above q.

(i) The fundamental unit ε K is of norm S = -1 if and only if the relation

q|M q = ( √ M )
is the unique relation of principality, distinct from (1), between the ramified prime ideals of K (this relation and the trivial one will be called the canonical relations).

(ii) In the case S = 1, the unique non-canonical relation m = q|m q = (α), of support m | M distinct from 1 and M , is given by ε K + 1 =: g α, where the rational integer g is maximal and, similarly, the complementary relation n = q|n q = (β), of support n = M m distinct from 1 and M , is given by ε K -1 =: g ′ β where the rational integer g ′ is maximal.

Proof. (i) Let G := Gal(K/Q) =: σ . The Chevalley-Herbrand formula [START_REF] Chevalley | Sur la théorie du corps de classes dans les corps finis et les corps locaux, Thèse 155[END_REF] gives, for the ordinary 2-class group

H K , #H G K = 2 r-1 ( -1 : -1 ∩ N(K × )) = 2 r-1
since -1 ∈ N(K × ) by assumption. Moreover, we have the classical exact sequence:

(2.1)

1 → H ram K -→ H G K -→ -1 ∩ N(K × )/ S = -1 / S → 1, where H ram K
is the subgroup generated by the classes of the ramified prime ideals q of K. Indeed, for an invariant class of an ideal a, one associates with (α

) := a 1-σ , α ∈ K × , the sign N(α) = ±1 ∈ -1 ∩ N(K × ) = -1 , defined modulo S since α is defined modulo E K := -1, ε K .
• Image. Since there exists β ∈ K × such that -1 = N(β), the ideal (β), being of norm (1), is of the form b 1-σ , giving a pre-image in H G K (surjectivity). • Kernel. If a 1-σ =: (α) with N(α) = S, one may suppose, up to a unit, that N(α) = 1, whence α = θ 1-σ (Hilbert's Theorem 90), and a(θ) -1 is an invariant ideal, product of a rational ideal by a product of ramified prime ideals of K.

This yields

#H ram K = 2 r-1 ( -1 : S )
, where we recall that r is the number of ramified prime ideals of K; let's examine each case for S:

If S = -1, then #H ram K = 2 r-1
and the unique non-trivial relation of principality between the ramified primes is the canonical one, q = ( √ M ).

If S = 1, then #H ram K = 2 r-2
, necessarily with r ≥ 2, and another relation of principality does exist, given by a suitable product q eq = (α), e q ∈ Z; since any q 2 is principal, one may write the relation under the form m = (ii) From m = (α) when S = 1, we get

α 1-σ = ±ε k K , k ∈ Z; since ε 2 K = ε 1+σ+1-σ K = ε 1-σ K , we may assume that m = (α) with α 1-σ ∈ {±1, ±ε K }. If α 1-σ = ±1, then α ∈ {1, √ M } × Q × gives the canonical relations (absurd); thus α 1-σ = ±ε K . If for instance α 1-σ = 1, then (α √ M ) 1-σ = -1 and this gives the complementary relation n = (β) with β 1-σ = -ε K .
Since we have (ε

K + 1) 1-σ = ε K + 1 ε σ K + 1 = ε K + 1 ε -1 K + 1 = ε K and similarly (ε K -1) 1-σ = -ε K , the quotients ε K + 1 α and ε K -1 β
are invariants under σ, hence are rational numbers; this proves the second claim of the theorem writing ε K + 1 = gα and ε K -1 = g ′ β in an obvious manner (g and g ′ are the maximal rational integer factors of the quadratic integers ε K ± 1).

Remarks 2.2. (i) If r = 1, one finds again the well-known result S = -1 for the prime Kummer radicals M = q ≡ 1 (mod 4) and for M = 2. The properties given by Theorem 2.1, due to the Chevalley-Herbrand formula, come from the "product formula" of Hasse's norm residue symbols in class field theory [Gra1, Theorem II.3.4.1].

(ii) The theorem is also to be related with that of Trotter [START_REF] Trotter | On the Norms of Units in Quadratic Fields[END_REF]Theorem,p. 198] leading, in another framework, to the study of the equations mx 2 -ny 2 = ±4, equivalent to the principalities of m and n, since, for instance, m = ( 1 2 (x + y √ M )) is equivalent to x 2 -M y 2 = ±4m, whence mx 2 -ny 2 = ±4; then, some sufficient conditions of solvability of these equations are given by means of properties of suitable quadratic residues.

Remark 2.3. We intend to give some properties of the case M = q 1 • • • q r odd, when one assumes that -1 / ∈ N(K × ) (there exists q | M such that q ≡ 3 (mod 4)), then S = 1, the

Chevalley-Herbrand formula becomes #H G K = 2 r+δ-1 ( -1 : -1 ∩ N(K × ))
= 2 r+δ-2 , where δ = 1 (resp. 0) if M ≡ 3 (mod 4) (resp. if not) and the exact sequence (2.1) becomes the isomorphism

H ram K ≃ H G K .
Nevertheless, if M ≡ 1 (mod 4) (thus an even number of primes q ≡ 3 (mod 4) dividing M ), we have δ = 0, so that one obtains the pair of non-canonical relations of principality from the computation of m and n from ε K ± 1. Now, we assume that M ≡ 3 (mod 4) implying the ramification of 2 with M odd and S = 1. So we have δ = 1, #H ram K = 2 r-1 and the existence of a group of relations of principality of order 4 between the r + 1 ramified primes, including the canonical ones.

• If q 2 | 2 is principal, this gives the non-canonical relation, and the process using ε K ± 1 only gives the canonical relations (1) and ( √ M ).

• If q 2 | 2 is not principal, this implies the existence of a non-canonical relation of principality, distinct from (1) and ( √ M ). We intend to show that this relation is not of the form q 2 • m principal, for m distinct from (1) and ( √ M ). Otherwise, we have:

(2.2) q 2 m = (α) and q 2 n = (β), mn = ( √ M ), whence the existence of units ε, ε ′ such that: α 2 ε = 2m and β 2 ε ′ = 2n; modulo the squares of units one may choose α and β such that:

α 2 = ±2m or α 2 ε K = ±2m and β 2 = ±2n or β 2 ε K = ±2m.
The cases ±2m and ±2n does not hold since the Kummer radical M is unique. So:

(2.3)

α 2 ε K = 2m and β 2 ε K = 2n.
In the same way, we have, from the principality relations (2.2), α 1-σ = η and β 1-σ = η ′ that we may write (using

ε 2 K = ε 1-σ K since S = ε 1+σ K = 1): α 1-σ = ±1 or α 1-σ = ±ε K and β 1-σ = ±1 or β 1-σ = ±ε K .
As above, the cases ±1 are excluded (e.g.,

α 1-σ = ±1 gives α ∈ Q × or Q × • √ M ). Thus: (2.4) α 1-σ = ±ε K and β 1-σ = ±ε K .
From (2.3) one gets the relation α 2 β 2 ε 2 K = 2m 2n = 4M and then αβε K = ±2 √ M , giving (αβε K ) 1-σ = -1. Using relations (2.4), the previous relation leads to: 78 [2,3,13]

±ε K • ε K • ε 2 K = -1 (absurd). So, when q 2 is non-principal,
26 3 [1] q2 non principal [3,11] 11 3 [] D=M 79 [79] 1 79 [0] q2 principal [5,7] 5 7 [1] q2 non principal 83 [83] 83 1 [] q2 principal [2,19] 2 19 [] 86 [2,43] 43 2 [] [3,13] 13 3 [1] q2 non principal 87 [3,29] 3 29 [1] q2 non principal [2,3,7] 6 7 [1] q2 non principal 91 [7,13] 13 7 [1] q2 non principal [43] 1 43 [] q2 principal 93 [3,31] 31 3 [] D=M [2,23] 2 23 [] 94 [2,47] 2 47 [] [47] 1 47 [] q2 principal 95 [5,19] 5 19 [1] q2 non principal
The mention D = M means that 2 does not ramify, so it does not intervene in the relations; the mention q2 principal is then the unique non-canonical relation and the mention q2 non principal occurs when 2 ramifies but there exists a pair of non-canonical relations (m, n) given in the left column. A box [ ] means a trivial class group and [0] is equivalent to the principality of q 2 when the class group in non-trivial and [a, b, ...], with not all zero a, b, ..., gives the components of the class of q 2 on the PARI basis of the class group.

The first "non-trivial" example is M = 51, where ε 51 = 50 + 7 √ 51, giving ε 51 + 1 = 51 + 7 √ 51 (m = 51) and ε 51 -1 = 7 (7 + √ 51) (n = 1), thus the canonical relations.

The case -1 / ∈ N(K × ) being without any mystery regarding the norm S, we will assume -1 ∈ N(K × ) in the sequel.

2.2. Computation of the non-canonical relations of principality. The following program computes, when -1 ∈ N(K × ) and S = 1, the non-canonical relations of principality between the ramified primes of K to make statistics and notice that any kind of relation seems to occur with the same probability for r fixed.

It uses the arithmetic information given by the PARI instructions K = bnfinit(x 2 -M) and bnfisprincipal(K, A) testing principalities. When S = -1, the program gives only the trivial list L = List([1, 1, 1, 1]) corresponding to the canonical relation. The parameter Br forces r ≥ Br. As illustration, let's give examples, for r = 5, of the relations of principality m = (α), n = (β), by means of the exponents [e 1 , ..., e r ] given by the list L and where the radical M is given via the list of its prime divisors; for instance: 2,5,13,17,37] L = List([0,1,0,1,1]), means q 5 • q 17 • q 37 principal (or q 2 • q 13 principal).

M = [

Main characterization of N(ε

K ). Assume that -1 ∈ N(K × ) and let S := N(ε K ).
When S = 1, the non-canonical relation m = q|m q = (α), of support m | M distinct from 1 and M , comes from Theorem 2.1 (ii); it suffices to determine the quadratic integer α, without any rational factor, deduced from ε K + 1, this giving m. In the same way

ε K -1 gives n = (β) of support n = M m such that mn = (αβ) = ( √ M ).
Let's give some numerical examples of the process leading to the result:

(i) For M = 15170 = 2 • 5 • 37 • 41, ε K = 739 + 6 √ M and: ε K + 1 = 740 + 6 √ M = 2 × (370 + 3 √ M ),
where 2 = gcd (740, 6); then gcd (370, M ) = 370 = 2 • 5 • 37, whence the principality of m = q 2 q 5 q 37 , which immediately gives the principality of q 41 that can be obtained from:

-ε K + 1 = -738 -6 √ M = -6 × (123 + √ M ),
for which gcd (123, M ) = 41.

(ii) For M = 141245 = 5 • 13 • 41 • 53, ε K = 49609 + 132 √ M and:

ε K + 1 = 49610 + 132 √ M = 22 × (2255 + 6 √ M ),
where 22 = gcd (49610, 132) and gcd (2255, M ) = 5 • 41 giving the principality of q 5 q 41 , and the principality of q 13 q 53 , also obtained from

-ε K + 1 = -12 × (4134 + 11 √ M ) and gcd (4134, M ) = 13 • 53. (iii) For M = 999826 = 2 • 41 • 89 • 137, ε K + 1 is given by: 11109636935777158836160759499956087745610931184259730878643242570969499893 0608609351188823863817034706422630544237192750927410464023060264033743426 +111106036003421265074388547121779710827974912909282096975471217501055084 481117390502436801341332286005566466631729812289759396153149523058885768 √ M
with the gcd of the two coefficients equal to:

21082286734619551653000708969094423248037542899079230940776043942241398 =2 × 3 × 43 × 11210269457991049 × 7289235104943832975100088612482411236091543240227619, giving the integer A + B √ M ∈ Z K equal to: 5269654604181931962753271711433450204598096091653697788648087227648861999187 +5270113123970195868835491287611281655343354587474034791159597224413298316 √ M
then gcd (A, M ) = 41 × 89 × 137, giving the principality of: q 41 q 89 q 137 =(5269654604181931962753271711433450204598096091653697788648087227648861999187

+5270113123970195868835491287611281655343354587474034791159597224413298316 √ M )
or simply that of q 2 . Theorem 2.4. Let M ≥ 2 be a square-free integer and put

K = Q( √ M ); we assume that -1 ∈ N(K × ). Let ε K = a + b √ M (a, b ∈ Z or 1 2 Z) be the fundamental unit of K. We consider the following integers A + B √ M , A ′ + B ′ √ M ∈ Z K , A, B, A ′ , B ′ ∈ Z or 1 2 Z
, where the gcd function must be understood in Z K , giving for instance, gcd (1 2 U 0 , 1 2 V 0 ) = gcd (U 0 , V 0 ) for U 0 and V 0 odd; in other words one may see g and g ′ below as the maximal rational integer factors of the quadratic integers:

1 ε K + 1 = a + 1 + b √ M =: g (A + B √ M ), g := gcd (a + 1, b), ε K -1 = a -1 + b √ M =: g ′ (A ′ + B ′ √ M ), g ′ := gcd (a -1, b). Let m := gcd (A, M ), n = M m , C = A m , m ′ := gcd (A ′ , M ), n ′ = M m ′ , C ′ = A ′ m ′ . (i) If M is odd, ε K is of norm S = 1 if and only if (m, m ′ ) = (1, 1). If M is even, ε K is of norm S = 1 if and only if, either m > 2 or else m ′ > 2. In other words, the characterization of S = -1 becomes: If M is odd, ε K is of norm S = -1 if and only if m = m ′ = 1. If M is even, ε K is of norm S = -1 if and only if m = m ′ = 2. (ii)
If the above conditions giving S = 1 hold, then q|m q = (α) and q|n q = (β),

with α = C m + B √ M and β = B n + C √ M in Z K .
Proof. We do not consider the particular case r = 1 giving S = -1 and H G K = H ram K = 1; we prove the characterization of S = 1 of the statement.

• Let's assume S = 1: Recall, from Theorem 2.1, that since (ε K + 1) 1-σ = ε K , the ideal (ε K + 1) gives, after elimination of its maximal rational factor, the unique non-canonical relation of principality m = (α), of support m | M , m = 1, M , between the ramified primes.

Since ( √ M • (ε K + 1)) 1-σ = -ε K and (ε K -1) 1-σ = -ε K , the ideals ( √ M • (ε K + 1)) (leading to n = (β) of support n = M m
) and (ε K -1) (leading to m ′ = (α ′ ) of support m ′ ) yield the same non-canonical relations of supports n and m ′ , so that n = m ′ , with m, n distinct from 1, M .

One obtains the suitable condition m = 1 and m ′ = n = 1 when M is odd; if M is even, the integers m, m ′ = n are of different parity, distinct from 1 and M and such that mm ′ = M > 2; so, if we assume, for instance, m ≤ 2 (hence m = 2), this implies

m ′ = M m > 2. • Reciprocal. We assume m = 1 (resp. m > 2 or m ′ > 2) if M is odd (resp. even): In the odd case, ε K ≡ -1 (mod m), m of support m, implies ε σ K ≡ -1 (mod m), whence S = ε 1+σ K ≡ 1 (mod m) thus S = 1 since m = 1 implies m > 2 in the odd case.
In the even case, since m > 2 or m ′ > 2, the same conclusion holds, using one of the congruence

ε K ≡ -1 (mod m) or ε K ≡ 1 (mod m ′ ) (note that in the reciprocal one does not know if m ′ = n).
• The characterization of S = -1 is of course obvious, but the precise statement is crucial for statistical interpretation, especially in the even case:

-In the odd case, one gets m = m ′ = 1.

-In the even case, one gets m ≤ 2 & m ′ ≤ 2, but we have m = 1 and

m ′ = 1; indeed, let ε K = a + b √ M , a, b ∈ Z,
where a 2 -M b 2 = -1 implies a and b odd (the case of a is obvious, so a 2 ≡ 1 (mod 8), then b even would imply 1 ≡ -1 (mod 8)). Since ε K ≡ 1 (mod q 2 ) with b odd, necessarily ε K ≡ 1 (mod 2) and (ε K + 1) = q 2 a, where a is an odd ideal and, except for M = 2, one gets a = 1, then (ε σ Remark 2.5. (i) In the case M even with S = -1, the ideals (ε K ± 1) do not define invariant classes (except that of

q 2 in Q( √ 2) since (ε 2 + 1) = (2 + √ 2) = √ 2 • ε 2 and (ε 2 -1) = ( √ 2
); this comes from the fact that it is the unique even case where H G K = 1). But q 2 is not principal since there is no non-canonical relation of principality in the case S = -1 (e.g., M ∈ {10, 26, 58, 74, 82, 106, 122, 130, 170}).

To get illustrations for M even, S = -1, the following program computes the class group of K (in HK = K.clgp), then (in R) the components of the (non-trivial) class of q 2 :

{forstep(M=2,10^6,2,if(core(M)!=M,next);K=bnfinit(x^2-M,1); S=norm(K.fu[1]);if(S==1,next);q2=component(idealfactor(K,2),1)[1]; R=bnfisprincipal(K,q2)[1];print("M=",M," R=",R," HK=",K.clgp))} M=10 R=[1] HK=[2,[2]] M=199810 R=[0,0,1,1] HK=[128,[16,2,2,2]] M=82 R=[2] HK=[4,[4]] M=519514 R=[32,1] HK=[128,[64,2]] M=130 R=[0,1] HK=[4,[2,2]] M=613090 R=[32,0,1] HK=[256,[64,2,2]] M=226 R=[4] HK=[8,[8]] M=690562 R=[16,2] HK=[128,[32,4]] M=442 R=[0,1] HK=[8,[4,2]] M=700570 R=[8,1,0,1] HK=[128,[16,2,2,2]] M=2210 R=[1,1,1] HK=[8,[2,2,2]] M=720802 R=[16,0] HK=[128,[32,4]] M=3026 R=[2,2]
HK= [16,[4,4]] M=776866 R=[16,0,0] HK= [128,[32,2,2]]

But we have the cases M even and S = 1 (e.g., M ∈ {34, 146, 178, 194, 386, 410, 466, 482, 514, 562}), where relations q 2 principal are more frequent when r is small (e.g., M ∈ {34, 146, 178, 194, 386, 466, 482}; for M = 410, the relation is given by m = 41, n = 10).

(ii) Consider the field

L = K( √ 2) for M even, M =: 2M ′ ; the extension L/K is unramified since Q( √ M ′ )/Q is not ramified at 2. The extension of q 2 in L becomes the principal ideal ( √ 2) whatever the decomposition of 2 in Q( √ M ′ )/Q. Meanwhile, if 2
is inert in this extension (i.e., M ′ ≡ 5 (mod 8)), q 2 can not be principal in K, otherwise, if q 2 = (α), then, in L, α = η √ 2, where η is a unit of L, and by unicity of radicals (up to K × ) this is absurd and the class of q 2 capitulates in L.

So either m = 2 & m ′ = 2, with q 2 non-principal and S = -1 (e.g., M ∈ {10, 26, 58, 74, 82, 106, 122} showing that reciprocal does not hold since 2 may split in

Q( √ M ′ )/Q, as for M = 82), or else m = 2 & m ′ > 2,
giving the principality of q 2 and S = 1 (e.g., all the previous cases M ∈ {34, 146, 178, 194, 386, 466, 482}).

2.4. Computation of S by means of the gcd criterion. The following PARI/GP program computes (if any) the non-canonical relation of principality m distinct from (1), ( √ M ) between the ramified primes, only by means of the previous result on the coefficients of the fundamental unit (Theorem 2.4), and deduces the norm S without calculating it; when there are no non-canonical relations (whence S = -1), the corresponding data is empty. One has only to give the bound BD of the discriminants D whose odd prime divisors are congruent to 1 modulo 4. The counters CD, Cm, Cp, C22, enumerate the sets D, D -, D + and the set D - 22 of cases where m = m ′ = 2 (equivalent to M even and S = -1), respectively; for short we do not write the cases where m = 1, giving S = -1 (M ∈ {5, 13, 17, 29, 37, . . .}:

MAIN PROGRAM COMPUTING S VIA THE RELATIONS OF PRINCIPALITY {BD=10^7;CD=0;Cm=0;Cp=0;C22=0;for(D=5,BD,v=valuation(D,2);if(v!=0 & v!=3,next); i0=1;M=D;if(v==3,M=D/4;i0=2);if(core(M)!=M,next);if(Mod(M,4)==3,next); r=omega(M);f=factor(M);ellM=component(f,1);for(i=i0,r,ell=ellM[i]; if(Mod(ell,4)==3,next(2)));CD=CD+1;res=lift(Mod(M,2));e=quadunit(D); Y=component(e,3)/(res+1);X=component(e,2)+res*Y;g=gcd(X+1,Y);m=gcd((X+1)/g,M); if(m==1,S=-1;print("D=",D," M=",M," relations: "," ",","," ",", S=",S);Cm=Cm+1); if(m>2,S=1;print("D=",D," M=",M," relations: ",m,",",M/m,", S=",S);Cp=Cp+1); if(m==2,gp=gcd(X-1,Y);mp=gcd((X-1)/gp,M); if(mp>2,S=1;print("D=",D," M=",M," relations: ",m,",",mp,", S=",S);Cp=Cp+1); if(mp==2,S=-1;print("D=",D," M=",M," relations: "," ",","," ",", S=",S,","," m=mp=2"); Cm=Cm+1;C22=C22+1))); print("CD=",CD," Cm=",Cm," Cp=",Cp," C22=",C22); print("Cm/CD=",Cm/CD+0.0," Cp/CD=",Cp/CD+0.0); print("C22/CD=",C22/CD+0.0," C22/Cm=",C22/Cm+0.0

Remarks on density questions

A classical principle in number theory is to examine some deep invariants (as class groups, units, etc.) of families of fields (assuming, in general, that some parameters are fixed, as for instance, the Galois group, the signature, etc.), classified regarding the discriminants. The analytic reason is that the order of magnitude of

h K • R K √ D K is controlled
by suitable ζ-functions and then, if the discriminant D K increase in the family, the class number h K and/or the regulator R K increase or, at least, have a larger complexity. This case represents the reality quite well in a global context, but it can be questioned for p-adic framework or non semi-simple Galois setting. We intend to give some remarks in this direction about the norm of S = N(ε K ) linked significantly to the 2-class group.

3.1. Classical approach of the density. We will describe the case of S = -1, using the following definitions:

Definitions 3.1. (i) Denote by M (resp. D) the set of all Kummer radicals (resp. of all Discriminants), such that -1 ∈ N(K × ). We have, from a result of Rieger [Rie]:

#M ≤X ≈ 3 2π p≡1 mod 4 1 - 1 p 2 1 2 X log(X) ≈ 0.464592... X log(X) , #D ≤X ≈ 3 4 #M ≤X .
(ii) Denote by M -⊂ M (resp. D -⊂ D) the subset of all Kummer radicals (resp. of all Discriminants), such that S := N(ε K ) = -1 and put:

∆ - disc := lim X→∞ M - ≤X M ≤X = lim X→∞ D - ≤X D ≤X .
Many heuristics have given ∆ - disc around 0.5 or 0.6. Our characterization would give a density around 3 2 • 6 π 2 2 ≈ 0.554363041753..., but without a precise classification by means of ascending discriminants or of number of ramified primes, a context using structure of the 2-class group, whence quadratic symbols, Rédei's matrices, Furuta symbols [Fu], etc. These classical principles consist in using the filtration of the 2-class group following, e.g., the theoretical algorithm described in whole generality in [Gra3], with the fixed point formulas generalizing that of Chevalley-Herbrand (say for the quadratic case):

#(H i+1 K /H i K ) = 2 r-1 (Λ i K : Λ i K ∩ N(K × )) , i ≥ 0,
where

H i K = Ker(1 -σ) i , the Λ i K 's, with Λ i K ⊆ Λ i+1 K for all i, defining a sequence of suitable subgroups of Q × ; more precisely, Λ 0 K = -1 , Λ 1 K = -1, q 1 , • • • , q r , the next Λ i+1 K 's introducing "random" numbers b = N(b) from identities of the form a = (y)b 1-σ , when x ∈ Λ i K is such that (x) = N(a) = N(y), cl(a) ∈ H i K , y ∈ K × . Then the index (Λ i K : Λ i K ∩ N(K × )) being nothing else than #ρ i K (Λ i K )
, where ρ i K is the r-uple of Hasse's norm residue symbols giving rise to generalized "Rédei matrices of quadratic residue symbols", or more simply, random maps F ri 2 → F r-1 2 (product formula of the symbols), r i = dim F2 Λ i K /(Λ i K ) 2 . Similar viewpoints are linking the norm of ε K to the structure of the 2-class group in the restricted sense (see many practical examples in [START_REF] Gras | Sur la norme du groupe des unités d'extensions quadratiques relatives[END_REF]).

This proportion of D -inside D ([St, § 1, p. 122], [BoSt, (1.3), p. 1328]), was conjectured by Stevenhagen to be:

P = 1 - k≥0 1 - 1 2 1+2k ≈ 0.5805775582 . . .
We refer to [St], then to [START_REF] Fouvry | On the negative Pell equation[END_REF][START_REF] Koymans | On Stevenhagen's conjecture[END_REF] for history and bibliographical comments about the norm of the fundamental unit of Q( √ M ) and for his heuristic based on the properties of densities P t , corresponding to discriminants having t distinct prime factors.

These results involving the 2-class groups structures allow informations about ∆ - disc and especially the determination of lower and upper bounds. For this aspect, we refer to the Chan-Koymans-Milovic-Pagano paper [CKMP] who had proven that ∆ - disc is larger than 0.538220, improving Fouvry-Klüners results [START_REF] Fouvry | The parity of the period of the continued fraction of √ d[END_REF][START_REF] Fouvry | On the negative Pell equation[END_REF] saying that ∆ - disc lies between 0.524275 and 0.6666666, which gave 0.538220 ≤ ∆ - disc ≤ 0.6666666.

For X = 10 8 , a PARI [P] calculation gives the experimental density

#D - ≤X #D ≤X ≈ 0.787255.
Moreover, it is well known that such partial densities decrease as X increases; in other words, computer approaches are misleading as explained in [St]. More precisely the arithmetic function ω(x) giving the number of prime divisors of x fulfills the optimal upper bound ω(x) ≤ (1 + o(1))

log(x) log(log(x))

[Ten, I.5.3], so that large Kummer radicals have "more prime divisors", whence more important probability to get S = -1.

In the present paper, we do not use these classical ways, so that the main question is to understand how densities may be defined; let's give the example of classification by ascending traces before giving that of the gcd criterion.

3.2. Classification by ascending traces of fundamental units. In another direction, let's apply the "First Occurrence Process" algorithm [START_REF] Gras | Unlimited lists of fundamental units of quadratic fields -Applications[END_REF]Section 4,Theorem 4.6] in the interval [1, B], simultaneously for the two cases s = -1 and s = 1 of the polynomials m s (t) = t 2 -4s, under the condition -1 ∈ N(K × ) (to be checked only for s = 1).

Recall that in the set

T ≤B of traces T(ε K ) ≤ B, T + ≤B , T - ≤B , denote the corresponding subsets of traces t ≤ B of fundamental units, of norm s = -1, s = 1, respectively.
As B → ∞, all units are represented in these lists, as shown with the following PARI program. Indeed, this is clear with t 2 + 4 = M r 2 giving T - ≤B , and from [Gra4, Theorem 4.6 and Corollaries], the set T + ≤B deals with minimal traces t for which t 2 -4 = M r 2 gives the unit ε K (if S = 1) or ε 2 K (if S = -1), but the squares of units of norm -1 were obtained with t 2 + 4 for a smaller trace, so that the process eliminates this data in the final list. Finally the densities dp, dm are that of units of norms 1, -1, respectively.

PROGRAM FOR DENSITY OF UNITS OF NORM 1 AND OF NORM -1 {B=10^6;Cm=0;Cp=0;LM=List;for(t=1,B,mtm=t^2+4;M=core(mtm);L=List([M,-1]); listput (LM,vector(2,c,L[c]));mtp=t^2-4;if(mtp<=0,next);M=core(mtp); r=omega(M);i0=1;if(Mod(M,2)==0,i0=2);f=factor(M);ellM=component(f,1); T=1;for(i=i0,r,c=ellM [i]

;if(Mod(c,4)!=1,T=0;break));if(T==1,L=List([M,1]); listput(LM,vector(2,c,L[c]))));VM=vecsort(vector(B,c,LM[c]),1,8);print(VM); for(k=1,#VM,S=VM[k][2];if(S==1,Cp=Cp+1);if(S==-1,Cm=Cm+1)); print("#VM=",#VM," Cp=",Cp," Cm=",Cm," dp=",Cp/#VM+0.," dm=",Cm/#VM+0.)} In that context, ε K = a + b √ M is written 1 2 (t + r √ M
) and only units with too large traces are missing in the above finite list. Restricting to the density ∆ - trace of the set of units of norm -1 inside the set of units classified by ascending traces, one gets:

Theorem 3.2. We have ∆ - trace := lim B→∞ #T - ≤B #T ≤B = 1. Proof. From [Gra4, Theorem 4.5], we have #T - ≤B ∼ B -O( 3 √ B).
3.3. Approximations of the density from the gcd principle. Theorem 2.4, on the characterization of the norm S of ε K , allows heuristics for densities since the statement reduces to elementary arithmetic properties. The criterion only depends on properties of m = gcd (A, M ) and m ′ = gcd (A ′ , M ) whose "probabilities" may be computed, assuming that the the pairs (A, M ) and (A ′ , M ) are random with Kummer radicals taken in the subset of square-free integers, without using the natural order of radicals or discriminants, nor that of the order of magnitude of the integers A, A ′ depending on the unpredictable trace of the unit. Before giving some heuristics, we introduce the partial densities corresponding to the six cases summarized by the following array, with numerical values obtained for M in various intervals [bM, BM]:

M ∈ [bM, BM ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 ↓ δ even 2,2 even = 2 > 2 = 1 ↓ δ even 2,m ′ even > 2 = 2 = 1 ↓ δ even m,2 even > 2 > 2 = 1 ↑ δ even m,m ′ odd = 1 = 1 -1 ↓ δ odd 1,1 odd > 2 > 2 = 1 ↑ δ odd m,m ′
Notations of partial densities are given in the right column; the densities δ even 2,m ′ and δ even m,2 , corresponding to each sign in formulas of ε K ± 1, are indistinguishable about the cases m = 2 & m ′ > 2 or m > 2 & m ′ = 2, so we will only give the sum δ even 2,m ′ + δ even m,2 . Then δ even 2,2 represent the cases M even, S = -1 where q 2 is not principal. The densities δ odd 1,1 (resp. δ odd m,m ′ ) represent the cases S = -1 with no principality relations (resp. S = 1 with the two complementary principality relations). We put ∆ - gcd := δ odd 1,1 + δ even 2,2 . Many tests, using the following program, have been done and have shown that some densities increase while the others decrease as the Kummer radicals are taken in larger intervals (indicated with arrows ↑ and ↓): {bM=2;BM=10^6;CM=0;C22=0;C2p=0;Cm2=0;Cmp=0;CC11=0;CCmp=0; for(M=bM,BM,res8=Mod(M,8);if(res8!=1&res8!=2&res8!=5,next); if(core(M)!=M,next);res=Mod(M,2);i0=1;if(res==0,i0=2); r=omega(M);f=factor(M);ellM=component(f,1);for (i=i0,r,ell=ellM[i]; if(Mod(ell,4)==3,next(2)));D=M;if(res==0,D=4*M);CM=CM+1;e=quadunit(D); res=lift(res);Y=component(e,3)/(res+1);X=component(e,2)+res*Y; g=gcd(X+1,Y);A=(X+1)/g;m=gcd(A,M);gp=gcd(X-1,Y);Ap=(X-1)/gp;mp=gcd(Ap,M); if (res==0, if(m==2 & mp==2,C22=C22+1)

;if(m==2 & mp>2,C2p=C2p+1); if(m>2 & mp==2,Cm2=Cm2+1);if(m>2 & mp>2,Cmp=Cmp+1)); if(res==1, if(m==1 & mp==1,CC11=CC11+1);if(m>2 & mp>2,CCmp=CCmp+1
))); print("CM=",CM," C22=",C22," C2p=",C2p," Cm2=",Cm2," Cmp= ",Cmp, " CC11=",CC11," CCmp= ",CCmp); d22=C22/CM+0.0;d2p=C2p/CM+0.0;dm2=Cm2/CM+0.0; dmp=Cmp/CM+0.0;dd11=CC11/CM+0.0;ddmp=CCmp/CM+0.0; print("Sum=",C22+C2p+Cm2+Cmp+CC11+CCmp); print ("d22=",d22," d2p=",d2p," dm2=",dm2," dmp=",dmp, " dd11=",dd11," ddmp=",ddmp)

} M ∈ [1, 10 6 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2347176480 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0652421881 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0389107558 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5475861515 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1135432564 ↑ δ odd m,m ′ CM = 124490, C22 = 29220C2p = 4079, Cm2 = 4043, Cmp = 4844, CC11 = 68169, CCmp = 14135, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3388705920 ↓, δ even 2,2 = 0.2347176480 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1041529440 ↑, δ odd 1,1 + δ odd m,m ′ = 0.6611294079 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.7823037995 ↓. M ∈ [10 6 , 10 7 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2312433670 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0614862378 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0452699271 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5374200520 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1245804159 ↑ δ odd m,m ′ CM = 1029889, C22 = 238155, C2p = 31753, Cm2 = 31571, Cmp = 46623, CC11 = 553483, CCmp = 128304, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.33767663 ↓, δ even 2,2 = 0.2312433670 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1067561648 ↑, δ odd 1,1 + δ odd m,m ′ = 0.66232334 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.768663419 ↓. M ∈ [10 7 , 10 8 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2290897913 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.058607396 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0497431369 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5297912763 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1327683993 ↑ δ odd m,m ′ CM = 9652809, C22 = 2211360, C2p = 283421, Cm2 = 282305, Cmp = 480161, CC11 = 5113974, CCmp = 1281588, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3374403243 ↓, δ even 2,2 = 0.2290897913 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1083505329 ↑, δ odd 1,1 + δ odd m,m ′ = 0.6625596756 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = .7588810676 ↓. M ∈ [10 8 , 10 8 + 10 6 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2285032150 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0571186698 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0518491039 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5276699767 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1348590343 ↑ δ odd m,m ′ CM = 105132, C22 = 24023, C2p = 2971, Cm2 = 3034, Cmp = 5451, CC11 = 55475, CCmp = 14178, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3374709887 ↓, δ even 2,2 = 0.2285032150 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1089677737 ↑, δ odd 1,1 + δ odd m,m ′ = 0.662529011 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.7561731917 ↓. M ∈ [10 9 , 10 9 + 10 6 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2262061480 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0563555787 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0540844730 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5226055410 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1407482589 ↑ δ odd m,m ′ CM = 99511, C22 = 22510, C2p = 2808, Cm2 = 2800, Cmp = 5382, CC11 = 52005, CCmp = 14006, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3366461999 ↓, δ even 2,2 = 0.2262061480 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1104400517 ↑, δ odd 1,1 + δ odd m,m ′ = 0.6633538000 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.748811689 ↓. M ∈ [10 10 , 10 10 + 10 6 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2252429443 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0535799257 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0571751842 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5164271590 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1475747866 ↑ δ odd m,m ′ CM = 94569, C22 = 21301, C2p = 2494, Cm2 = 2573, Cmp = 5407, CC11 = 48838, CCmp = 13956, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3359980543 ↓, δ even 2,2 = 0.2252429443 ↓, (δ even 2,m ′ + δ even δ even m,2 ) + δ even m,m ′ = 0.1107551099 ↑, δ odd 1,1 + δ odd m,m ′ = 0.6640019456 ↑, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.7416701033 ↓. M ∈ [10 11 , 10 11 + 2.5•10 5 ] m m ′ S = N(ε K ) densities δ even = 2 = 2 -1 0.2240462381 ↓ δ even 2,2 even = 2, > 2 > 2, = 2 = 1 0.0514559794 ↓ δ even 2,m ′ + δ even m,2 even > 2 > 2 = 1 0.0607678259 ↑ δ even m,m ′ odd = 1 = 1 -1 0.5127736860 ↓ δ odd 1,1 odd > 2 > 2 = 1 0.1509562704 ↑ δ odd m,m ′ CM = 49829, C22 = 11164, C2p = 1308, Cm2 = 1256, Cmp = 3028, CC11 = 25551, CCmp = 7522, δ even 2,2 + (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.3362700435 ↓↑, δ even 2,2 = 0.2240462381 ↓, (δ even 2,m ′ + δ even m,2 ) + δ even m,m ′ = 0.1122238054 ↑, δ odd 1,1 + δ odd m,m ′ = 0.6637299564 ↑↓, ∆ - gcd = δ even 2,2 + δ odd 1,1 = 0.7368199241 ↓.
3.3.1. First heuristic from the above data. It is difficult to go further because of the execution time, but some rules appear, that are not proved, but allow possible heuristics:

• δ even := δ even 2,2 + δ even 2,m ′ + δ even m,2 + δ even m,m ′ → 1 3 ; • δ odd := δ odd 1,1 + δ odd m,m ′ → 2 3
; this is almost obvious since random Kummer radicals M , such that -1 ∈ N(K × ), are in the classes 1, 2 or 5 modulo 8, whence with uniform repartition 1 3

for M even (class of 2) and 2 3

for the case M odd (classes of 1 and 5).

The indications ↑ and ↓ give some interesting phenomena:

• δ even m,m ′ must have a hight increasing, since δ even 2,m ′ and δ even m,2 are decreasing, but the sum δ even 2,m ′ + δ even m,2 + δ even m,m ′ is increasing. • δ even 2,2 must have a hight decreasing, since δ even = δ even 2,2 + δ even 2,m ′ + δ even m,2 + δ even m,m ′ is decreasing while the partial sum δ even 2,m ′ + δ even m,2 + δ even m,m ′ is increasing. • The sum ∆ - gcd = δ odd 1,1 + δ even 2,2 is much decreasing.

• The quotient

δ even 2,2 δ odd 1,1
seems to be increasing and the quotient

δ odd 1,1 δ odd m,m ′
seems to be rapidly decreasing.

• The quotient

δ even 2,2
δ even 2,m ′ + δ even m,2 + δ even m,m ′ seems to be decreasing up to a constant ρ ≈ 2.

To reinforce this last heuristic, let's consider the computation of the parity of the component b of ε K = a + b √ M , for M even and -1 ∈ N(K × ); indeed, recall that in that cases S = -1 is equivalent to b odd. The following program examines this question taking M ≡ 2 (mod 8), in the intervals [k * 10 7 , (k + 1) * 10 7 ], k ≥ 1: Many oscillations can be observed, on the successive intervals [k * 10 7 , (k + 1) * 10 7 ], which support the idea of a slow convergence of CI/CP towards ρ = 2 + .

With the same principle, but in intervals of the form [k * 10 9 , k * 10 9 + 10 7 ], k ≥ 1 (long calculation time), we obtain, as expected, a slow global decreasing of the data: To conclude, one may say that these heuristics are compatible with the next one suggesting that δ odd 1,1 → 6 π 2 2 ≈ 0.3695..., then ∆ - gcd := δ odd 1,1 + δ even 2,2 → 6 π 2

1
2 (1 + 0.5) ≈ 0.5543....

3.3.2.

Second heuristic from randomness of A, A ′ . In our viewpoint, we are reduced to use the well-known fact that the density of pairs of independent co-prime integers is 6 π 2 ≈ 0.6079...; but this implies that no condition is assumed, especially for a radical R taken at random, and we must take into account that a radical lies in the subset of square-free integers, whose relative density is also given by 6 π 2 . The integers a ± 1 giving A, A ′ may be considered as random and independent regarding M .

• When M is odd, S = -1 is equivalent to m := gcd (A, M ) = 1; which gives the partial density δ odd 1,1 = 6 π 2

2

.

• When M is even, S = -1 is equivalent to m ′ := gcd (A ′ , M ) = 2 and this may be written

m ′ 2 := gcd A ′ 2 , M 2
= 1; we know this is equivalent to b odd and that a good heuristic is that this occur with probability 1 2 . The specific case m = 2 (with the alternative m ′ > 2 or m ′ = 2) occurs only for M even, whence a coefficients ≈ 0.554363041753.

To be compared with the density 0.5805775582 [St, Conjecture 1.4], proven in [START_REF] Koymans | On the distribution of Cl(K)[ℓ ∞ ] for degree ℓ cyclic fields[END_REF][START_REF] Koymans | On Stevenhagen's conjecture[END_REF] depending on the natural order of discriminants.

Our method, assumes the independence and randomness of the parameters; moreover it does not classify the radicals (or discriminants), nor the units (for example by means of their traces), so one can only notice that the density (3.1) may be an lower bound for the classical case; fortunately it is greater than the lower bound 0.538220, which was proved in [CKMP], and also less than 0.666666..., proved in [START_REF] Fouvry | The parity of the period of the continued fraction of √ d[END_REF][START_REF] Fouvry | On the negative Pell equation[END_REF].

  q|m q = (α) of support m | M . For n = M m we get the non-canonical analogous relation n = q|n q = (β), with mn = (αβ) = ( √ M ); which proves the first claim.

π 2 2 ;

 2 densities; indeed, M even andWe then obtain the following discussion, on m and m ′ , from Theorem 2.4:• m = 1 (M ofany parity); thus S = -1 with density 6 • m = m ′ = 2 (M even); thus S = -1 with density the previous interpretation, we propose, for D -inside D, the conjectural

  the non-canonical relations are of the form m and n, given by the usual process. Let's give few examples using Program 2.4:

	M	relations		M	relations
	3 [3]	1	3	[] q2 principal	51 [3,17]	1	51 [0] q2 principal
	6 [2,3]	2	3	[]	55 [5,11]	11 5	[1] q2 non principal
	7 [7]	1	7	[] q2 principal	57 [3,19]	3	19 [] D=M
	[11]	1	11 [] q2 principal	59 [59]	59 1	[] q2 principal
	[2,7]	7	2	[]	62 [2,31]	2	31 []
	[3,5]	3	5	[1] q2 non principal	66 [2,3,11] 33 2	[0]
	[19]	1	19 [] q2 principal	67 [67]	67 1	[] q2 principal
	[3,7]	3	7	[] D=M	69 [3,23]	23 3	[] D=M
	[2,11]	2	11 []	70 [2,5,7] 14 5	[1] q2 non principal
	[23]	1	23 [] q2 principal	71 [71]	1	71 [] q2 principal
	[2,3,5] 5	6	[1] q2 non principal	77 [7,11]	7	11 [] D=M
	[31]	1	31 [] q2 principal

The PARI/GP gcd function gives instead gcd ( 1

U 0 , 1 2 V 0 ) = 12 gcd (U 0 , V 0 ); this gap only occurs when M is odd, in which case this does not matter for the computation of the odd integers m and m ′ .