Olivier Garet
email: olivier.garet@iecn.u-nancy.fr

R Égine Marchand
email: regine.marchand@iecn.u-nancy.fr

MODERATE DEVIATIONS FOR THE CHEMICAL DISTANCE IN BERNOULLI PERCOLATION

Keywords: 2000 Mathematics Subject Classification. 60K35, 82B43 Percolation, chemical distance, moderate deviations, concentration inequalities, subadditivity

In this paper, we establish moderate deviations for the chemical distance in Bernoulli percolation. The chemical distance between two points is the length of the shortest open path between these two points. Thus, we study the size of random fluctuations around the mean value, and also the asymptotic behavior of this mean value. The estimates we obtain improve our knowledge of the convergence to the asymptotic shape. Our proofs rely on concentration inequalities proved by Boucheron, Lugosi and Massart, and also on the approximation theory of subadditive functions initiated by Alexander.

Introduction and results

We consider supercritical Bernoulli percolation on the edges of Z d , where d ≥ 2 is a fixed integer. The set of edges of Z d is denoted by E d and the set Ω = {0, 1} E d is endowed with the probability P = B(p) ⊗E d : the coordinates (ω e ) e∈E d are thus independent and identically distributed random variables following the Bernoulli law with parameter p. We denote by p c (Z d ) the critical point for Bernoulli percolation on Z d , and in the following, p > p c (Z d ) is fixed.

We denote by C ∞ the infinite percolation cluster. The chemical distance between two points x, y ∈ Z d is the length of the shortest open path between these two points. Asymptotically, this chemical distance is equivalent to a deterministic norm µ -see Garet and Marchand [START_REF] Garet | Asymptotic shape for the chemical distance and firstpassage percolation on the infinite Bernoulli cluster[END_REF]. Moreover, we even obtain large deviations inequalities in [START_REF] Garet | Large deviations for the chemical distance in supercritical Bernoulli percolation[END_REF]:

∀ε > 0 lim y 1→+∞ log P 0 ↔ y, D(0,y) µ(y) / ∈ (1 -ε, 1 + ε) y 1 < 0.
Our main results here are the following moderate deviation estimates:

Theorem 1.1. There exists a constant C 1 > 0 such that

(1) ∀y ∈ Z d E |D(0, y) -µ(y)| 1 1 {0↔y} ≤ C 1 y 1 log(1 + y 1 ).
There exist constants A 2 , B 2 , C 2 > 0 such that ∀y ∈ Z d \{0}, ∀x ∈ [C 2 (1 + log y 1 ), y

1/2 1 ] P |D(0, y) -µ(y)| y 1 > x, 0 ↔ y ≤ A 2 e -B2x . ( 2
)
There exists a constant C 3 > 0 such that, P-almost surely, on the event {0 ↔ ∞}, for t large enough,

(3) B 0 µ (t -C 3 √ t log t) ∩ C ∞ ⊂ B 0 (t) ⊂ B 0 µ (t + C 3 √ t log t),
where B 0 (t) = {x ∈ Z d : D(0, x) ≤ t} is the ball with radius t for the chemical distance and B 0 µ (t) is the ball with radius t for the norm µ . In Kesten's work on first-passage percolation, the analogue of Inequality (2) is valid for x ∈ [0, y 1 ]. Note however that for x ∈ [ y 1 , y 1 ], the large deviation estimates are more accurate; on the other hand, we cannot extend our results for x ∈ [0, C 2 (1 + log y 1 )] because of the approximation and renormalization process we use in the proof.

Let us note first that the chemical distance between two points is infinite as soon as these points are not in the same open cluster: to overcome this problem, we introduce a variation of the chemical distance in the following way: for x ∈ Z d , we denote by x * the closest point to x in C ∞ (for the . 1 -distance). For indeterminate cases, we choose x * to minimize x * -x for a given deterministic rule, as the lexicographic order for instance. Then, we define: ∀x, y ∈ Z d D * (x, y) = D(x * , y * ).

We will mainly work with D * and we will come back to the chemical distance D by bounding the discrepancy between the two quantities. Here are the results we obtain for D * : Theorem 1.2. There exists a constant C 4 > 0 such that [START_REF] Benaïm | Exponential concentration for first passage percolation through modified Poincaré inequalities[END_REF] ∀y ∈ Z d Var D * (0, y) ≤ C 4 y 1 log(1 + y 1 ).

For every D 5 > 0, there exist constants A 5 , B 5 , C 5 > 0 such that for each y ∈ Z d \{0}, for each x ∈ [C 5 (1 + log y 1 ), D 5 y 1 ],

(5) P |D * (0, y) -E[D * (0, y)]|

y 1 > x ≤ A 5 e -B5x .
There exists a constant C 6 > 0 such that

(6) ∀y ∈ Z d \{0} 0 ≤ E[D * (0, y)] -µ(y) ≤ C 6 y 1 log(1 + y 1 ).
The last two inequalities easily give some constants A 7 , B 7 , C 7 > 0 such that for every y ∈ Z d \{0},

(7) ∀x ∈ [C 7 (1 + log y 1 ), y 1 ] P |D * (0, y) -µ(y)| y 1 > x ≤ A 7 e -B7x .
As in first-passage percolation (see Kesten [START_REF] Kesten | On the speed of convergence in first-passage percolation[END_REF]), the proof naturally falls into two parts:

• the control of the random fluctuations of D * (0, x) around its mean value (concentration property), • the control of the discrepancy between the mean value of D * (0, x) and µ(x). In his original work, Kesten used martingale technics. Such technics were also used by Howard and Newman [START_REF] Howard | Euclidean models of first-passage percolation[END_REF][START_REF] Howard | Geodesics and spanning trees for Euclidean first-passage percolation[END_REF] for Euclidean first-passage percolation (see also the survey by Howard [START_REF] Howard | Models of first-passage percolation[END_REF]) and by Pimentel [START_REF] Pimentel | Asymptotics for first-passage times on Delaunay triangulations[END_REF] for the Vahidi-Asl and Wierner model. Since then, the concentration method developed by Talagrand [START_REF] Talagrand | Concentration of measure and isoperimetric inequalities in product spaces[END_REF] offered a new approach to this kind of problems and allowed to improve Kesten's estimates. In the same spirit, Benaïm and Rossignol [START_REF] Benaïm | Exponential concentration for first passage percolation through modified Poincaré inequalities[END_REF] managed to enhance variance estimates in first-passage percolation. Here, we bound the fluctuations (4) and ( 5) thanks to recent concentration inequalities of Boucheron, Lugosi and Massart [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF], which are easier to use than the abstract result of Talagrand.

The control [START_REF] Chayes | The correlation length for the high-density phase of Bernoulli percolation[END_REF] of the discrepancy between E[D * (0, y)] and µ(y) usually relies on the moderate deviations estimates for the fluctuations of D * (0, x) around its mean value; it is particularly clear for the models with spherical symmetry such as Euclidean first-passage percolation [START_REF] Howard | Euclidean models of first-passage percolation[END_REF][START_REF] Howard | Geodesics and spanning trees for Euclidean first-passage percolation[END_REF]. A symmetry argument can also give simple proofs in the main direction, see Alexander [START_REF] Alexander | A note on some rates of convergence in first-passage percolation[END_REF]. Since this argument does not apply in an arbitrary direction, we choose to use the technics developed by Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF] for the approximation of subadditive functions.

The paper is organized as follows: in Section 2, we give some estimates for the chemical distance D and its variation D * , that are mainly derived from Antal and Pisztora's results [START_REF] Antal | On the chemical distance for supercritical Bernoulli percolation[END_REF]; we also deduce Theorem 1.1 for D from Theorem 1.2 for D * . In Section 3, we prove Inequalities (4) and ( 5) of Theorem 1.2, using concentration inequalities of Boucheron, Lugosi and Massart on one hand, and a mesoscopic renormalization argument on the other hand. Section 4 is devoted to the control of the discrepancy (6) between µ(x) and E[D * (0, x)], following Alexander's method.

2. Some inequalities 2.1. Classical estimates. For each x in Z d , we denote by C(x) the percolation cluster of x; |C(x)| is its cardinal. Thanks to Chayes, Chayes, Grimmett, Kesten and Schonmann [START_REF] Chayes | The correlation length for the high-density phase of Bernoulli percolation[END_REF], we can control the radius of finite clusters: there exist constants A 8 , B 8 > 0 such that [START_REF] Efron | The jackknife estimate of variance[END_REF] ∀r

> 0 P |C(0)| < +∞, C(0) ⊂ [-r, . . . , r] d ≤ A 8 e -B8r .
We can also control the size of the holes in the infinite cluster: there exist two strictly positive constants A 9 et B 9 such that [START_REF] Garet | Asymptotic shape for the chemical distance and firstpassage percolation on the infinite Bernoulli cluster[END_REF] ∀r

> 0 P C ∞ ∩ [-r, . . . , r] d = ∅ ≤ A 9 e -B9r .
When d = 2, this result follows from the large deviation estimates by Durrett and Schonmann [START_REF] Durrett | Large deviations for the contact process and twodimensional percolation[END_REF]. Their methods can easily be transposed when d ≥ 3. Nevertheless, when d ≥ 3, the easiest way to obtain it seems to use Grimmett and Marstrand [START_REF] Grimmett | The supercritical phase of percolation is well behaved[END_REF] slab's result.

2.2.

Estimates for the chemical distance. The following lemma is a consequence of an auxiliary result obtained by Antal and Pisztora [START_REF] Antal | On the chemical distance for supercritical Bernoulli percolation[END_REF]. This lemma actually contains the two theorems stated in their article.

Lemma 2.1. There exist positive constants α 10 , β 10 such that

(10) ∀y ∈ Z d E[e α101 1 {0↔y} D(0,y) ] ≤ e β10 y 1 .
Proof. Inequality (4.49) in Antal-Pisztora [START_REF] Antal | On the chemical distance for supercritical Bernoulli percolation[END_REF] says that there exist an integer N and a real c > 0 such that ∀ℓ ≥ 0 P(0 ↔ y, D(0, y) > ℓ) ≤ P n i=0

(|C i | + 1) > ℓcN -d ,
where the C i 's are independent identically distributed random sets, such that there exists h > 0 with E[exp(h|C i |)] < +∞, and n is an integer with n ≤ y 1 /2N , which leads to n + 1 ≤ y 1 . Thus, for each ℓ > 0, P(0 ↔ y, D(0, y) ≥ ℓ) ≤ P(0 ↔ y, D(0, y) > ℓ/2)

≤ P n i=0 (|C i | + 1) > ℓ 2 cN -d ≤ P   y 1 i=1 2N d c (|C i | + 1) ≥ ℓ   .
Of course, the last inequality remains true for ℓ ≤ 0, which proves that

1 1 {0↔y} D(0, y) µ * y 1 ,
where µ is the distribution of

P(0 ↔ y, D(0, y) > t) ≤ e -α10t E[e α101 1 {0↔y} D(0,y) ] ≤ e β10 y 1-α10 t .
To get [START_REF] Grimmett | The supercritical phase of percolation is well behaved[END_REF], we take ρ > 2 β10 α10 .

2.3.

Estimates for the modified chemical distance D * . We now show some estimates for D * that are analogous to the ones that we have obtained for the chemical distance D:

Lemma 2.3. There exist some constants ρ * , A 12 , B 12 , α 13 , β 13 , A 14 , B 14 > 0 such that, for each y ∈ Z d :

∀t ≥ ρ * y 1 P(D * (0, y) > t) ≤ A 12 exp(-B 12 t), (12)
E[e α13D * (0,y) ] ≤ e β13 y 1 , (13) (D * (0, y) -ρ * y 1 ) + 2 ≤ A 14 exp(-B 14 y 1 ). ( 14)

Proof. Let λ = 1
4ρ and ρ * = 2ρ. Since D * (0, y) = D(0 * , y * ), we have

P(D * (0, y) > t) ≤ P( 0 * 1 ≥ λt) + P( y * -y 1 ≥ λt) + a 1≤λt b-y 1 ≤λt P(1 1 {a↔b} D(a, b) > t).
The first and second terms are controlled with [START_REF] Garet | Asymptotic shape for the chemical distance and firstpassage percolation on the infinite Bernoulli cluster[END_REF]. If t ≥ ρ * y 1 , then for each term in the sum, we have:

a -b 1 ≤ y 1 + 2λt ≤ t 2ρ + 2λt = t ρ ,
which permits to use the bound in [START_REF] Grimmett | The supercritical phase of percolation is well behaved[END_REF], and hence completes the proof of (12 8) about the radius of large finite clusters makes us able to prove that on the event {0 ↔ y}, the quantities D(0, y) and D * (0, y) coincide with a huge probability: indeed, on the event {0 ↔ y, 0 ↔ ∞}, the identity D(0, y) = D * (0, y) holds, and we can bound the probability

P(0 ↔ y, 0 ↔ ∞) ≤ A 8 e -B8 y 1 .
Proof of Theorem 1.1. We begin with the proof of (1). Let y ∈ Z d .

E(|D(0, y) -µ(y)|1 1 {0↔y} ) = E(|D(0, y) -µ(y)|1 1 {0↔y, 0↔∞} ) + E(|D(0, y) -µ(y)|1 1 {0↔y, 0 ↔∞} ).
On one hand, with the Cauchy-Schwarz inequality and the estimates [START_REF] Grimmett | The supercritical phase of percolation is well behaved[END_REF] and ( 8), we have

E(|D(0, y) -µ(y)|1 1 {0↔y,0 ↔∞} ) ≤ (D(0, y) -µ(y))1 1 {0↔y} 2 P(0 ↔ y, 0 ↔ ∞) ≤ ( D(0, y)1 1 {0↔y} 2 + µ(y)) P(0 ↔ y, 0 ↔ ∞) = o y 1 log(1 + y 1 ) .
On the other hand, with the inequalities ( 6) and ( 4) in Theorem 1.2,

E(|D(0, y) -µ(y)|1 1 {0↔y,0↔∞} ) = E(|D * (0, y) -µ(y)|1 1 {0↔y,0↔∞} ) ≤ E(|D * (0, y) -µ(y)|) ≤ |E[D * (0, y)] -µ(y)| + Var (D * (0, y)) ≤ C 6 y 1/2 1 log(1 + y 1 ) + (C 4 y 1 log(1 + y 1 )) 1/2 ,
which proves [START_REF] Alexander | A note on some rates of convergence in first-passage percolation[END_REF]. Now we turn to the proof of (2). Let y ∈ Z d . For each x ∈ [C 7 (1 + log y 1 ), y 1 ], Inequality [START_REF] Durrett | Large deviations for the contact process and twodimensional percolation[END_REF] in Theorem 1.2 and the estimate (8) ensure that

P |D(0, y) -µ(y)| y 1 > x, 0 ↔ y ≤ P |D * (0, y) -µ(y)| y 1 > x + P(0 ↔ y, 0 ↔ +∞) ≤ A 7 e -B7x + A 8 e -B8 y 1 . Since x ≤ y 1 ≤ y 1 , this proves (2)
. The proof of ( 3) is standard from (2) -see for instance the proof of Theorem 3.1 in Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF].

Moderate deviations

We prove here the concentration results ( 4) and ( 5) for D * . The proof is of course based on Kesten's one [START_REF] Kesten | On the speed of convergence in first-passage percolation[END_REF]; however, to overcome the lack of integrability of the chemical distance, we use an approximation and renormalization process: for a real t > 0 and any k ∈ Z d , we denote by Λ t k the set of edges whose centers are closer from tk than from any other point of the grid tZ d (in equality cases, we use an arbitrary deterministic rule to associate the edge to a unique box). We say that a point in Z d is in the box Λ t k if it is the extremity of an edge in this box: thus, the boxes (Λ t k ) k∈Z d partition the set of edges E d , but not the set of points Z d . We denote by D t (a, b) the distance obtained from the chemical distance as follows: if two points x and y are in the same box Λ t k , we add an extra red edge between them with length Kt, where K is a constant such that K > 4ρ. For t large enough, we will check with Lemma 3.3 that D * (0, y) and D t (0 * , y * ) are really close.

Since D t (0, y) can by deterministically bounded, we can localize optimal paths in a deterministic box, which was not the case with D * . Thus we can use a concentration result of Boucheron, Lugosi and Massart [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF] to bound the fluctuations of D t (0, y) around E[D t (0, y)]: Lemma 3.1. For every C 15 > 0, there exist constants B 15 , γ > 0 such that for every y ∈ Z d \{0}, [START_REF] Kesten | On the speed of convergence in first-passage percolation[END_REF] ∀x ≤ C 15 y

1/2 1 P |D γx (0, y) -E[D γx (0, y)]| y 1 ≥ x ≤ 2 exp(-B 15 x).
Proof. Let C 15 > 0, y ∈ Z d and t > 0 be fixed. One of the ingredients of the proof is the existence of exponential moments for D t (0, y), which mainly follows from the existence of exponential moments for D * . First, since we may use red edges, (16)

D t (0, y) ≤ Kt y 1 t + 1 = K( y 1 + t).
Let us now see that there exist constants α, β, η > 0 such that

(17) ∀y ∈ Z d \{0} ∀t > 0 log E(exp(αD t (0, y)) ≤ β y 1 + ηt.
Note first that the triangle inequality and ( 16) ensure that

D t (0, y) ≤ D t (0, 0 * ) + D t (0 * , y * ) + D t (y * , y) ≤ K(2t + 0 -0 * 1 + y -y * 1 ) + D * (0, y).
With Hölder's inequality, we get

E(exp(αD t (0, y)) ≤ exp(2αKt)[E exp(3αK 0 -0 * 1 )] 2/3 [E exp(3αD * (0, y))] 1/3 .
Inequalities ( 9) and ( 13) give then the announced control [START_REF] Steele | An Efron-Stein inequality for nonsymmetric statistics[END_REF]. By [START_REF] Pimentel | Asymptotics for first-passage times on Delaunay triangulations[END_REF], any path realizing D t (0, y) stays inside a finite deterministic box: the quantity D t (0, y) only depends on the edges inside a finite family of mesoscopic boxes (Λ t k ) k∈Z d , that we number from 1 to N . Let U 1 , . . . , U N be the random vectors such that U i contains the states of the edges in box number i. There exists a function S = S y,t such that

D t (0, y) = S(U 1 , . . . , U N ). Note that the (U i ) are independent. Let U ′ 1 , . . . , U ′ N be independent copies of U 1 , . . . , U N ; set S (i) = S(U 1 , . . . , U i-1 , U ′ i , U i+1 , .
. . , U N ) and

V + = E N i=1 ((S -S (i) ) + ) 2 |U 1 , . . . , U N , V -= E N i=1 ((S -S (i) ) -) 2 |U 1 , . . . , U N .
We can already note, with the Efron-Stein-Steele inequality (see Efron-Stein [START_REF] Efron | The jackknife estimate of variance[END_REF] and Steele [START_REF] Steele | An Efron-Stein inequality for nonsymmetric statistics[END_REF] or Proposition 1 in Boucheron, Lugosi and Massart [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF]) that ( 18)

Var D t (0, y) ≤ E[V -].
Moreover, Theorem 2 in Boucheron, Lugosi and Massart [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF] gives the following concentration inequalities: for every λ, θ > 0 such that λθ < 1:

log E[exp(λ(S -E[S]))] ≤ λθ 1 -λθ log E exp λV + θ , (19) log E[exp(-λ(S -E[S]))] ≤ λθ 1 -λθ log E exp λV - θ . ( 20
)
Let M t (y, z) denote the shortest path for D t between y and z, chosen with any deterministic rule in undetermined cases. If we denote by R i the event "M t (0, y) crosses box number i", we can see that S (i) -S ≤ Kt1 1 Ri . Thus, if Y denotes the number of boxes visited by M t (0, y), then

K 2 t 2 Y is an upper bound for V -. Since Y ≤ 3 d (1 + D t (0, y)/t), this leads to (21) V -≤ 3 d K 2 t(D t (0, y) + t).
This bound, together with the existence of exponential moments for D t (0, y), allows to bound the lower fluctuations. On the other hand, we cannot obtain such a simple bound for V + . Instead, we use a variant of Inequality (19), which was given to us by R. Rossignol and M. Théret: Lemma 3.2. Assume there exist δ > 0, real functions (ϕ i ) 1≤i≤n , (ψ i ) 1≤i≤n and (g i ) 1≤i≤n such that for any i,

(S -S (i) ) -≤ ψ i (U ′ i ) and (S -S (i) ) 2 -≤ ϕ i (U ′ i )g i (U 1 , . . . , U n ) and α i = E[e δψi(Ui) ϕ i (U i )] < +∞. If W = n i=1 α i g i (U 1 , . . . , U n ), then for every θ > 0 and every λ ∈ [0, min(δ, 1 θ )), log E[exp(λ(S -E[S]))] ≤ λθ 1 -λθ log E exp λW θ . ( 22
)
Remember that S (i) -S ≤ Kt1 1 Ri ; thus we can take ϕ i = ψ i = Kt, g i = 1 1 Ri and α i = Kte δKt ; we get

W = K 2 t 2 e δKt Y ≤ 3 d K 2 te δKt 3 d (D t (0, y) + t).
To recover an inequality similar to (21), we choose δ = 1/t:

(23) max(V -, W ) ≤ 3 d K 2 e K t(D t (0, y) + t).
Both sides can then be treated simultaneously, we only need to keep track of the two conditions: λ < 1/θ and λ < 1/t. Let us take the constants α, β, η given in [START_REF] Steele | An Efron-Stein inequality for nonsymmetric statistics[END_REF], and choose λ, t > 0 such that

λ < 1/t, λ 2 ≤ 1 2 α 3 d K 2 e K t . Setting θ = λ3 d K 2 e K t α
, the condition θλ ≤ 1/2 is satisfied, so we can use (20) and ( 22). Since λ θ 3 d K 2 e K t = α, estimates ( 23) and ( 17)

say that λθ 1 -λθ log E exp λV - θ ≤ 2λθ log E[exp(α(D t (0, y) + t))] ≤ 2.3 d K 2 e K α λ 2 t(β y 1 + (η + α)t) ≤ Lλ 2 (t y 1 + t 2 ), ( 24
)
where L is a constant such that L ≥ 2.3 d K 2 e K α max(β, η + α) and L ≥ C 15 /2 -the last condition will be used at the very end of the proof. Similarly,

(25) λθ 1 -λθ log E exp λW θ ≤ Lλ 2 (t y 1 + t 2 ).
Thus, for any u > 0 and any λ, t > 0 such that λ < 1/t and λ 2 ≤ 1 2 α 3 d K 2 e K t , the Markov inequality, (20) and ( 22) ensure that

P |D t (0, y) -E[D t (0, y)]| > u ≤ 2 exp(-λu + Lλ 2 (t y 1 + t 2 )). But taking λ = x y 1/2 1 2Lt( y 1 + t) < x 2Lt y 1/2 1
, we get

x ≤ 2L y 1/2 1 , x 2 ≤ 2α 3 d L 2 K 2 e K t y 1 ⇒ λ < 1/t, λ 2 ≤ 1 2 α 3 d K 2 e K t
and taking now u = x y 1 , we obtain

P |D t (0, y) -E[D t (0, y)]| y 1 ≥ x ≤ 2 exp - x 2 y 1 4Lt( y 1 + t) . At last, taking t = γx with γ = 3 d α K 2 e K
L , we see that

x ≤ 2L y 1/2 1 ⇒ λ < 1/t, λ 2 ≤ 1 2 α
and we obtain, for any x ≤ C 15 y

1/2 1 ≤ 2L y 1/2 1 : P |D γx (0, y) -E[D γx (0, y)]| y 1 > x ≤ 2 exp - x 4Lγ × 1 1 + 2Lγ ,
which ends the proof of Lemma 3.1.

Lemma 3.3. There exist constants A 26 , B 26 , A 27 , B 27 > 0 such that for every y ∈ Z d and every t ≤ y 1 ,

P(D t (0 * , y * ) = D * (0, y)) ≤ A 26 (1 + y 1 ) 2d exp(-B 26 t), (26)
D * (0, y) -D t (0 * , y * ) 2 ≤ A 27 (1 + y 1 ) d+1 exp(-B 27 t). (27) Proof. Set Γ = {x ∈ Z d : x 1 ≤ 3ρ * y 1 )} and L = {M t (0 * , y * ) ⊂ Γ}, A = ∩ a,b∈Γ: a-b 1≥t {1 1 {a↔b} D(a, b) ≤ 2ρ a -b 1 }, B = ∩ a∈Γ {a ∈ C ∞ or C(a) ⊂ [-t, . . . , t] d }.
Let us say that two boxes Λ t k and Λ t ℓ are * -adjacent if k -ℓ ∞ = 1. For k ∈ Z d , say that the box Λ t k is good if any x ∈ Λ t k communicating with any y in Λ t k or in one of the 3 d -1 * -adjacent boxes is linked to y by an open path with length smaller than 4ρt. We also set

G = ∩ k 1 ≤1+3ρ * y 1/t {Λ t k is good.}.
Let us prove that (28)

L ∩ A ∩ B ∩ G ⊂ {D t (0 * , y * ) = D * (0, y)}.
Let us focus on the event L ∩ A ∩ B ∩ G. On the event L, the optimal path M t (0 * , y * ) = (0 * = y 0 , . . . , y n = y * ) stays inside Γ. This path is composed by three types of portions: sequences of red edges, sequences of edges in the infinite cluster and sequences of edges in finite clusters. To jump from a finite cluster to the infinite cluster, the path has to use a red edge. Set

i 0 = max{i : D(0 * , y i ) = D t (0 * , y i )}.
To prove (28), we just need to show that i 0 = n. Since D(0 * , y i0 ) = D t (0 * , y i0 ) ≤ D t (0 * , y * ) ≤ D * (0, y) < +∞, the point y i0 is in the infinite cluster. Assume by contradiction that i 0 < n: the edge between y i0 and y i0+1 is not open, otherwise the maximality of i 0 would be denied. It is thus an extra red edge, with length Kt, added between two points of a same mesoscopic box: therefore, D t (y i0 , y i0+1 ) = Kt. If y i0 and y i0+1 are in the same open cluster, since G occurs, D(y i0 , y i0+1 ) ≤ 4ρt ≤ Kt. But then D(y i0 , y i0+1 ) ≤ D t (y i0 , y i0+1 ), which would contradict once again the maximality of i 0 . Thus, y i0 and y i0+1 are not in the same open cluster, which means that y i0+1 is not in the infinite cluster. Let

j 0 = inf{j ∈ [i 0 + 1, . . . , n] : y j ∈ C ∞ }.
Since y n ∈ C ∞ , we know that j 0 < +∞. Between y i0 and y j0 , the path alternatively uses red edges and pieces of finite clusters. Look now at this microscopic path at the mesoscopic scale -i.e. consider the path of coordinates of mesocopic boxes successively visited. A site of the mesoscopic path is said to be red if the portion of the microscopic path crossing the corresponding mesoscopic box contains a red edge. Since event B prevents any finite cluster in Γ to link two non * -adjacent boxes, two consecutive red sites of the mesoscopic path can not be separated by more than one non-red site. Let us also remark that the edge linking y i0 (in the infinite cluster) and y i0+1 (in a finite cluster) has be be red. Thus at least half of the sites of the mesoscopic path are red. Consequently,

D(y i0 , y j0 ) ≥ D t (y i0 , y j0 ) ≥ y i0 -y j0 1 t × 1 2 × Kt = K 2 y i0 -y j0 1 .
If y i0 and y j0 are not in * -adjacent boxes, then y i0 -y j0 1 ≥ t and at the same time, D(y i0 , y j0 ) ≥ K 2 y i0 -y j0 1 > 2ρ y i0 -y j0 1 , which cannot occur on event A. Thus y i0 and y j0 are in * -adjacent boxes: the event G ensures then that D(y i0 , y j0 ) ≤ 4ρt ≤ Kt ≤ D t (y i0 , y j0 ), which contradicts once again the maximality of i 0 and ends the proof of (28).

Thus P(D * (0, y) = D t (0, y)) ≤ P(L c ) + P(A c ) + P(B c ) + P(G c ), and it now remains to bound each of these four probabilities.

To bound P(L c ), let us note that since K ≥ 1, any point in M t (0 * , y * ) is at a . 1 -distance less than D t (0 * , y * ) from 0 * . Since D t (0 * , y * ) ≤ D * (0, y), we have, using ( 9) and ( 12), With [START_REF] Efron | The jackknife estimate of variance[END_REF], P(B c ) = (1 + 3ρ * y 1 ) d A 8 exp(-B 8 t). Remember that ρ > 2β 10 /α 10 . Thus, if ℓ-k ∞ ≤ 1, x ∈ Λ t k and y ∈ Λ t ℓ , with (11), P(x ↔ y, D(x, y) > 4ρt) ≤ exp(-4α 10 ρt) exp(β 10 y -x 1 )

P(L c ) = P(M t (0 * , y * ) ⊂ Γ) ≤ P ( 0 -0 * 1 ≥ ρ * y 1 ) + P (D * (0, y) ≥ 2ρ * y 1 ) ≤ A 9 exp(-B 9 y 1 ) + A 12 exp(-2ρ * y 1 B 12 y 1 ), With (11)
≤ exp(-4(α 10 ρ -2β 10 )t).

Thus,

P(G c ) ≤ k 1 ≤1+3ρ * y 1/t P(Λ t k is not good) ≤ k 1 ≤1+3ρ * y 1/t x∈Λ t k ℓ-k ∞ ≤1 y∈Λ t ℓ P(x ↔ y, D(x, y) > 4ρt) ≤ (3 + 6ρ * y 1 /t) d (2t + 1) d 3 d (2t + 1) d exp(-4(α 10 ρ -2β 10 )t).
Since t ≤ y 1 , we get (26).

For the second point, note that

0 ≤ D * (0, y) -D t (0 * , y * ) ≤ ρ * y 1 1 1 {D * (0,y) =D t (0 * ,y * )} + (D * (0, y) -ρ * y 1 ) + .
Thus D * (0, y) -D t (0 * , y * ) 2 ≤ ρ * y 1 P(D * (0, y) = D t (0 * , y * )) + (D * (0, y) -ρ * y 1 ) + 2 , and we conclude with ( 26) and ( 14), using once again that y 1 ≥ t.

We can now move forward to the proof of ( 4) and ( 5) in Theorem 1.2. The idea is quite simple: we use the estimates obtained for D t in Lemma 3.1, and bound with Lemma 3.3 the approximation error between D * and D t .

Proof of ( 4). We can write, for y ∈ Z d , Var D * (0, y) ≤ 2(Var D t (0, y) + Var (D * (0, y) -D t (0, y))

≤ 2Var D t (0, y) + 4 E(D * (0, y) -D t (0 * , y * )) 2 + E(D t (0 * , y * ) -D t (0, y)) 2 .
We take t = d+1 B27 log(1 + y 1 ) ≤ y 1 as soon as y 1 is large enough. • With ( 14), we know that E[D * (0, y)] = O( y 1 ); using ( 18) and ( 21), we get:

Var D t (0, y) ≤ 3 d K 2 (tE[D * (0, y)] + t 2 ) = O( y 1 log(1 + y 1 )).
• Inequality (27) ensures that 1). • The triangle inequality for D t together with [START_REF] Pimentel | Asymptotics for first-passage times on Delaunay triangulations[END_REF] ensure that

E(D * (0, y) -D t (0 * , y * )) 2 ≤ A 2 27 (1 + y 1 ) 2d+2 exp(-2B 27 t) = O(
|D t (0 * , y * ) -D t (0, y)| ≤ D t (0, 0 * ) + D t (y, y * ) ≤ K( 0 * 1 + y -y * 1 + 2t
). Minkowski's inequality and (9) say then that D t (0 * , y * ) -D t (0, y) 2 = O(log(1 + y 1 )), which ends the proof of (4).

Proof of [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF]. Let us remark first that it is sufficient to prove (5) for y large enough. Let D 5 > 0. Choose γ given by Lemma 3.1 with C 15 = D 5 . We set

C 5 = max 1, 4d γB 26 , d + 1 γB 27 .
For every y ∈ Z d \{0}, if x ≤ D 5 y 1 and x ≥ C 5 (1 + log y 1 ), then, using ( 27) and [START_REF] Pimentel | Asymptotics for first-passage times on Delaunay triangulations[END_REF], 9), we know that E( 0 * 1 ) = E( y -y * 1 ) < +∞. Thus, since C 5 ≥ d+1 γB27 , for y large enough, if x ≤ D 5 y 1 and x ≥ C 5 (1 + log y 1 ), we have

|E[D * (0, y)] -E[D γx (0, y)]| ≤ |E[D * (0, y)] -E[D γx (0 * , y * )]| + |E[D γx (0 * , y * )] -E[D γx (0, y)]| ≤ D * (0, y) -D γx (0 * , y * ) 1 + E[D γx (0, 0 * )] + E[D γx (y, y * )] ≤ A 27 (1 + y 1 ) d+1 exp(-B 27 γC 5 (1 + log y 1 )) +KE( 0 * 1 ) + KE( y -y * 1 ) + 2Kγx. With (
|E[D * (0, y)] -E[D γx (0, y)]| y 1 ≤ x/2,
which leads to

P |D * (0, y) -E[D * (0, y)]| y 1 > x ≤ P(D * (0, y) = D γx (0 * , y * )) + P |D γx (0 * , y * ) -E[D γx (0, y)]| y 1 > x/2 .
Since x ≥ C 5 (1 + log y 1 ) and C 5 ≥ 4d B26γ , estimate (26) ensures that

P(D * (0, y) = D γx (0 * , y * )) ≤ A 26 (1 + y 1 ) 2d exp(-B 26 γx) ≤ A 26 2 2d exp - B 26 2 γx ,
For the second term, we write with ( 16):

|D γx (0 * , y * ) -E[D γx (0, y)]| ≤ |D γx (0, y) -E[D γx (0, y)]| + D γx (0, 0 * ) + D γx (y, y * ) ≤ |D γx (0, y) -E[D γx (0, y)]| + K 0 * 1 + K y -y * 1 + 2Kγx Then, for y large enough, P |D γx (0 * , y * ) -E[D γx (0, y)]| y 1 > x/2 ≤ P |D γx (0, y) -E[D γx (0, y)]| y 1 > x/9 + 2P 0 * 1 ≥
x y 1 9K .

Lemma 3.1 gives a bound of the correct order for the first term, while [START_REF] Garet | Asymptotic shape for the chemical distance and firstpassage percolation on the infinite Bernoulli cluster[END_REF] gives a bound of the correct order for the second term, which ends the proof.

Asymptotic behavior of the mean value

The aim of this section is to prove (6) in Theorem 1.2. The function D * inherits the subadditivity from D. Besides, we can note that for each a in Z d , the joint distribution of (D * (x + a, y + a)) x∈Z d ,y∈Z d does not depend on a. Thus, if we define h

(x) = E[D * (0, x)], we have ∀x, y ∈ Z d h(x + y) ≤ h(x) + h(y).
Since h is subadditive, we can use the technics developped by Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF] for the approximation of subadditive functions. First, we prove the convergence of h(ny)/n to µ(y): Lemma 4.1. For each y ∈ Z d , the sequence D * (0,ny) n converges almost surely and in L 1 to µ(y). Particularly, h(ny)/n converges to µ(y).

Proof. Since D * (0, y) is integrable and (D * (x, y)) x∈Z d ,y∈Z d is stationary, the subadditive ergodic theorem tells us that there exists µ * (y) such that D * (ny)/n converges almost surely and in L 1 to µ * (y). Thus, we just have to prove that µ * (y) coincides with µ(y). By Garet-Marchand [START_REF] Garet | Asymptotic shape for the chemical distance and firstpassage percolation on the infinite Bernoulli cluster[END_REF], on the event {0 ↔ ∞}, we can almost surely find a sequence (n k y) k≥1 with 0 ↔ n k y and D(0, n k y)/n k tends to µ(y) when k goes to infinity. Obviously, D * (0, n k y)/n k converges to µ * (y). Since the equality D(0, n k y) = D * (0, n k y) holds on {0 ↔ ∞}, we get that µ(y) = µ * (y).

We recall the results of Alexander on the approximation of subadditive functions. Let us introduce some notation derived from Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF]. For some positive constants M and C, we define

GAP (M, C) = h : Z d → R, ( x 1 ≥ M ) ⇒ µ(x) ≤ h(x) ≤ µ(x) + C x 1/2 1 log x 1 .
For x ∈ R d , we choose a linear form µ x on R d such that µ x (x) = µ(x) and such that ∀y ∈ B 0 µ (µ(x)) µ x (y) ≤ µ(x). The quantity µ x (y) is the µ-length of the projection of y onto the line from 0 to x, following a hyperplane tangent to the convex set B 0 µ (µ(x)) at x. It is easy to see that for each y ∈ R d , |µ x (y)| ≤ µ(y). Then, for each positive constant C, we define

Q h x (C) = y ∈ Z d : y 1 ≤ (2d + 1) x 1 , µ x (y) ≤ µ(x), h(y) ≤ µ x (y) + C x 1/2 1 log x 1 .
The idea is that the elements of Q h

x (C) permit to realize a mesh of Z d with increments for which µ x correctly approaches h. We also define, for M > 0, C > 0, a > 1,

CHAP (M, C, a) = h : Z d → R, ( x 1 ≥ M ) ⇒ ∃α ∈ [1, a], x/α ∈ Co(Q h x (C))
, where Co(A) is the convex hull of A in R d . Alexander has the following results:

Lemma 4.2 (Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF]). Let h be a nonnegative subadditive function on Z d , M > 1, C > 0, a > 1 some fixed constants. We assume that for each x ∈ Z d with x 1 ≥ M , there exist a natural number n, a lattice path γ from 0 to nx, and a sequence of points 0 = v 0 , v 1 , . . . , v m = nx in γ such that m ≤ an and whose increments v i -v i-1 belong to Q h x (C). Then h ∈ CHAP (M, C, a) Theorem 4.3 (Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF]). Let h be a nonnegative subadditive function on Z d and M > 1, C > 0, a > 1 some fixed constants. If h ∈ CHAP (M, C, a), then h ∈ GAP (M, C). Definition 4.4. We call Q h x (C)-path every sequence (v 0 , . . . , v m ) such that for each i ∈ {0, . . . , m -1}, v i+1 -v i ∈ Q h x (C). Let γ = (γ(0), . . . , γ(n)) be a simple lattice path in Z d . We consider the unique sequence of indices (u i ) 0≤i≤m such that

u 0 = 0, u m = n, ∀i ∈ {0, . . . , m -1} ∀j ∈ {u i + 1, . . . , u i+1 } γ(j) -γ(u i ) ∈ Q h x (C), ∀i ∈ {0, . . . , m -1} γ(u i+1 + 1) -γ(u i ) ∈ Q h x (C). Then, the Q h x (C)-skeleton of γ is the sequence (γ(u i ))
0≤i≤m . We will prove the following result relative to the modified chemical distance h(.) = E[D * (0, .)]: Proposition 4.5. There exist some constants M > 1 and C > 0 such that if x 1 ≥ M , then for sufficiently large n there exists a lattice path from 0 to nx with a Q h x (C)-skeleton of 2n + 1 or fewer vertices.

Let us first see how this proposition leads to [START_REF] Chayes | The correlation length for the high-density phase of Bernoulli percolation[END_REF] and concludes the proof of Theorem 1.2.

We denote by D(v 1 , v m ; (v i )) the length of the shortest open path from v 1 to v m that visits v 1 , . . . , v m in this order. Then, Lemma 4.7.

lim x 1→+∞ P    ∃m ≥ 1 ∃ a Q x -path (v 0 = 0, . . . , v m ) : m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) > Cm x 1/2 1 log x 1    = 0.
The proof of this lemma relies on a denumeration of the Q x -paths, on a bound on exponential moments for Proof. Let us fix m ≥ 1 and x large enough. Let (v 0 = 0, v 1 , . . . , v m ) be a Q x -path starting from 0. Lemma 4.6 implies that for each i, v i+1 -v i 1 ≤ 2d x 1 . We define

E[D * (v i , v i+1 )] -D(v i , v i+1
Y i = E[D * (v i , v i+1 )] -D * (v i , v i+1 ) Z i = E[D * (v i , v i+1 )] -D(v i , v i+1 ).
The moderate deviation result allows first to bound some exponential moments of Y i for large x. Indeed, we can write

E exp β(Y i ) + 2d x 1 = 1 + +∞ 0 βe βt P Y i ≥ t 2d x 1 dt.
Let us note that ( 14) already gives the simple bound:

max(Y i , Z i ) ≤ E[D * (v i , v i+1 )] ≤ A 14 + ρ * v i+1 -v i 1 ;
remarking that v i+1 -v i 1 ≥ 1, this particularly implies, for x 1 large enough, that

(30) max(Y i , Z i ) 2d x 1 ≤ 2ρ * v i+1 -v i 1 .
This ensures that P(Y i ≥ t 2d x 1 ) = 0 as soon as t > 2ρ * v i+1 -v i 1 . On the other hand, the moderate deviation result (5) ensures the existence of constants

A 5 , B 5 > 0 such that if C 5 (1 + log v i+1 -v i 1 ) ≤ t ≤ 2ρ * v i+1 -v i 1 , then, since v i+1 -v i 1 ≤ 2d x 1 , P(Y i ≥ t 2d x 1 ) ≤ P(Y i ≥ t v i+1 -v i 1/2 1 ) ≤ A 5 exp(-B 5 t). Thus, since β < B 5 , we get E exp β(Y i ) + 2d x 1 ≤ 1 + C5(1+log(2d x 1)) 0 βe βt dt + +∞ 0 βe βt A 5 e -B5t dt ≤ 1 + (2de) βC5 x βC5 1 + A 5 β B 5 -β . (31)
Let us note that the bound for the exponential moments of Y i is not as good as in first-passage percolation, where it does not depend on x 1 (see Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF]): this is due to the renormalization used to get the moderate deviations [START_REF] Boucheron | Concentration inequalities using the entropy method[END_REF].

We can remark that

• if v i ↔ v i+1 , then (Z i ) + = 0; • if v i ↔ v i+1 and v i ↔ ∞, then (Z i ) + = (Y i ) + ;
Then, using (30),

exp β(Z i ) + 2d x 1 ≤ 1 + exp β(Y i ) + 2d x 1 + 1 1 n vi↔vi+1 vi ↔∞ o exp 2βρ * v i+1 -v i 1 .
Using ( 8) then (31), we get, for x large enough:

E exp β(Z i ) + 2d x 1 (32) ≤ 1 + E exp β(Y i ) + 2d x 1 + exp 2βρ * v i+1 -v i 1 P v i ↔ v i+1 v i ↔ ∞ ≤ 1 + E exp β(Y i ) + 2d x 1 + A 8 exp 2βρ * v i+1 -v i 1 -B 8 v i+1 -v i 1 ≤ (6d x 1 ) βC5 .
We can apply a BK-like inequality to D(v 1 , v m ; (v i )): by Theorem 2.3 in Alexander [START_REF] Alexander | A note on some rates of convergence in first-passage percolation[END_REF], for each t > 0, if the Z ′ i 's are independent copies of the Z i 's, then, with (32),

P m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) > Cm x 1/2 1 log x 1 ≤ P m-1 i=1 Z ′ i > Cm x 1/2 1 log x 1 ≤ exp - βCm log x 1 √ 2d m-1 i=1 E exp βZ i 2d x 1 ≤ (6d) βC5 x -βC √ 2d +βC5 1 m .
From Lemma 4.6, there exists a constant K such that there are at most (K x d ) m Q x -pathss of m + 1 points starting from 0. Then, summing on these paths, we get

P    ∃ a Q x -path (v 0 = 0, . . . , v m ) : m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) > Cm x 1/2 1 log x 1    ≤ K(6d) βC5 x d-βC √ 2d +βC5 1 m = L x α 1 m ,
where L and α are some constants; the choice (29) we did for β and C ensures that α > 0. Thus, for x large enough, L x -α 1 ≤ 1 2 , so summing over all possible lengths m:

P    ∃m ≥ 1 ∃ a Q x -path (v 0 , . . . , v m ) : m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) > Cm x 1/2 1 log x 1    ≤ 2L x α 1 ,
which completes the proof of the lemma.

Proof of Proposition 4.5. This proposition corresponds to Proposition 3.4. in Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF].

The proof of this deterministic result uses the so-called "probabilistic method": we are going to prove that with positive probability, we can construct such a Q xpath from a path realizing D * (0, nx). With Lemma 4.7 and (9), we can find M > 1 such that if x 1 ≥ M , then

P    ∃m ≥ 1 ∃ a Q x -path (v 0 = 0, . . . , v m ) : m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) > Cm x 1/2 1 log x 1    ≤ 1 5 , et P 0 * ≥ x 1/2 1 ≤ 1 5 .
Should we take a greater M , we can also assume that if Then, we can find ω fulfilling these properties, and work from now on with this particular realization. Let v 1 = 0 * , . . . , v m = (nx) * be the Q x -skeleton of some path γ realizing the chemical distance from 0 * to (nx) * . Define v 0 = 0 and v m+1 = nx: properties c) and d) ensure that we get a Q x -path from 0 to nx. We will prove that m + 2 ≤ 2n + 1, which will conclude the proof of the proposition. Note that, by construction,

y 1 ≤ x 1/2 1 and x 1 ≥ M , then y ∈ Q x . Now fix x ∈ Z d with x 1 ≥ M .
D(v 1 , v m ; (v i )) = D * (0, nx).
From a), our Q x -path satisfies, for this particular ω,

(33) m-1 i=1 E[D * (v i , v i+1 )] -D(v 1 , v m ; (v i )) ≤ Cm x 1/2 1 log x 1 .
Besides, using the definition of Q x , property d), the fact that µ is a norm and ( 11 We now distinguish in the Q x -skeleton the short increments and the long ones:

S((v i )) = {i : 1 ≤ i ≤ m -1, v i+1 -v i ∈ ∆ x }, L((v i )) = {i : 1 ≤ i ≤ m -1, v i+1 -v i ∈ D x }.
By the definition of a Q x -skeleton, these two sets partition {1, . . . , m -1}. Let us first bound the number of short increments with Lemma 4.6, estimate (2): recall that µ x (y) ≤ µ(y) ≤ E[D * (0, y)], so

m-1 i=1 E[D * (v i , v i+1 )] = m-1 i=1 [µ x (v i+1 -v i ) + (ED * (v i , v i+1 ) -µ x (v i+1 -v i ))] ≥ µ x ((nx) * ) -µ x (0 * ) + |S((v i ))| C ′ 2 x 1/2 1 log x 1 ≥ nµ(x) -2ρ x 1/2 1 + |S((v i ))| C ′ 2 x 1/2 1 log x 1 .
Thus, summing the two estimates and enlarging M if necessary, we get

|S((v i ))| C ′ 2 x 1/2 1 log x 1 ≤ 2ρ x 1/2 1 + 2Cm x 1/2 1 log x 1 ≤ 3Cm x 1/2 1 log x 1 , hence |S((v i ))| ≤ 6 C C ′ m = m 8 .
Similarly, we bound the number of long increments with Lemma 4.6, estimate (3):

m-1 i=1 E[D * (v i , v i+1 )] = m-1 i=1 [µ x (v i+1 -v i ) + (E[D * (v i , v i+1 )] -µ x (v i+1 -v i ))]
≥ nµ(x) -2ρ x We would like to thank Raphaël Rossignol and Marie Théret for kindly giving us the extension of Boucheron, Lugosi and Massart's result.

  , P(A c ) = a,b∈Γ: a-b 1 ≥t P(D(a, b) ≥ 2ρ a -b 1 ) = a,b∈Γ: a-b 1 ≥t A 11 exp(-2B 11 ρ a -b 1 ) = (1 + 2ρ 2 y 1 ) 2d exp(-2B 11 ρt).

  ) and on a BK-like inequality. Of course, it would be more natural to deal with quantities likeE[D * (v i , v i+1 )] -D * (v i , v i+1). But D * lacks the monotonicity property of D needed to use this kind of tools. Once more, we have to deal alternatively with D and D * .

5 . 2 1 log x 1 ,

 521 Lemma 4.1 ensures that there exists n 0 ∈ Z + such that ∀n ≥ n 0 P(D * (0, nx) > n(µ(x) + 1)) ≤ 1Let n ≥ n 0 . With probability at least 1/5, the following properties hold:a) for each m ≥ 1, for each Q x -path (v 0 = 0, . . . , v m ), * (v i , v i+1 )] -D(v 1 , v m ; (v i )) ≤ Cm x 1/b) D * (0, nx) ≤ n(µ(x)

/2 1 . 2 1 log x 1 ≤ 2 1 log x 1 ≤ 2 1

 121212 v i+1 -v i ) = µ x ((nx) * ) = µ x ((nx)) + µ x ((nx) * -nx) ≥ nµ(x) -µ((nx) * -nx) ≥ nµ(x) -ρ x 1Thus, should we take a larger M , we get n ≤11 10 m. Now, with b) and taking once more a larger M if necessary,m-1 i=1 E[D * (v i , v i+1 )] ≤ D * (0, nx) + Cm x 1/n(µ(x) + 1) + Cm x 1/nµ(x) + 2Cm x 1/log x 1 .

8 .

 8 Finally, m = |S((v i ))| + |L((v i ))|+ ≤ 65 n + m/4, so m ≤ 8 5 n, which concludes the proof.

  2N d c (|C 0 |+1) and denotes the stochastic domination. Thus, we can choose α 10 = h c 2N d and β 10 = log E[exp(h|C 0 | + 1)].Proof. Let y ∈ Z d and t > 0. With the Markov inequality and (10), we get

	Corollary 2.2. There exist some constants ρ, A 11 , B 11 > 0 such that
	(11)	∀y ∈ Z d ∀t ≥ ρ y 1 P(0 ↔ y, D(0, y) > t) ≤ A 11 exp(-B 11 t).

  ).

	Now, for y ∈ Z d \{0}, it follows from (12) that
	E[e αD * (0,y) ] = 1 +	+∞	P(D * (0, y) > t)αe αt dt
	0
	≤ e αρ * y 1 +	ρ * y 1 +∞	A 12 exp(-B 12 t)αe αt dt,
	which gives (13), taking for instance α 13 = B 12 /2. Similarly, using (12) again,
		+∞
	E([(D * (0, y) -ρ * y 1 ) + ] 2 ) =	0		P(D * (0, y) -ρ * y 1 > t)2t dt
				+∞
	≤ A 12 exp(-B 12 y 1 )	0	2t exp(-B 12 t) dt,
	which gives (14).
	2.4. Proof of theorem 1.1. Let us see how Theorem 1.1 follows from Theo-
	rem 1.2. The estimate (

Proof of [START_REF] Chayes | The correlation length for the high-density phase of Bernoulli percolation[END_REF]. Proposition 4.5 and Lemma 4.2 ensure that h(.) = E[D * (0, .)] is in CHAP (M, C, 2), which implies, thanks to Theorem 4.3, that h is in GAP (M, C). This gives [START_REF] Chayes | The correlation length for the high-density phase of Bernoulli percolation[END_REF] for each y ∈ Z d such that y 1 ≥ M , hence for each y ∈ Z d , should we increase C 6 .

Let us go to the proof of Proposition 4.5. We now choose h(.) = E[D * (0, .)], take β and C such that

We define

Proof. The arguments are simple and essentially deterministic. One can refer to Lemma 3.3 in Alexander [START_REF] Alexander | Approximation of subadditive functions and convergence rates in limiting-shape results[END_REF], which is the analogous result in first-passage percolation. Particularly, we use the fact that E[D * (0, ±e i )] ≤ ρ * + A 14 < +∞, which plays the same role as the integrability of passage times does in first-passage percolation.


François Garillot
email: francois.garillot@inria.fr

Georges Gonthier
email: gonthier@microsoft.com

Assia Mahboubi
email: assia.mahboubi@inria.fr

Laurence Rideau
email: laurence.rideau@inria.fr

Packaging mathematical structures

Keywords: Formalization of Algebra, Coercive subtyping, Type inference, Coq, SSReflect

This paper proposes generic design patterns to define and combine algebraic structures, using dependent records, coercions and type inference, inside the Coq system. This alternative to telescopes in particular supports multiple inheritance, maximal sharing of notations and theories, and automated structure inference. Our methodology is robust enough to handle a hierarchy comprising a broad variety of algebraic structures, from types with a choice operator to algebraically closed fields. Interfaces for the structures enjoy the convenience of a classical setting, without requiring any axiom. Finally, we present two applications of our proof techniques: a key lemma for characterising the discrete logarithm, and a matrix decomposition problem.

Introduction

Large developments of formalized mathematics demand a careful organization. Fortunately mathematical theories are quite organized, e.g., every algebra textbook [START_REF] Lang | Algebra[END_REF] describes a hierarchy of structures, from monoids and groups to rings and fields. There is a substantial literature [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF][START_REF] Betarte | Formalisation of systems of algebras using dependent record types and subtyping: An example[END_REF][START_REF] Pottier | User contributions in Coq[END_REF][START_REF] Geuvers | A constructive algebraic hierarchy in Coq[END_REF][START_REF] Haftmann | Local theory specifications in Isabelle/Isar[END_REF][START_REF] Rudnicki | Commutative algebra in the Mizar system[END_REF] devoted to their formalization within formal proof systems.

In spite of this body of prior work, however, we have found it difficult to make practical use of the algebraic hierarchy in our project to formalize the Feit-Thompson Theorem in the Coq system; this paper describes some of the problems we have faced and how they were resolved. The proof of the Feit-Thompson Theorem covers a broad range of mathematical theories, and organizing this formalization into modules is central to our research agenda. We've developed [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF] an extensive set of modules for the combinatorics and set and group theory required for the "local analysis" part of the proof, which includes a rudimentary algebraic hierarchy needed to support combinatorial summations [START_REF] Bertot | Canonical big operators[END_REF].

Extending this hierarchy to accommodate the linear algebra, Galois theory and representation theory needed for the "character theoretic" part of the proof has proved problematic. Specifically, we have found that well-known encodings of algebraic structures using dependent types and records [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF] break down in the face of complexity; we address this issue in section 2 of this paper.

Many of the cited works focused on the definition of the hierarchy rather than its use, making simplifying assumptions that would have masked the problems we encountered. For example some assume that only one or two structures are involved at any time, or that all structures are explicitly specified. The examples in section 4 show that such assumptions are impractical: they involve several different structures, often within the same expression, and some of which need to be synthesized for existing types.

We have come to realize that algebraic structures are not "modules" in the software engineering sense, but rather "interfaces". Indeed, the mathematical theory of, say, an abstract ring, is fairly thin. However, abstract rings provide an interface that allows "modules" with actual contents, such as polynomials and matrices, to be defined and, crucially, composed. The main function of an algebraic structure is to provide common notation for expressions and for proofs (e.g., basic lemmas) to facilitate the composition and application of these generic modules. Insisting that an interface be instantiated explicitly each time it is used negates this function, so it is critical that structures be inferred on the fly; we'll see in the next section how this can be accomplished.

Similarly, we must ensure that our algebraic interfaces are consistent with the other modules in our development: in particular they should integrate the existing combinatoric interfaces [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF], as algebra requires equality. As described in section 3, we have therefore adapted classical algebra to our constructive combinatorics. In addition to philosophical motivations (viz., allowing constructive proof of a finitary result like the Feit-Thompson Theorem), we have practical uses for a constructive framework: it provides basic but quite useful proof automation, via the small-scale reflection methodology supported by the SSReflect extension to Coq [START_REF] Gonthier | A small scale reflection extension for the Coq system[END_REF].

Due to space constraints, we will assume some familiarity with the Coq type system [START_REF] Paulin-Mohring | Définitions Inductives en Théorie des Types d'Ordre Supérieur[END_REF] (dependent types and records, proof types, type inference with implicit terms and higher-order resolution) in section 2, and with the basic design choices in the Feit-Thompson Theorem development [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF] (boolean reflection, concrete finite sets) in sections 3 and 4.

Encoding structures

Mixins

An algebraic or combinatorial structure comprises representation types (usually only one), constants and operations on the type(s), and axioms satisfied by the operations. Within the propositions-as-types framework of Coq, the interface for all of these components can be uniformly described by a collection of dependent types: the type of operations depends on the representation type, and the statement (also a "type") of axioms depends on both the representation type and the actual operations.

For example, a path in a combinatorial graph amounts to a representation type T for nodes an edge relation e : rel T an initial node x 0 : T the sequence p : seq T of nodes that follow x 0 the axiom p P : path e x 0 p asserting that e holds pairwise along x 0 :: p.

The path "structure" is actually best left unbundled, with each component being passed as a separate argument to definitions and theorems, as there is no one-toone relation between any of the components (there can be multiple paths with the same starting point and relation, and conversely a given sequence can be a path for different relations). Because it depends on all the other components, only the axiom p P needs to be passed around explicitly; type inference can figure out T , e, x 0 and p from the type of p P , so that in practice the entire path "structure" can be assimilated to p P . While this unbundling allows for maximal flexibility, it also induces a proliferation of arguments that is rapidly overwhelming. A typical algebraic structure, such as a ring, involves half a dozen constants and even more axioms. Moreover such structures are often nested, e.g., for the Cayley-Hamilton theorem one needs to consider the ring of polynomials over the ring of matrices over a general commutative ring. The size of the terms involved grows as C n , where C is the number of separate components of a structure, and n is the structure nesting depth. For Cayley-Hamilton we would have C = 15 and n = 3, and thus terms large enough to make theorem proving impractical, given that algorithms in user-level tactics are more often than not nonlinear.

Thus, at the very least, related operations and axioms should be packed using Coq's dependent records (Σ-types); we call such records mixins. Here is, for example, the mixin for a Z-module, i.e., the additive group of a vector space or a ring: Here we are using a Coq Module solely to avoid name clashes with similar mixin definitions.

Note that mixins typically provide only part of a structure; for instance a ring structure would actually comprise a representation type and three mixins: one for equality, one for the additive group, and one for the multiplicative monoid together with distributivity. A mixin can depend on another one: e.g., the ring multiplicative mixin depends on the additive one for its distributivity axioms.

Since types don't depend on mixins (it's the converse) type inference usually cannot fill in omitted mixin parameters; however, the type class mechanism of Coq 8.2 [START_REF] Sozeau | First-Class Type Classes[END_REF] can do so by running ad hoc tactics after type inference.

Packed structures

The geometric dependency of C n on n is rather treacherous: it is quite possible to develop an extensive structure package in an abstract setting (when n = 1) that will fail dramatically when used in practice for even moderate values of n. The only case when this does not occur is with C = 1 -when each structure is encapsulated into a single object. Thus, in addition to aesthetics, there is a strong pragmatic rationale for achieving full encapsulation.

While mixins provide some degree of packaging, it falls short of C = 1.

However, mixins require one object per level in the structure hierarchy. This is far from C = 1 because theorem proving requires deeper structure hierarchies than programming, as structures with identical operations can differ by axioms; indeed, despite our best efforts, our algebraic hierarchy is nine levels deep.

For the topmost structure in the hierarchy, encapsulation just amounts to using a dependent record to package a mixin with its representation type. For example, the top structure in our hierarchy, which describes a type with an equality comparison operation (see [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF]), could be defined as follows:

Module Equality. Record mixin _ of (T : Type) : Type := Mixin {op : rel T; _ : forall x y, reflect (x = y) (op x y)}. Structure type : Type := Pack {sort :> Type; mixin : mixin _ of sort}. End Equality. Notation eqType := Equality.type. Notation EqType := Equality.Pack. Definition eq _ op T := Equality.op (Equality.mixin T). Notation "x == y" := (@eq _ op _ x y).

Coq provides two features that support this style of interface, Coercion and Canonical Structure. The sort :> Type declaration above makes the sort projection into a coercion from type to Type. This form of explicit subtyping allows any T : eqType to be used as a Type, e.g., the declaration x : T is understood as x : sort T . This allows x == x to be understood as @eq _ op T x x by simple first-order unification in the Hindley-Milner type inference, as @eq _ op α expects arguments of type sort α.

Coercions are mostly useful for establishing generic theorems for abstract structures. A different mechanism is needed to work with specific structures and types, such as integers, permutations, polynomials, or matrices, as this calls for construing a more specific Type as a structure object (e.g., an eqType): coercions and more generally subtyping will not do, as they are constrained to work in the opposite direction.

Coq solves this problem by using higher-order unification in combination with Canonical Structure hints. For example, assuming int is the type of signed integers, and given Definition int _ eqMixin := @Equality.Mixin int eqz ... Canonical Structure int _ eqType := EqType int _ eqMixin.

Coq will interpret 2 == 2 as @eq _ op int _ eqType 2 2, which is convertible to eqz 2 2. Thanks to the Canonical Structure hint, Coq finds the solution α = int _ eqType to the higher-order unification problem sort α ≡ βιδ int that arises during type inference.

Telescopes

The simplest way of packing deeper structures of a hierarchy consists in repeating the design pattern above, substituting "the parent structure" for "representation type". For instance, we could end Module Zmodule with Structure zmodType : Type := Pack {sort :> eqType; _ : mixin _ of sort}.

This makes zmodType a subtype of eqType and (transitively) of Type, and allows for the declaration of generic operator syntax (0, x + y, -x, x -y, x * i), and the declaration of canonical structures such as Canonical Structure int _ zmodType := Zmodule.Pack int _ zmodMixin.

Many authors [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF][START_REF] Pollack | Dependently typed records in type theory[END_REF][START_REF] Rudnicki | Commutative algebra in the Mizar system[END_REF][START_REF] Geuvers | A constructive algebraic hierarchy in Coq[END_REF] have formalized an algebraic hierarchy using such nested packed structures, which are sometimes referred to as telescopes [START_REF] Bruijn | Telescopic mappings in typed lambda calculus[END_REF], the term we shall use henceforth.

As the coercion of a telescope to a representation Type is obtained by transitivity, it comprises a chain of elementary coercions: given T : zmodType, the declaration x : T is understood as x : Equality.sort(Zmodule.sort T ). It is this explicit chain that drives the resolution of higher-order unification problems and allows structure inference for specific types. For example, the implicit α : zmodType in the term 2 + 2 is resolved as follows: first Hindley-Milner type inference generates the constraint Equality.sort(Zmodule.sort α) ≡ βιδ int. Coq then looks up the Canonical Structure int _ eqType declaration associated with the pair (Equality.sort, int), reduces the constraint to Zmodule.sort α ≡ βιδ int _ eqType which it solves using the Canonical Structure int _ zmodType declaration associated with the pair (Zmodule.sort, int _ eqType). Note that int _ eqType is an eqType, not a Type: canonical projection values are not restricted to types.

Although this clever double use of coercion chains makes telescopes the simplest way of packing structure hierarchies, it raises several theoretical and practical issues for deep or complex hierarchies.

Perhaps the most obvious one is that telescopes are restricted to single inheritance. While multiple inheritance is rare, it does occur in classical algebra, e.g., rings can be unitary and/or commutative. It is however possible to fake multiple inheritance by extending one base structure with the mixin of a second one (similarly to what we do in Section 3.2), provided this mixin was not inlined in the definition of the second base structure.

A more serious limitation is that the head constant of the representation type of any structure in the hierarchy is always equal to the head of the coercion chain, i.e., the Type projection of the topmost structure (Equality.sort here). This is a problem because for both efficiency and robustness, coercions and canonical projections for a type are determined by its head constant, and the topmost projection says very little about the properties of the type (e.g., only that it has equality, not that it is a ring or field).

There is also a severe efficiency issue: the complexity of Coq's term comparison algorithm is exponential in the length of the coercion chain. While this is clearly a problem specific to the current Coq implementation, it is hard and unlikely to be resolved soon, so it seems prudent to seek a design that does not run into it.

Packed Classes

We now describe a design that achieves full encapsulation of structures, like telescopes, but without the troublesome coercion chains. The key idea is to introduce an intermediate record that bundles all the mixins of a structure, but not the representation type; the latter is packed in a second stage, similarly to the top structure of a telescope. We call this intermediate record a class, by analogy with open-recursion models of objects, and Haskell type classes; hence in our design structures are represented by packed classes. The definitions of the class _ of and type records are straightforward; unpack is a general dependent destructor for cT : type whose type is expressed in terms of sort cT and class cT. Almost all of the code is fixed by the design pattern 5 ; indeed the definitions of type and unpack are literally identical for all packed classes, while usually only the name of the parent class module (here, Equality) changes in the definitions of class _ of and pack.

Indeed, the code assumes that Module Equality is similarly defined. Because Equality is a top structure, the definitions of class _ of and pack in Equality reduce to Notation class _ of := mixin _ of. Definition pack T c := @Pack T c T.

While Pack is the primitive constructor for type, the usual constructor is pack, whose only explicit argument is a Z-module mixin: it uses Equality.unpack to break the packed eqType supplied by type inference into a type and class, which it combines with the mixin to create the packed zmodType class. Note that pack ensures that the canonical Type projections of the eqType and zmodType structure are exactly equal.

The inconspicuous Canonical Structure Zmodule.eqType declaration is the keystone of the packed class design, because it allows Coq's higher order unification to unify Equality.sort and Zmodule.sort. Note that, crucially, int _ eqType and Zmodule.eqType int _ zmodType and are convertible; this holds in general because Zmodule.eqType merely rearranges pieces of a zmodType. For a deeper structure, we will need to define one such conversion for each parent of the structure. This is hardly inconvenient since each definition is one line, and the convertibility property holds for any composition of such conversions.

Description of the hierarchy

Figure 3 gives an account for the organization of the main structures defined in our libraries. Starred blocks denote algebraic structures that would collapse on an unstarred one in either a classical or an untyped setting. The interface for each structure supplies notation, definitions, basic theory, and generic connections with other structures (like a field being a ring).

In the following, we comment on the main design choices governing the definition of interfaces. For more details, the complete description of all the structures and their related theory, see module ssralg on http://coqfinitgroup.gforge. inria.fr/.

We do not package as interfaces all the possible combinations of the mixins we define: a structure is only packaged when it will be populated in practice. For instance integral domains and fields are defined on top of commutative rings as in standard textbooks [START_REF] Lang | Algebra[END_REF], and we do not develop a theory for non commutative algebra, which hardly shares results with its commutative counterpart.

Combinatorial structures

SubType structures To handle mathematical objects like "the units of Z/nZ", one needs to define new types in comprehension-style, by giving a specification over an existing type. The Coq system already provides a way to build such new types, by the means of Σ-types (dependent pairs). Unfortunately, in general, to compare two inhabitants of such a Σ-type, one needs to compare both components of the pairs, i.e. comparing the elements and comparing the related proofs.

To take advantage of the proof-irrelevance on boolean predicates when defining these new types, we use the following subType structure: This interface gathers a new type sub _ sort for the inhabitants of type T satisfying the boolean predicate P, with a projection val on type T, a Sub constructor, and an elimination scheme. Now, the val projection can be proved injective: to compare two elements of a subType structure on type T it is enough to compare their projections on T. A simple example of subType structure equips the type of finite ordinals:

Inductive ordinal (n : nat) := Ordinal m of m < n.

where < stands for the boolean strict order on natural numbers. Crucially, replacing a primitive Coq Σ-type by this encoding makes it possible to coerce ordinal to nat. Moreover, in Coq, the definition of this inductive type automatically generates the ord _ rect associated elimination scheme. We can hence easily build a (canonical) structure of subType on top of ordinal, by providing ord _ rect to the SubType constructor, as the other arguments are trivial.

Types with a choice function Our intentional, proof-irrelevant representation of finite sets was sufficient to address quotients of finite objects like finite groups [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF]. However, this method does not apply to an infinite setting, where arguments like the incomplete basis theorem are pervasive. The construction of quotients and its practice inside type theory based proofs assistants has been quite intensively studied. In classical systems like HOL, the infrastructure needed to work with quotient types is now well understood [START_REF] Paulson | Defining Functions on Equivalence Classes[END_REF].

Coq provides support for Setoids [START_REF] Barthe | Setoids in type theory[END_REF], which is a way to define quotients by explicitly handling the involved equivalence relation, and the proved substitutive contexts. In our case, quotients have to be dependent types, the dependent parameters often being themselves (dependent) quotients. This combination of dependent types with setoids, which has proved successful in an extensional setting like NuPRL [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF], is not adapted to an intentional theory like the one of Coq. Crafting and implementing a Curry-Howard based system featuring the appropriate balance between intentional and extensional type theories, as well as an internalized quotient construction is still work in progress [START_REF] Altenkirch | Observational equality, now! In: Proceedings of the PLPV'07 workshop[END_REF].

To circumvent this limitation, we combine the structure of types with equality with a choice operator on decidable predicates in a Choice structure. This structure, at the top of the hierarchy, is embedded in every lower level algebraic structure.

To construct objects like linear bases, we need to choose sequences of elements. Yet a choice operator on a given type does not canonically supply a choice operator on sequences of elements of this type. This would indeed require a canonical encoding of (seq T) into T which is in general not possible: for the empty void type, (seq void) has a single inhabitant, while (seq (seq void)) is isomorphic to nat. The solution is to require a choice operator on (seq (seq T)). This leads to a canonical structure of choice for T and any (seq .. (seq T)), using a Gödel-style encoding.

Thus we arrive at the following definition for the Choice mixin and class: The xfun choice operator for boolean predicates should return a witness satisfying P, given a proof of the existence of such a witness. It is extensional with respect to both the proofs of existence and the predicates.

Countable structures A choice structure will still not be transmitted to any desired construction (like product) over types featuring themselves a choice structure. Types with countably many inhabitants on the other side are more amenable to transmit their countability. This leads us to define a structure for these countable types, by requiring an injection pickle : T -> nat on the underlying type T.

Since the Calculus of Inductive Constructions [START_REF] Paulin-Mohring | Définitions Inductives en Théorie des Types d'Ordre Supérieur[END_REF] validates the axiom of countable choice, it is possible to derive a Choice structure from any countable type. However since a generic choice construction on arbitrary countable types would not always lead to the expected choice operator, we prefer to embed a Choice structure as base class for the Countable structure.

Finite types structures

The structure of types with a finite number of inhabitants is at the heart of our formalization of finite quotients [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF]. The Finite mixin still corresponds to the description given in this reference, but the FinType structure now packs this mixin with a Countable base instead of an eqType. Proofs like the cardinal of the cartesian product of finite types make the most of this computational content for the enumeration. Indeed the use of (computations of) list iterators shrinks the sizes of such proofs by a factor of five compared to the abstract case.

Advanced algebraic structures

Commutative rings, rings with units, commutative rings with units We package two different structures for both commutative and plain rings, as well as rings enjoying a decidable discrimination of their units. The latter structure is for instance the minimum required on a ring for a polynomial to bound the number of roots of a polynomial on that ring by the number of its roots (see lemma max _ ring _ poly _ roots in module poly). For the ring Z/nZ, this unit predicate selects coprimes to n. For matrices, it selects those having a non-zero determinant. Its semantic and computational content can prove very efficient when developing proofs.

Yet we also want to package a structure combining the ComRing structure of commutative ring and the UnitRing deciding units, equipping for instance Z/nZ. This ComUnitRing structure has no mixin of its own: Its class packages the class of a ComRing structure with the mixin of a UnitRing (which reflects a natural order for further instantiation). The base1 projection coerces the ComUnitRing class to its ComRing base class. Note that this definition does not provide the required coercion path from a ComUnitRing class to its underlying UnitRing class, which is only provided by base2. Now the canonical structures of ComRing and UnitRing for a ComUnitRing structure will let the latter enjoy both theories with a correct treatment of type constraints.

Decidable fields

The DecidableField structure models fields with a decidable first order theory. One motivation for defining such a structure is our need for the decidability of the irreductibility of representation of finite groups, which is a valid but highly non trivial [START_REF] Olteanu | Computing the Wedderburn decomposition of group algebras by the Brauer-Witt theorem[END_REF] property, pervasive in representation theory.

For this purpose, we define a reflected representation of first order formulas. The structure requires the decidability of satisfiability of atoms and their negation. Proving quantifier elimination leads to the decidability for the full first-order theory.

Closed fields Algebraically closed fields are defined by requiring that any non constant monic polynomial has a root. Since such a structure enjoys quantifier elimination, any closed field canonically enjoys a structure of decidable field.

Population of the hierarchy

The objective of this section is to give a hint of how well we meet the challenge presented in section 1: defining a concrete datatype and extending it externally with several algebraic structures that can be used in reasoning on this type. We aim at showing that this method works smoothly by going through the proofs of easy lemmas that reach across our algebraic hierarchy and manipulate a variety of structures.

Multiplicative finite subgroups of fields

Motivation, notations and framework Our first example is the well-known property that a finite multiplicative subgroup of a field is cyclic. When applied to F * , the multiplicative group of non-null elements of a finite field F , it is instrumental in defining the discrete logarithm, a crucial tool for cryptography. Various textbook proofs of this result exist [START_REF] Rotman | An Introduction to the Theory of Groups[END_REF][START_REF] Lang | Algebra[END_REF], prompting us to state it as:

1 Lemma field _ mul _ group _ cyclic : forall (gT: finGroupType) 2 (G : {group gT}) (F : fieldType) (f : gT -> F), 3 {in G & G, {morph f : u v / u * v >-> (u * v)%R}} -> 4 {in G, forall x, f x = 1%R <-> x = 1} -> 5 cyclic G.
The correspondence of this lemma with its natural language counterpart becomes straightforward, once we dispense with a few notations: %R : is a scope notation for ring operations. {group gT} :

The types we defined in section 3 are convenient for framing their elements in a precise algebraic setting. However, since a large proportion of the properties we have to consider deal with relations between sets of elements sharing such an algebraic setting, we have chosen to define the corresponding settheoretic notions, for instance sets and groups, as a selection of elements of their underlying type, as covered in [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF].

{morph f : u v / u * v >-> (u * v)%R} :
This reads as :∀x, y, f

(x * y) = (f x) * R (f y). {in G, P} : If P is of the form ∀x, Q(x) this means ∀ x ∈ G, Q(x).
Additional & symbols (as in line 3 above) extend the notation to relativize multiple quantifiers.

The type of f along with the scope notation %R, allows Coq to infer the correct interpretation for 1 and the product operator on line 3. field _ mul _ group _ cyclic therefore states that any finite group G mapped to a field F by f, an injective group morphism for the multiplicative law of F, is cyclic. 6Fun with polynomials Our proof progresses as follows: if a is an element of any such group C of order n, we already know that a n = 1. C thus provides at least n distinct solutions to X n = 1 in any group G it is contained in. Moreover, reading the two last lines of our goal above, it is clear that f maps injectively the roots of that equation in G to roots of X n = 1 in F . Since the polynomial X n -1 has at most n roots in F , the arbitrarily chosen C is exactly the collection of roots of the equation in G.

This suffices to show that for a given n, G contains at most one cyclic group of order n. Thanks to a classic lemma ( [START_REF] Rotman | An Introduction to the Theory of Groups[END_REF], 2.17), this means that G is cyclic.

An extensive development of polynomial theory on a unitary ring allows us to simply state the following definition in our proof script: pose P : {poly F} := ('X^n -1)%R.

The construction of the ring of polynomials with coefficients in a unitary ring (with F canonically unifying with such a ring) is triggered by the type annotation, and allows us to transparently use properties based on the datatype of polynomials, such as degree and root lemmas, and properties of the Ring structure built on the aforementioned datatype, such as having an additive inverse.

This part of the proof can therefore be quickly dispatched in Coq. The final lemma on cyclicity works with the cardinal of a partition of G, and is a good use case for the methods developed in [START_REF] Bertot | Canonical big operators[END_REF]; we complete its proof in a manner similar to the provided reference.

Importing various proof contexts inside a proof script is therefore a manageable transaction : here, we only had to provide Coq with the type of a mapping to an appropriate unitary ring for it to infer the correct polynomial theory.

Practical linear algebra

Motivations Reasoning on an algorithm that aims at solving systems of linear equations seems a good benchmark of our formalization of matrices. Indeed, the issue of representing fixed-size arrays using dependent types has pretty much become the effigy of the benefits of dependent type-checking, at least for its programatically-minded proponents.

However, writing functions that deal with those types implies some challenges, among which is dealing with size arguments. We want our library to simplify this task, while sharing operator symbols, and exposing structural properties of objects as soon as their shape ensures they are valid.

LUP decomposition

The LUP decomposition is a recursive function that returns, for any non-singular matrix A, three matrices P, L, U such that L is a lower-triangular matrix, U is an upper-triangular matrix, and P is a permutation matrix, and P A = LU .

We invite the reader to refer to ( [START_REF] Cormen | Introduction to Algorithms[END_REF], 28.3) for more details about this notorious algorithm. Our implementation is strikingly similar to a tail-recursive version of its textbook parent. Its first line features a type annotation that does all of the work of dealing with matrix dimensions: Here, in a fashion congruent with the philosophy of our archive, we return a value for any square matrix A, rather than just for non-singular matrices, and use the following shorthand: are auxiliary functions that use the shape 7 of the dependent parameter of their argument A to return respectively A ul , A ll , A ur , A lr when A is as repre-sented above. Notice we will now denote their application using the same subscript pattern.

1 Fixpoint cormen _ lup n : let M := 'M _ n.+1 in M -> M * M * M := 2 match n return let M := 'M _ (1 + n) in M -> M * M * M with 3 | 0 => fun A => (1%:M, 1%:M, A) 4 | n'.+1 => fun A => 5 let k := odflt 0 (pick [pred k | A k 0 != 0]) in
The rest of our notations can be readily interpreted, with 1 and 0 coercing respectively to identity and null matrices of the right dimension, and (A i j) returning the appropriate a i,j coefficient of A through coercion.

Correctness of the algorithm We will omit in this article some of the steps involved in proving that the LUP decomposition is correct: showing that P is a permutation matrix, for instance, involved building a theory about those matrices that correspond to a permutation map over a finite vector. But while studying the behavior of this subclass with respect to matrix operations gave some hint of the usability of our matrix library8 , it is not the part where our infrastructure shines the most. The core of the correction lies in the following equation:

Lemma cormen _ lup _ correct : forall n A, let: (P, L, U) := @cormen _ lup F n A in P * A = L * U.

Its proof proceeds by induction on the size of the matrix. Once we make sure that A' and Q (line 7) are defined coherently, it is not hard to see that we are proving is9 :

0 B B B @ 1 0 . . . 0 0 . . . P * A' 0 1 C C C A = 0 B B @ 1 0 . . . 0 a -1 k,0 • P' *m A' ll L 1 C C A * 0 B B B @ A ul A ur 0 . . . U 0 1 C C C A (1)
where P',L',U' are provided by the induction hypothesis

P' A' lr -a -1 k,0 • A' ll *m A' ur = L' * U' (2)
Notice that we transcribe the distinction Coq does with the three product operations involved: the scalar multiplication (•), the square matrix product ( * ), and the matrix product, accepting arbitrary sized matrices ( *m ). Using block product expansion and a few easy lemmas allows us to transform (1) into:

At this stage, we would like to rewrite our goal with (2) -named IHn in our script-, even though its right-hand side does not occur exactly in the equation. However, SSReflect has no trouble expanding the definition of the ring multiplication provided in [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF] to see it exactly matches the pattern10 -[L' * m U']IHn.

We conclude by identifying the blocks of (3) one by one. The most tedious step consists in treating the lower left block, which depends on whether we have been able to chose a non-null pivot in creating A' from A. Each alternative is resolved by case on the coefficients of that block, and it is only in that part that we use the fact that the matrix coefficients belong to a field. The complete proof is fourteen lines long.

Related Work

The need for packaging algebraic structures and formalizing their relative inheritance and sharing inside proof assistants is reported in literature as soon as these tools prove mature enough to allow the formalisation of significant pieces of algebra [START_REF] Jackson | Enhancing the Nuprl proof-development system and applying it to computational abstract algebra[END_REF]. The set-theoretic Mizar Mathematical Library (MML) certainly features the largest corpus of formalized mathematics, yet covering rather different theories than the algebraic ones we presented here. Little report is available on the organization a revision of this collection of structures, apart from comments [START_REF] Rudnicki | Commutative algebra in the Mizar system[END_REF] on the difficulty to maintain it. The Isabelle/HOL system provides foundations for developing abstract algebra in a classical framework containing algebraic structures as first-class citizens of the logic and using a type-class like mechanism [START_REF] Haftmann | Local theory specifications in Isabelle/Isar[END_REF]. This library proves Sylow theorems on groups and the basic theory of rings of polynomials.

Two main algebraic hierarchies have been built using the Coq system: the seminal abstract Algebra repository [START_REF] Pottier | User contributions in Coq[END_REF], covering algebraic structures from monoids to modules, and the CCorn hierarchy [START_REF] Geuvers | A constructive algebraic hierarchy in Coq[END_REF], mainly devoted to a constructive formalisation of real numbers, and including a proof of the fundamental theorem of algebra. Both are axiomatic, constructive, and setoid based. They have proved rather difficult to extend with theories like linear or multilinear algebra, and to populate with more concrete instances. In both cases, limitations mainly come from the pervasive use of setoids and the drawbacks of telescope based hierarchies pointed in section 2.

The closest work to ours is certainly the hierarchy built in Matita [START_REF] Sacerdoti Coen | Working with Mathematical Structures in Type Theory[END_REF], using telescopes and a more liberal system of coercions. This hierarchy, despite including a large development in constructive analysis [START_REF] Sacerdoti Coen | A constructive and formal proof of Lebesgue Dominated Convergence Theorem in the interactive theorem prover Matita[END_REF], is currently less populated than ours. For example, no counterpart of the treatment of polynomials presented in section 4 is described in the Matita system.

We are currently extending our hierarchy to extend the infrastructure to the generic theory of vector spaces and modules.

  Module Zmodule. Record mixin _ of (M : Type) : Type := Mixin { zero : M; opp : M -> M; add : M -> M -> M; _ : associative add; _ : commutative add; _ : left _ id zero add; _ : left _ inverse zero opp add }. ... End Zmodule.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Telescopes for Equality and Zmodule

Fig. 3 .

 3 Fig. 3. The algebraic hierarchy in the ssreflect libraries

  Module Choice. Definition xfun (T : Type) := forall P : pred T, (exists x, P x) -> T. Definition correct (f : xfun) := forall (P : pred T) xP, P (f P xP). Definition extensional (f : xfun) := forall P Q xP xQ, P =1 Q -> f P xP = f Q xQ. Record mixin _ of (T : Type) : Type := Mixin { xchoose : xfun T; xchooseP : correct xchoose; eq _ xchoose : extensional xchoose}. Record class _ of (T : Type) : Type := Class { base :> Equality.class _ of T; ext2 : mixin _ of (seq (seq T)) }. ... End Choice.

  Module ComUnitRing. Record class _ of (R : Type) : Type := Class { base1 :> ComRing.class _ of R; ext :> UnitRing.mixin _ of (Ring.Pack base1 R)}. Coercion base2 R m := UnitRing.Class (@ext R m). ... End ComUnitRing.

6 13 (

 13 let A' := rswap A 0 k in 7 let Q := tperm _ mx F 0 k in 8 let Schur := ((A k 0)^-1 * m: llsubmx A') * m ursubmx A' in 9 let: (P', L', U') := cormen _ lup (lrsubmx A' -Schur) in 10 let P := block _ mx 1 0 0 P' * Q in 11 let L := block _ mx 1 0 ((A k 0)^-1 * m: (P' * m llsubmx A')) L' in 12 let U := block _ mx (ulsubmx A') (ursubmx A') 0 U' in

  • P' *m A' ll *m A' ul a -1 k,0 • P' *m A' ll *m A'ur + L' *m U'

odflt 0 (pick [pred k:fT | P k]) returns

  k, an inhabitant of the finType fT such that P k if it exists, and returns 0 otherwise.

	blockmx Aul Aur All Alr
	reads as Aul Aur All Alr .

ulsubmx, llsubmx, ursubmx, lrsubmx

It is nevertheless impractical to use the Coq Module construct to package these three fixed definitions, because of its verbose syntax and technical limitations.

Unlike in[START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF], cyclic is a boolean predicate that corresponds to the usual meaning of the adjective.

As crafted in line 2 above

François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau

The theory, while expressed in a general manner, is less than ninety lines long.

We will write block expressions modulo associativity and commutativity, to reduce parenthesis clutter.

See[START_REF] Gonthier | A small scale reflection extension for the Coq system[END_REF] for details on the involved notation for the rewrite tactic.