Hugo Herbelin
email: hugo.herbelin@inria.fr

Ramkumar Ramachandra

Hugo Moeneclaey

Thorsten Altenkirch

A parametricity-based formalization of semi-simplicial and semi-cubical sets

Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semisimplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of n-simplices or n-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.

b ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory c In hindsight, the title of the paper "A dependently-typed construction of semi-simplicial types" is somewhat confusing: it implicitly claimed to construct semi-simplicial types, but the construction was done in a type theory with Uniqueness of Identity Proofs. Consequentially, what was really obtained was an indexed presentation of semi-simplicial sets. The confusion was however, common at the time.

d github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda

I Introduction

Fibered vs indexed presentation of semi-simplicial and semi-cubical sets

A family of sets can commonly be represented in two ways: as a family properly speaking, indexed by the elements of a given set S, or as a set T together with a map from T to S, which specifies for each element of T its dependency on S. In the former case, we call it an indexed presentation. In the latter case, the set associated to a given element of S is the fiber of this element, so we call it a fibered presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF] as the fibered/indexed equivalence a .

(fibered)

(ΣT : HSet.(T → S)) ≃ (S → HSet) (indexed)

Here, HSet represents in homotopy type theory the subset of types within a given universe where equality of any two elements has at most one proof.

A presheaf on an category is a family of sets indexed by the object of the category with maps indexed by the morphisms. As such, it lives on the indexed side of the equivalence, contrasting with the fibered side, where we have discrete Grothendieck fibrations [START_REF] Loregian | Categorical notions of fibration[END_REF]. However, there are situations where a presheaf can also be seen as living on the fibered side of the equivalence. This happens when the indexing category is direct, or has a downwards-well-founded collection of non-identity morphisms. Let us consider, for instance, the case of a semi-cubical set [START_REF] Grandis | Cubical sets and their site[END_REF][START_REF] Buchholtz | Varieties of cubical sets[END_REF] presented with 2n face maps from the set of n-cubes to the set of (n -1)-cubes. Formulated in type theory, the corresponding presheaf definition of a semi-cubical set prescribes a family of sets and face maps between them as follows.

X 0 : HSet X 1 : HSet X 2 : HSet . . .

∂ L ∂ R ∂ L⋆ ∂ R⋆ ∂ ⋆L ∂ ⋆R
a In an informal discussion, alternative nomenclatures were proposed: fibration/family equivalence and unbundled/bundled equivalence. The fibered/indexed nomenclature echoes the Grothendieck construction of fibered categories from indexed categories. The most elementary instance of the equivalence, with Type instead of HSet, is sometimes called "Grothendieck construction for dummies", and its proof requires univalence [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF].

I. INTRODUCTION 2/ 15

up to cubical faces identities. Here, X 1 can be seen as a family over X 0 × X 0 , and X 2 can be seen as a family over X 1 × X 1 × X 1 × X 1 , in the fibered presentation. This suggests an alternative indexed presentation of the presheaf as a stratified sequence of families indexed by families of lower rank, taking into account the coherence conditions to prevent duplications. Formulated in type theory, it takes the form:

X 0 : HSet X 1 : X 0 × X 0 → HSet X 2 : Πabcd. X 1 (a, b) × X 1 (c, d) × X 1 (a, c) × X 1 (b, d) → HSet . . .
The idea for such an indexed presentation of presheaves over a direct category was mentioned at the Univalent Foundations year in the context of defining semi-simplicial types b . A few constructions have been proposed since then. The first construction by [START_REF] Voevodsky | Semi-simplicial types[END_REF] relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by [START_REF] Herbelin | A dependently-typed construction of semi-simplicial types[END_REF] c formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by [START_REF] Part | Semi-simplicial types in logic-enriched homotopy type theory[END_REF] formalized in an emulation of logic-enriched homotopy type theory in the Plastic proof assistant, and yet another by [START_REF] Annenkov | Two-level type theory and applications[END_REF] formalized in an emulation of a two-level type theory in the Agda proof assistant d , rely on the presentation of the semi-simplicial category from increasing injective functions over finite ordinals.

The indexed definition of a presheaf over a direct category is technically more involved than the presheaf definition, as it requires hard-wiring in the structure the dependencies between elements of the sets of the presheaf, including the coherence conditions between these dependencies, such as taking the i-th face of the j-th face of a n-simplex being the same as taking the (j -1)-th face of the i-th face (when j > i). However, exhibiting a concrete instance of a presheaf in indexed form only requires providing the families, since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition of the structure.

Reynolds parametricity and its unary and binary variants

In the context of functional programming, Reynolds parametricity ( [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF]) interprets types as relations characterizing the observational behavior of programs of this type. More generally, families over a product of sets, or correspondences, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered presentation of correspondences as spans, it has been noted that iterated Reynolds parametricity has the structure of a cubical set [START_REF] Altenkirch | Towards a cubical type theory without an interval[END_REF][START_REF] Moulin | Internalizing parametricity[END_REF][START_REF] Johann | Cubical categories for higher-dimensional parametricity[END_REF][START_REF] Moeneclaey | Parametricity and semi-cubical types[END_REF][START_REF] Moeneclaey | Cubical models are cofreely parametric[END_REF]. We obtain a unary variant of Reynolds binary parametricity by using predicates or families instead of relations or correspondences, and this is a form of realizability [START_REF] Bernardy | A computational interpretation of parametricity[END_REF][START_REF] Lasson | Réalisabilité et Paramétricité dans les Systèmes de Types Purs[END_REF][START_REF] Moulin | Internalizing parametricity[END_REF]. It has then been noted that iterated unary parametricity has the structure of an augmented simplicial set e . This suggests that the definition of augmented semi-simplicial sets and semi-cubical sets can both be seen as instances of a more general construction, which we call ν-sets, of presheaves over a ν-semi-shape category made of words of some cardinal ν + 1, where ν = 1 gives augmented semi-simplicial sets and ν = 2 gives semi-cubical sets.

Contribution

The main contribution of the paper is to describe the details of a recipe that uniformly characterizes unary and binary iterated parametricity in indexed form, and to derive from it a new indexed presentation, called indexed ν-sets, of augmented semi-simplicial and semi-cubical sets.

Our work is a step in the direction of the program initiated in [START_REF] Altenkirch | Towards a cubical type theory without an interval[END_REF] to develop parametricity-based models of parametric type theory [BCM15, NVD17, CH20] and cubical type theory [BCH13, CCHM18, ABC + 21], which are closer to the syntax of type theory, and are likely to better reflect the definitional properties of type theory than presheaf-based cubical sets would. For example, consider the loss of definitional properties when interpreting "indexed" dependent types of type theory as "fibrations" in models such as locally cartesian closed categories [START_REF] Curien | Revisiting the categorical interpretation of dependent type theory[END_REF].

Our mechanization can be found at github.com/artagnon/bonak. The construction was conceived in Summer 2019, and the mechanization began in late 2019. A sketch of the construction was presented at the 2020 HoTT-UF workshop, and the completion of the mechanization was reported at the TYPES 2022 conference.

II Semi-simplicial and semi-cubical sets

In this section, we generalize semi-simplicial and semi-cubical sets to ν-sets, subsuming the earlier definitions. We start with some introductory material on semi-simplicial and semi-cubical sets.

Augmented semi-simplicial sets

Augmented semi-simplicial sets are defined similarly to semi-simplicial sets, except that the connected components are additionally dependent on a "color". Conversely, semi-simplicial sets can be seen as augmented semi-simplicial sets over the singleton set of a fixed color. Let us associate dimension 0 to colors; then, points are dimension 1, lines are dimension 2, and so on. There is hence a shift by one when compared to semi-simplicial sets.

While ordinary semi-simplicial sets are presheaves over the semi-simplex category, augmented semi-simplicial sets are presheaves over ∆ + . There are different ways to define ∆ + , up to equivalence, and we use a definition that can be extended to semi-cubical sets in a straightforward manner. II.0.1 Notation [Finite sequences] We denote finite sequences by i 1 . . . i n for i j ranging over some domain. The empty sequence is written ϵ. II.0.2 Definition [∆ + ] The definition of ∆ + is shown below. Note that, if g • f is well-defined, then the length of f is less than that of g. It can be shown that composition is associative and that id is neutral.

Obj ∆ + := N Hom ∆ + (p, n) := {l ∈ {0, ⋆} n | number of ⋆ in l = p} g • f :=      f if g = ϵ 0 (g ′ • f ) if g = 0 g ′ a (g ′ • f ′ ) if g = ⋆ g ′ , f = a f ′ , where a = 0 or ⋆ id := ⋆ . . . ⋆ n times for id ∈ Hom ∆ + (n, n) II.0.3 Definition [Set ∆ + ]
We define the category of augmented semi-simplicial sets as the functor category:

Set ∆ + := Set ∆ op +
To provide examples, we define the standard augmented n-semi-simplex.

II.0.4 Definition [∆ n

+ ] The standard augmented n-semi-simplex ∆ n + is defined as the Yoneda embedding of n ∈ Obj(∆ + ):

∆ n + : Set ∆ + ∆ n + (p) := Hom(p, n) ∆ n + (f ) := λg. g • f
The standard augmented 0-semi-simplex is a singleton made of one color (in this case, black). Standard augmented n-semi-simplices for n ≥ 1 have a geometric interpretation, and we illustrate them for dimensions 1, 2, and 3.

II.0.5 Example [∆ 1

+ ] The standard augmented 1-semi-simplex can be pictured as a point, colored black, corresponding to the unique morphism in Hom(0, 1). This point is the identity in Hom(1, 1); it is hence shown as a singleton ⋆. ⋆

II.0.6 Example [∆ 2 + ]
The standard augmented 2-semi-simplex is drawn as two points, given by Hom(1, 2), along with a line connecting them, given by Hom(2, 2). We use black to denote the unique morphisms in Hom(0, 1) and Hom(0, 2). ⋆0 0⋆ ⋆⋆ II.0.7 Example [∆ 3 + ] ∆ 3 + is drawn as three points, given by Hom(1, 3), three lines connecting them, given by Hom(2, 3), and a triangular filler given by Hom(3, 3). 00⋆

⋆00 0⋆0 0⋆⋆ ⋆⋆0 ⋆0⋆

⋆⋆⋆

More generally, the standard augmented (n + 1)-semi-simplex can be obtained by taking a copy of the standard augmented n-semi-simplex serving as a base, and gluing on top of it another copy lifted by one dimension. In the second copy, the color becomes an extra point, the points become lines connecting the points of the base to the extra point, and so on. In particular, the components of the base are those of the standard augmented n-semi-simplex postfixed by 0 while the components of the lifted copy are postfixed by ⋆. Note that the components may be oriented by letting each n-dimensional component point to the (n -1)-dimensional component obtained by replacing the leftmost ⋆ of the n-dimensional component with 0.

Semi-cubical sets

Semi-cubical sets are defined like augmented semi-simplicial sets except that ∆ + is replaced by □ in which we take sequences of L, R and ⋆, instead of sequences of 0 and ⋆.

II.0.8 Definition [□]

The definition of □ is shown below. The symbols L and R indicate opposite faces of a cube.

Obj □ := N Hom □ (p, n) := {l ∈ {L, R, ⋆} n | number of ⋆ in l = p} g • f :=      f if g = ϵ a (g ′ • f ) if g = a g ′ , where a = L or R a (g ′ • f ′ ) if g = ⋆ g ′ , f = a f ′ , where a = L, R, or ⋆ id := ⋆ . . . ⋆ n times
Again, if g • f is well-defined, then the length of f is less than that of g. It can be shown that composition is associative and that id is neutral. II.0.9 Definition [Set □ ] We define the category of semi-cubical sets as the functor category:

Set □ := Set □ op II.0.10 Definition [□ n ]
The standard semi-cube □ n is defined as the Yoneda embedding of n ∈ Obj(□):

□ n : Set □ □ n (p) := Hom(p, n) □ n (f ) := λg. g • f
Standard n-semi-cubes have a geometric interpretation, which we illustrate for dimensions 0, 1, and 2. II.0.11 Example [□ 0 ] □ 0 is Hom(0, 0), or the singleton set of the empty sequence: ϵ II.0.12 Example [□ 1 ] □ 1 consists of two points, given by Hom(0, 1), and a line, given by Hom(1, 1).

L R

⋆ II.0.13 Example [□ 2 ] □ 2 consists of four points, given by Hom(0, 2), four lines connecting the four points, given by Hom(1, 2), and a filler, given by Hom(2, 2):

LR RR LL RL ⋆R L⋆ R⋆ ⋆L ⋆⋆
More generally, the standard (n + 1)-semi-cube can be obtained by taking two copies of the standard nsemi-cube serving as bottom and top face and connecting them on their border by a cylinder obtained as a third copy stretched in the new dimension. The bottom and top faces are obtained from the standard n-semicube by postfixing with respectively L and R while the cylinder is obtained by postfixing with ⋆. Note that the components can be oriented by letting each n-dimensional component go from the (n -1)-dimensional component obtained by replacing the leftmost ⋆ with L, to the one obtained by replacing the leftmost ⋆ with R.

ν-sets

Let us call ν-sets, the generalization of augmented semi-simplicial sets and semi-cubical sets obtained by building on an arbitrary alphabet ν, so that the following holds:

Cardinal of ν 1 2 Interpretation Augmented semi-simplicial types Semi-cubical types
To obtain this, we extend ∆ + and □ in a straightforward manner into a category which we call . II.0.14 Definition [ ] The definition of ν-semi-shape category is shown below. Note that, if g • f is well-defined, then the length of f is less than that of g. It can be shown that composition is associative and that id is neutral.

Obj := N Hom (p, n) := {l ∈ (ν ⊔ {⋆}) n | number of ⋆ in l = p} g • f :=      f if g = ϵ a (g ′ • f ) if g = a g ′ , where a ∈ ν a (g ′ • f ′ ) if g = ⋆ g ′ , f = a f ′ , where a ∈ ν or a = ⋆ id := ⋆ . . . ⋆ n times for id ∈ Hom (n, n)
A ν-set is thus a contravariant functor ϕ from the ν-semi-shape category to Set and we call n-ν-semi-shape an element of ϕ(n). As in the augmented semi-simplicial and semi-cubical cases, the standard (n + 1)-νsemi-shape is obtained by connecting together ν copies of the standard n-ν-semi-shape with an extra copy stretched in the new dimension. We clarify in the next sections, how this process of construction is similar to the parametricity translation developed for functional programming [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] and more generally for type theory [BJP10, BL11, AGJ14, BCM15].

III Type theory

Martin-Löf's Type theory ( [START_REF] Martin-Löf | An intuitionistic theory of types, predicative part[END_REF][START_REF] Martin-Löf | Intuitionistic type theory[END_REF]) is a logical formalism based on the notion of a type rather than that of a set. It can be seen as a foundation of mathematics alternative to set theory and is the core of several tools for the formalization of mathematics such as Agda ([The23a]), Coq ( [START_REF]The Coq Reference Manual[END_REF]) and Lean ([dMKA + 15]). In type theory, propositions are types and proofs are programs. Type theory includes definitional equality, by which all propositions and proofs are quotiented.

Type theory is a flexible formalism supporting different models. Some models are based on topological spaces, where equality is interpreted as path, and substitutivity of equality as transport [START_REF] Kapulkin | The simplicial model of univalent foundations (after voevodsky)[END_REF]. These models support the univalence principle stating that equality of types mimics equivalence of types, leading to the development of Homotopy Type Theory [START_REF]Homotopy Type Theory: Univalent Foundations of Mathematics[END_REF].

Types are organized in a hierarchy of universes written Type m for m a natural number. The main types in type theory are the type of dependent pairs, written Σa : A. B(a), the type of dependent functions, written Πa : A. B(a), for A a type and B(a) a type dependent on the inhabitant a of A, and the type of propositional equalities, written t = u. As a notation, the type of dependent pairs when B is not dependent on A is shortened into A × B and the type of dependent functions when B is not dependent on A is written A → B. We assume our type theory to also include a distinguished singleton type, written unit, and with inhabitant * , the type of boolean values, and the type of natural numbers. We also assume that our type theory includes the coinductive type of infinite dependent tuples. We write hd and tl the projections of dependent pairs, and refl for reflexivity. Logical propositions being types themselves, we use Π to represent universal quantification and Σ to represent existential quantification.

A type-theoretic notion of sets can be recovered in each universe as HSet m , denoting the subtype of Type m for which paths are degenerated, using Uniqueness of Identity Proofs (UIP). Technically, this is expressed as a structure equipping a domain Dom with the property UIP: Dom : Type m UIP : Πxy : Dom. Πpq : x = y. p = q In HSet m , the following properties hold: 1. UIP holds on the unit type, bool type, as well as all types of finite cardinal ν. 2. UIP propagates to Σ-types. 3. UIP propagates to Π-types, with some additional functional extensionality axioms. By notation, Type and HSet mean Type m and HSet m at some unspecified universe level m. We are also interested in extensional type theory, a type theory with the following reflection rule, where = is propositional equality in some type and ≡ is definitional equality [START_REF] Martin-Löf | Intuitionistic type theory[END_REF]:

Γ ⊢ p : t = u Γ ⊢ t ≡ u
Note that the reflection rule implies UIP so that HSet and Type are equivalent in extensional type theory. The reflection rules also implies functional extensionality. Extensional type theory is logically equivalent to intensional type theory extended with UIP and functional extensionality [START_REF] Hofmann | Extensional concepts in intensional type theory[END_REF].

IV Relating to parametricity

Recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:

X 0 : HSet X 1 : X 0 × X 0 → HSet X 2 : Πabcd. X 1 (a, b) × X 1 (c, d) × X 1 (a, c) × X 1 (b, d) → HSet . . .
Here, the process of construction of the type of X 1 from that of X 0 , and of the type of X 2 from that of X 1 , is similar to iteratively applying a binary parametricity translation. The binary parametricity which we consider interprets a closed type A by a family A ⋆ over A × A, and this can be seen as a graph whose vertices are in A. Each type constructor is associated with the construction of a graph. To start with, the type of types HSet is interpreted as the family of type of families HSet ⋆ , which takes A L and A R in HSet and returns the type A L × A R → HSet of families over A L and A R . Also, for A interpreted by A ⋆ and B interpreted by B ⋆ , a dependent function type Πa : A. B is interpreted as the graph (Πa : A. B) ⋆ that takes two functions f L and f R of type Πa : A. B, and expresses that these functions map related arguments in A to related arguments in B:

(Πa : A. B) ⋆ (f L , f R ) ≜ Π(a L , a R ) : (A × A). (A ⋆ (a L , a R ) → B ⋆ (f L (a L ), f R (a R ))) Similarly, a product type A × B is interpreted as the graph (A × B) ⋆ that relates two tuples (a L , b L ) and (a R , b R ) in A × B as follows: (A × B) ⋆ ((a L , b L ), (a R , b R )) ≜ A ⋆ (a L , a R ) × B ⋆ (b L , b R )
In particular, for X : HSet, applying our parametricity translation is about associating to X an inhabitant X ⋆ of HSet ⋆ (X, X) i.e. of X × X → HSet. In turn, applying the translation again to X ⋆ : X × X → HSet is about associating to X ⋆ an inhabitant X ⋆⋆ of (X × X → HSet) ⋆ (X ⋆ , X ⋆ ) i.e. of:

Π((x LL , x LR ), (x RL , x RR )) : ((X × X) × (X × X)). (X ⋆ (x LL , x LR ) × X ⋆ (x RL , x RR ) → X ⋆ (x LL , x RL ) × X ⋆ (x LR , x RR ) → HSet)
which hints us at how the sequence X 0 , X 1 , X 2 can be seen as a sequence of inhabitants of the iteration of the composition of binary parametricity with the diagonal on types and type families, applied to an initial X : HSet:

X 0 ≜ X : HSet X 1 ≜ X ⋆ : HSet ⋆ (X, X) X 2 ≜ X ⋆⋆ : (HSet ⋆ (X, X)) ⋆ (X ⋆ , X ⋆ ) . . .
This tells us how the informal type given to X 2 in the previous section could be rephrased so that it comes as the instance of a general recipe characterizing the type of all X i . Notice, however, that the recipe obtained so far, X n+1 : (S n ) ⋆ (X n , X n ) for X n : S n , applies parametricity on the syntax of the type of X n . It does not directly yield a characterization of S n as a function from n. Reformulating the recipe as an explicit recursive construction, without requiring an interpretation of the syntax of types, is the main outcome of this work, together with the mechanization and the uniform treatment of augmented semi-simplicial and semi-cubical sets by means of the generalization to ν-sets.

V Our construction

In this section, we describe our parametricity-based construction of ν-sets in indexed form at two levels of formality.

Sections V.1 and V.3 describe the construction at an informal level of discourse: 1. In V.1, we present it in informal extensional type theory where equational reasoning is left implicit, and we give an intuition for the construction in V.2. 2. While reasoning in extensional type theory is similar to reasoning in set theory regarding how equality is handled, extensional type theory has two limitations. The first limitation is that it enforces the principle of Uniqueness of Identity Proofs and this is inconsistent with the Univalence principle, thus making it inexpressible in Homotopy Type Theory. The second limitation is that we want the construction to be formalizable in the Coq proof assistant whose underlying type theory is intensional. Section V.3 thus rephrases the construction in (informal) intensional type theory. Sections V.4, V.5, and V.6 describe additional issues to be addressed in order to get a fully formal construction:

1. The well-foundedness of the induction requires a special termination evidence which will be discussed in section V.4. 2. The construction is indexed over integers and holds under some constraints on the range of these integers.

There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities on natural numbers. We discuss how we deal with such dependencies in section V.5. 3. A number of standard groupoid properties of equality as well as type isomorphisms have been left implicit in the informal definition. This is discussed in section V.6.

V.1 The construction in informal type theory

A ν-set in indexed form is a sequence of families of HSet, that is HSet m for some universe level m. We call such sequence a ν-set at level m, whose type thus lives in HSet m+1 . Table 1 describes the type of a ν-set at level m in indexed form, as the type of a coinductively-defined infinite sequence of type families representing the limit of n-truncated ν-sets: νSet ≥n m denotes an infinite sequence X n+1 , X n+2 , . . . dependent on a n-truncated ν-set, νSet <n m , so that, when n is 0, it denotes a full ν-set, written νSet m . This is made possible because the 0-truncated ν-set, νSet <0 m , is degenerated: it is an empty family, and there is thus only one 0-truncated ν-set, namely the canonical inhabitant ⋆ of unit.

The definition of the type of a n-truncated ν-set is in turn described in table 2. In the infinite sequence of type families representing a ν-set, the n-th component is a type dependent over a fullframe. It is recursively defined in table 3, using the auxiliary definitions of frame, layer and painting. A fullframe describes a boundary of a standard form (simplex, cube), which we decompose into layer, and a painting corresponds to a filled frame. Notice that the type layer relies on an operator of frame restriction restr frame which is defined in table 4, and this restriction operator is in turn defined using auxiliary definitions restr layer and restr painting .

Notably, the definition of restr layer relies on an equality expressing the commutation of the composition of two restr frame . The proof of this commutation is worth being made explicit, which we do in table 5 using proof-term notations. The proof requires an induction on the dimension and on the structure of frame, layer, and painting. This is what coh frame does using auxiliary proofs coh layer and coh painting . Even though it looks independent of the definitions from the other tables, coh frame has to be proved mutually with the definitions of frame, layer, painting, and their corresponding restrictions. More precisely, for a fixed n, the block of frame, restr frame , and coh frame has to be defined in one go by induction on p. Also, each of painting, restr painting , and coh painting is built by induction from p to n. The painting block at n relies on the frame block at n, but the converse dependency is only on lower n, so this is well-founded. Note that layer, restr layer and coh layer are just abbreviations. The exact way this mutual recursion is eventually formalized is explained in section V.4.

Note that for a fixed constant n, relying on the evaluation rules of type theory, the coherence conditions degenerate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore.

{D : νSet <n } (d : frame n,p (D)) : frame n-1,p (D.1) restr n,0 frame,ϵ,q D * ≜ * restr n,p ′ +1
frame,ϵ,q D (d, l) ≜ (restr n,p ′ frame,ϵ,q (d), restr n,p ′ layer,ϵ,q-1 (l))

restr n,p,p≤q≤n-2 layer,ϵ,q {D : νSet <n } {d : frame n,p (D)} (l : layer n,p (d))

: layer n-1,p (restr n,p frame,ϵ,q+1 (d))

restr n,p layer,ϵ,q D d l ≜ λω.(restr n-1,p painting,ϵ,q (D.2)(lω))

restr n,p,p≤q≤n-1 painting,ϵ,q

(D : νSet <n ) (E : νSet =n (D)) (d : frame n,p (D)) (c : painting n,p (E)(d))
:

painting n-1,p (D.2)(restr n,p frame,ϵ,q+1 (d))

restr n,p,p=q painting,ϵ,q

D E d (l, _) ≜ lϵ restr n,p,p<q painting,ϵ,q D E d (l, c)
≜ (restr n,p layer,ϵ,q (l), restr n,p+1 painting,ϵ,q (E)(c))

Table 4: q-th projection of restr, or faces

coh n,p,p≤r≤q≤n-2 frame,ϵ,ω,q,r {D : νSet <n } (d : frame(D)) : restr n-1,p frame,ϵ,q (restr n,p frame,ω,r (d)) = restr n-1,p frame,ω,r (restr n,p frame,ϵ,q+1 (d)) coh n,0 frame,ϵ,ω,q,r D * ≜ refl( * ) coh n,p ′ +1 frame,ϵ,ω,q,r D (d, l) ≜ (coh n,p ′ frame,ϵ,ω,q,r (d), coh n,p ′ layer,ϵ,ω,q,r (l))
coh n,p,p<r≤q≤n-2 layer,ϵ,ω,q,r (D : νSet <n ) {d : frame(D)} (l : layer(d))

: restr n-1,p layer,ϵ,q (restr n,p layer,ω,r (l)) = restr n-1,p layer,ω,r (restr n,p layer,ϵ,q+1 (l)) coh n,p layer,ϵ,ω,q,r

D d l ≜ λθ. coh n-1,p painting,ϵ,ω,q-1,r-1 (D.2)(l θ ) coh n,p,p≤r≤q≤n-2 painting,ϵ,ω,q,r (D : νSet <n ) (E : νSet =n (D)) (d : frame(D)) (c : painting(E)(d))
:

restr n-1,p painting,ϵ,q (D.2)(restr n,p painting,ω,r (E)(c)) = restr n-1,p painting,ω,r (D.2)(restr n,p painting,ϵ,q+1 (E)(c))

coh n,p,p=r painting,ϵ,ω,q,r D E d (l, _) ≜ refl(restr n-1,p painting,ϵ,q-1 (D.2)(lϵ)) coh n,p,p<r painting,ϵ,ω,q,r D E d (l, c) ≜ (coh n,p layer,ϵ,ω,q,r (l), coh n,p+1 painting,ϵ,ω,q,r (E)(c))

V.2 Intuition for our formal construction

There is a fullframe for each dimension n, written fullframe n , and every X n is uniformly assigned a type of the form fullframe n → HSet. Here, fullframe n is a "telescope" collecting all arguments of the type of X i in section IV as a nesting of Σ-types.

To illustrate how to recursively build fullframe n , let us begin by setting fullframe 0 ≜ unit, so that the type HSet given to X 0 in section IV can be equivalently formulated as unit → HSet. Then, more generally, let each fullframe n consist of n layers, written layer n,p with p < n, that we stack in order, starting from unit, and writing frame n,p for the p first layers of a fullframe n , so that fullframe n is frame n,n . For instance, X 1 is made of one layer, so that it can be written as a Σ-type of an inhabitant of unit and layer 1,0 . Then, X 2 is similarly made of two layers.

X 0 : unit frame 0,0 → HSet X 1 : Σ * : unit.        X 0 ( * ) painting 0,0 × X 0 ( * ) painting 0,0        layer 1,0 frame 1,1 → HSet X 2 : Σa :                             Σ * : unit.                        Σb : X 0 ( * ) × X 0 ( * ) . X 1 ( * , b) restr 2,0 frame,L painting 1,1 painting 1,0 × Σb : X 0 ( * ) × X 0 ( * ) . X 1 ( * , b) restr 2,0 frame,R painting 1,1 painting 1,0                        layer 2,0                             frame 2,1 .                   X 1 a.hd, a.tl.L.hd.L, a.tl.R.hd.L restr 2,1 frame,L painting 1,1 × X 1 a.hd, a.tl.L.hd.R, a.tl.R.hd.R restr 2,1 frame,R painting 1,1                   layer 2,1 frame 2,2 → HSet . . .
Let us now illustrate the construction of fullframe 3 , necessary to build the type of X 3 .

The figure on the left is frame 3,1 , in the middle is frame 3,2 , and on the right is frame 3,3 , which is full. Further, frame 3,1 is made of one layer, layer 3,0 , shown in blue, frame 3,2 is made of one additional layer, layer 3,1 , shown in red, frame 3,3 is made of one more layer, layer 3,2 , shown in green.

We illustrated here the cubical case, that is ν = 2, but, in general, a layer n,p is a product of ν painting n-1,p . A painting n,0 is a n-dimensional object corresponding to a filled fullframe n . More generally, a painting n,p is an n-dimensional object which has the form of a painting n-p,0 , thus of (n -p)-dimensional form, but shifted and living in dimensions p to n. Such painting n,p fills a space framed by a partial frame n,p so that, together, they form a filled fullframe n . For instance, in the picture, each of the two painting 2,0 of layer 3,0 is a filled blue square, each of the two painting 2,1 of layer 3,1 is a line, shown in red, stretched into a partial square filling the partial frames made of respectively, the left and right border of the blue square, and each of the two painting 2,2 of layer 3,2 is the point shown in green, stretched into a partial square filling the full frames made respectively of the upper and lower borders of the blue and red squares. A painting n,p complements a frame n,p by adding layers needed to form a fullframe n and by filling the resulting fullframe n with an inhabitant of X n . Layers are added from dimension n to dimension p, opposite to the order from 0 to p the frame n,p are built, as shown below.

frame n,p ≜ Σa n : (. . . (Σ * : layer n,0 ) . . .). layer n,p-1 painting n,p ≜ Σl p : layer n,p .(. . . (Σl n : layer n,n-1 . X n ) . . .)

So far, we have not paid attention to the fact that we have a dependent type, shown as Σ. To be more precise, note that fullframe n depends on all X i up to n -1. So, we need to package up X i , for i < n, into a nesting of Σ-types, constituting the type of a n-truncated ν-set, which we wrote νSet <n . This allows us to give the type νSet <n → HSet to fullframe n . Then, for D : νSet <n , representing an initial prefix of X 0 , X 1 , . . . X n-1 , the indexed set X n has type fullframe n (D) → HSet. Thus, frame n,p , layer n,p and painting n,p also depend on D. We can then reformulate the previous equation with its dependency on D. In particular, X n is just the last component of D, that is D.tl. An extra refinement arises from the fact that each new layer of a frame has to be glued onto the border of the partial frame built so far. So, each layer n,p has to depend on frame n,p . We also need a way to characterize the ν borders of each painting n-1,p that composes a layer n,p , and this is where the restriction restr n,p frame,ϵ,p arrives, for each ϵ < ν. For instance, in the picture, the left and right painting 2,1 , shown in red, are laid on respectively the left and right borders of the blue boxes, and hence need to depend on frame 3,1 . The left and right borders of the two blue boxes are then extracted as restr 2,1 frame,L (D)(d) and restr 2,1 frame,R (D)(d). We can then refine again the previous equation by showing the dependencies on d, as shown below. where (d, l p , . . . , l q ) abbreviates ((. . . (d, l p ), . . .), l q )

When ν = 2, using L and R to represent the sides, the formation of layers from paintings amounts to: The operation restr n,p frame,ϵ,q restricts the p first layers of a frame, and the construction is by recursion on the structure of a frame d. This necessitates the definitions restr n,p layer,ϵ,q (d)(l) and restr n,p painting,ϵ,q (d)(c), for l a layer, and c a painting. The key case is restr n,p painting,ϵ,p (d)(c), where c, a painting n,p , necessarily has the form of ((c L , c R ), _). Here, restr n,p painting,L,p picks out c L , a painting n-1,p , restr n,p painting,R,p picks out the c R , also a painting n-1,p , and the last component, shown as _, a painting n,p+1 , is discarded. There is one last difficulty, which we illustrate by writing down expected and actual types.

Given c ω of type c ω : painting n-1,p (D.hd)(restr n-1,p frame,ω,q (d))

restr n,p layer,ϵ (d)(c L , c R ) produces a layer in which the ω-component has the type painting n-2,p (D.hd.hd)(restr n-1,p frame,ϵ,q (restr n,p frame,ω,p (d)))

while we expect a component of type painting n-2,p (D.hd.hd)(restr n-1,p frame,ω,p (restr n,p frame,ϵ,q+1 (d)))

Hence, we need a coherence condition to commute the restrictions. Coherence conditions similar to this necessitate what are shown as, coh frame , coh layer and coh painting in table 5. These are by induction on the structure of frame, layer and painting. Note that, for the construction in intensional type theory, we further need a 2-dimensional coherence condition, coh2 frame , for coh layer , which is explained in the next section.

V.3 From extensional to intensional type theory

In this section, we intend to get rid of the reflection rule and make explicit the equational reasoning step needed to rephrase the construction in intensional type theory. For readability purposes, we make only explicit in this section the key coherence conditions of the construction. Other cases of equality reasoning would have to be made explicit to fully obtain a construction in intensional type theory, but these steps are standard enough to be omitted at this stage. See section V.6 for the details.

The need for transport along a proof of commutation of restr frame in the definition of restr layer is made explicit in table 4', where the arrow over coh frame indicates the direction of rewrite.

restr n,p,p≤q≤n-1 frame,ϵ,q {D : νSet <n } (d : frame n,p (D))

: frame n-1,p (D.1)

restr n,0 frame,ϵ,q D * ≜ * restr n,p ′ +1
frame,ϵ,q D (d, l) ≜ (restr n,p ′ frame,ϵ,q (d), restr n,p ′ layer,ϵ,q-1 (l))

restr n,p,p≤q≤n-2 layer,ϵ,q {D : νSet <n } {d : frame n,p (D)} (l : layer n,p (d))

: layer n-1,p (restr n,p frame,ϵ,q+1 (d))

restr n,p layer,ϵ,q

D d l ≜ λω.( ------------→ coh n,p frame,ϵ,ω,q,p (d)(restr n-1,p painting,ϵ,q (D.2)(lω)))
restr n,p,p≤q≤n-1 painting,ϵ,q

(D : νSet <n ) (E : νSet =n (D)) (d : frame n,p (D)) (c : painting n,p (E)(d))
:

painting n-1,p (D.2)(restr n,p frame,ϵ,q+1 (d))

restr n,p,p=q painting,ϵ,q

D E d (l, _) ≜ lϵ restr n,p,p<q painting,ϵ,q D E d (l, c)
≜ (restr n,p layer,ϵ,q (l), restr n,p+1 painting,ϵ,q (E)(c))

Table 4': q-th projection of restr, or faces

coh n,p,p≤r≤q≤n-2 frame,ϵ,ω,q,r {D : νSet <n } (d : frame n,p (D)) : restr n-1,p frame,ϵ,q (restr n,p frame,ω,r (d)) = restr n-1,p frame,ω,r (restr n,p frame,ϵ,q+1 (d)) coh n,0 frame,ϵ,ω,q,r D * ≜ refl( * ) coh n,p ′ +1 frame,ϵ,ω,q,r D (d, l) ≜ (coh n,p ′ frame,ϵ,ω,q,r (d), coh n,p ′ layer,ϵ,ω,q,r (l))
coh n,p,p<r≤q≤n-2 layer,ϵ,ω,q,r (D : νSet <n ) {d : frame n,p (D)} (l : layer n,p (d))

:

------------→ coh n,p frame,ϵ,ω,q,r (d)(restr n-1,p layer,ϵ,q (restr n,p layer,ω,r (l))) = restr n-1,p layer,ω,r (restr n,p layer,ϵ,q+1 (l))

coh n,p layer,ϵ,ω,q,r D d l ≜

λθ.( --------------→ coh2 n,p frame,ϵ,ω,θ,q,r (d))(ap ( -------------------------→ coh n-1,p frame,ω,θ,r,p (restr n,p frame,ϵ,q+2 (d)))) (ap ( ----------------------→ restr n-1,p frame,ω,r (coh n,p frame,ϵ,θ,q+1,p ))) coh n-1,p painting,ϵ,ω,q-1,r-1 (D.2)(l θ )

coh n,p,p≤r≤q≤n-2 painting,ϵ,ω,q,r

(D : νSet <n ) (E : νSet =n (D)) (d : frame n,p (D)) (c : painting n,p (E)(d)) : ------------→ coh n,p
frame,ϵ,ω,q,r (d)(restr n-1,p painting,ϵ,q (D.2)(restr n,p painting,ω,r (E)(c))) = restr n-1,p painting,ω,r (D.2)(restr n,p painting,ϵ,q+1 (E)(c))

coh n,p,p=r painting,ϵ,ω,q,r D E d (l, _) ≜ refl(restr n-1,p painting,ϵ,q-1 (D.2)(lϵ)) coh n,p,p<r painting,ϵ,ω,q,r D E d (l, c) ≜ (coh n,p layer,ϵ,ω,q,r (l), coh n,p+1 painting,ϵ,ω,q,r (E)(c))

Table 5': Commutation of q-th projection and r-th projection, or coherence conditions

The proof of coh frame itself requires making explicit several rewrites which were invisible in extensional type theory. The commutation of restr layer lives in a type referring to coh frame , so we need a transport along the commutation of restr frame in the statement of coh layer . The proof of coh layer is the most involved proof of the construction, as it requires a higher-dimensional coherence condition, coh2 frame , whose exact formulation is as follows.

coh n,p frame,ω,θ,r,p (restr n,p frame,ϵ,q+2 (d)) • ap restr n,p frame,ω,r (coh n,p frame,ϵ,θ,q+1,p (d)) • coh n,p frame,ϵ,ω,q,r (restr n,p frame,θ,p (d)) = ap restr n,p frame,θ,p (coh n,p frame,ϵ,ω,q+1,r+1 (d)) • coh n,p frame,ϵ,θ,q,p (restr n,p frame,ω,r+1 (d)) • ap restr n,p frame,ϵ,q (coh n,p frame,ω,θ,r,p (d))

where ap applies a function on two sides of an equality, and • is transitivity of equality. This property of equality proofs holds in HSet, and since our construction is done in HSet, the term is trivially discharged. Notice that each restr layer in the type of coh layer is hiding a coh frame rewrite: this makes a sum total of three coh frame rewrites on the left-hand side, and two coh frame rewrites on the right-hand side. In the proof term of coh layer , coh painting has one coh frame rewrite on its left-hand side. This, combined with the two terms of the form ap coh frame , matches our expectation of three coh frame on the left-hand side, and two coh frame on the right-hand side. Then, coh2 frame can be seen as expressing the commutation of these coh frame terms.

Finally, let us explain coh painting . The base case p = r is the key case of the commutation of restr frame , when one of the restr painting collapses, and the remaining equation holds trivially. The case of p < r follows the structure of restr painting by induction.

If we were not working in HSet, but in HGpd we would need to prove one more higher-dimensional coherence, and if we were working in Type, we would need to prove arbitrarily many higher-dimensional coherences. Here, HGpd is the subset of types A such that for all x and y in A, x = y is in HSet. See [START_REF] Herbelin | A dependently-typed construction of semi-simplicial types[END_REF][START_REF] Altenkirch | Extending homotopy type theory with strict equality[END_REF][START_REF] Kraus | Internal ∞-categorical models of dependent type theory : Towards 2LTT eating HoTT[END_REF] for a discussion on the need for recursive higher-dimensional coherence conditions in formulating higher-dimensional structures in type theory.

V.4 Well-foundedness of the construction

Since the construction shown in the previous sections is by induction on n, and dependencies are on lower n and p < n, one would imagine formalizing this using well-founded induction in dependent type theory. We initially tried this approach, and had terms dependent on the proofs of the case distinction that n ′ ≤ n implies n ′ < n or n ′ = n, but these proofs did not come with enough definitional properties to be usable in practice. Hence, we chose a different route: in practice, since restr n frame depends on frame n and frame n-1 , while coh n frame depends on frame n , frame n-1 , and frame n-2 , we only need to keep track of three consecutive dimensions. Hence, what we build by induction at level n, is a structure made not only of the definitions shown in the tables 3, 4', and 5', but also of frame, layer, painting at levels n -1 and n -2, as well as restr frame , restr layer , and restr painting at level n -1, together with helper equations.

V.5 Dependencies in inequality proofs

The entire construction relies on inequalities over natural numbers, and we use two different definitions of ≤ addressing different concerns in our formalization. In order to build our first variant, we use an intermediate "recursive definition" phrased as: Here, SProp is a definitionally proof-irrelevant impredicative universe morally f living at the bottom of the universe hierarchy [START_REF] Gilbert | Definitional proofirrelevance without K[END_REF]. By placing the definition in SProp, we have definitional equality of inequality proofs. However, for the purpose of unification, this definition does not go far enough. Consider the unification problems: leR_trans ?p leR_refl = ?p leR_trans leR_refl ?p = ?p where leR_trans is transitivity, leR_refl is reflexivity, and ?p is an existential variable. These two problems definitionally hold in SProp, but equating them does not solve the existential variable. For unification to be useful in solving existential variables, we present our first variant of ≤, which we dub as the "Yoneda variant": Definition leY n m := forall p, leR p n -> leR p m.

This definition is an improvement over leR since reflexivity is now definitionally the neutral element of transitivity, and associativity of transitivity also holds definitionally. Although it significantly eases our proof, there are some instances where unification is unable to solve the existential variables, and we have to provide them explicitly.

The second variant of ≤, the "inductive variant", is phrased as:

  frame n,p (D) ≜ Σa n : (. . . (Σ * : unit. layer n,0 (D)) . . .). layer n,p-1 (D) painting n,p (D) ≜ Σl p : layer n,p (D). (. . . (Σl n : layer n,n-1 (D). D.tl) . . .)

  frame n,p (D) ≜ Σd : (. . . (Σ * : unit. layer n,0 (D)( * )) . . .). layer n,p (D)(d) painting n,p (D)(d) ≜ Σl p : layer n,p (D)(d). (. . . (Σl n : layer n,n-1 (D)(d, l p , . . . , l n-1 ). D.tl(d, l p , . . . , l n )) . . .)

  layer n,p (D)(d) ≜ painting n-1,p (D.hd)(restr n,p frame,L,p (d)) × painting n-1,p (D.hd)(restr n,p frame,R,p (d))

V. 3

 3 FROM EXTENSIONAL TO INTENSIONAL TYPE THEORY 11/ 15

Fixpoint

  leR (n m : nat) : SProp := match n, m with | O, _ => STrue | S n, O => SFalse | S n, S m => leR n m end.

Table 1 :

 1 Main definition

	V.1 THE CONSTRUCTION IN INFORMAL TYPE THEORY

Σl : layer n,p (d). painting n,p+1 (E)(d, l)

Table 3 :

 3 frame, layer, and painting

restr n,p,p≤q≤n-1 frame,ϵ,q

Table 5 :

 5

	V.2 INTUITION FOR OUR FORMAL CONSTRUCTION

Commutation of q-th projection and r-th projection, or coherence conditions

f In Coq ([START_REF]The Coq Reference Manual[END_REF]), it is however a stand-alone universe unrelated to the universe hierarchy.

13/ 15

Inductive leI : nat -> nat -> Type := | leI_refl n : n <~n | leI_down {n p} : p.+1 <~n -> p <~n where "n <~m" := (leI n m) : nat_scope.

Compared to leY, leI has no proof-irrelevance properties. This definition is specially crafted for painting, where we have to reason inductively from p ≤ n to n. In our usage, we have lemmas leY_of_leI and leI_of_leY in order to equip leY with the induction scheme of leI. The resulting induction scheme has computational rules holding propositionally.

V.6 Groupoid properties of equality and basic type isomorphisms

The construction relies on groupoid properties of equality which are left implicit in table 5'. The use of the equivalence between u = v and Σ(p : u.hd = v.hd).(u.tl = v.tl) for u and v in a Σ-type is left implicit in the same table. Also implicit is the use of the equivalence between f = g and Πa : A. f (a) = g(a) for f and g in Πa : A. B, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.

As a final remark, note that as a consequence of η-conversion for finite enumerated types, the requirement of functional extensionality disappears when ν is finite. However, this is a conversion which Coq does not implement, and the alternative would be to replace Πa : ν. B by a "flat" iterated product B(1) × B(2) × . . . × B(ν).

VI Future work

The construction could be extended with degeneracies as well as with permutations [START_REF] Grandis | Cubical sets and their site[END_REF]. Dependent ν-sets could also be defined, opening the way to construct Π-types and Σ-types of ν-sets. A ν-set of ν-sets representing a universe could also be defined as sketched in a talk at the HoTT-UF workshop for the bridge case ( [START_REF] Herbelin | Investigations into syntactic iterated parametricity and cubical type theory[END_REF]). More generally, we believe these lines of work would eventually provide alternative models to parametric type theories [START_REF] Nuyts | Parametric quantifiers for dependent type theory[END_REF][START_REF] Cavallo | Internal Parametricity for Cubical Type Theory[END_REF] where equality of types, now a family rather than the total space of a fibration, is not only definitionally isomorphic to bridges [START_REF] Bernardy | A presheaf model of parametric type theory[END_REF], but definitionally the same as bridges.

By equipping the universe construction with a structure of equivalences, as suggested along the lines of [START_REF] Altenkirch | Towards a cubical type theory without an interval[END_REF], we also suspect the construction to be able to serve as a basis for syntactic models of various versions of cubical type theory [BCH13, CCHM18, ABC + 21], saving the detour via the fibered approach inherent to usual presheaf models. In particular, we conjecture being able to justify univalence holding definitionally. Our approach would also firmly ground cubical type theory in iterated parametricity.

Another direction for future work is to give a general definition of presheaf in indexed form over a direct category, and to show the equivalence with the standard definition of presheaf.


Fabricio Benevides

Jean-Claude Bermond

Hicham Lesfari

Nicolas Nisse

Minimum lethal sets in grids and tori under 3-neighbour bootstrap percolation *

Let r ≥ 1 be any non negative integer and let G = (V, E) be any undirected graph in which a subset D ⊆ V of vertices are initially infected. We consider the process in which, at every step, each non-infected vertex with at least r infected neighbours becomes infected and an infected vertex never becomes non-infected. The problem consists in determining the minimum size s r (G) of an initially infected vertices set D that eventually infects the whole graph G. This problem is closely related to cellular automata, to percolation problems and to the Game of Life studied by John Conway. Note that s 1 (G) = 1 for any connected graph G. The case when G is the n × n grid, G n×n , and r = 2 is well known and appears in many puzzle books, in particular due to the elegant proof that shows that s 2 (G n×n ) = n for all n ∈ N. We study the cases of square grids, G n×n , and tori, T n×n , when r ∈ {3, 4}. We show that s 3 (G n×n ) = n 2 +2n+4 3 for every n even and that n 2 +2n 3 ≤ s 3 (G n×n ) ≤ n 2 +2n 3 + 1 for any n odd. When n is odd, we show that both bounds are reached, namely s 3 (G n×n ) = n 2 +2n 3

if n ≡ 5 (mod 6) or n = 2 p -1 for any p ∈ N * , and s 3 (G n×n ) = n 2 +2n 3 + 1 if n ∈ {9, 13}. Finally, for all n ∈ N, we give the exact expression of s 3 (T n×n ).

Introduction

Originally developed by von Neumann after a suggestion of Ulam, cellular automata are a dynamical system defined over graphs endowed with some homogeneous and local update rules. The notion of bootstrap percolation is an example of a cellular automaton which has been extensively investigated by mathematicians, physicists, computer scientists and sociologists, among others. For further applications to several other areas, we refer the reader to the survey article by Adler and Lev [START_REF] Adler | Bootstrap percolation: visualizations and applications[END_REF], and the references therein.

Several variants of classical bootstrap percolation on graphs have been considered. The particular model we are studying belongs to the class of r-neighbour bootstrap processes (r ≥ 1). It was first introduced by Chalupa, Leath, and Reich [START_REF] Chalupa | Bootstrap percolation on a bethe lattice[END_REF] as a monotone version of the Glauber dynamics in ferromagnetism.

Let r ≥ 1 be a given integer and G a finite graph whose vertices (usually called sites in the context of percolation) can be in one of two states: healthy or infected. An initial set of infected nodes is given. At any step, any healthy vertex with at least r infected neighbours becomes infected, while infected vertices remain infected forever. The parameter r reflects at which extent sites resist to the infection spread. Note that the term bootstrap percolation is sometimes used with the implicit assumption that the initial set of vertices infected is random. In this paper we consider the same model but use a deterministic initial set.

An initial set of infected vertices is called lethal if at the end of the process all the vertices are infected. A problem widely considered in the literature consists in determining the minimum size of a lethal set denoted by s r (G). (Knowing this value, for example, plays certain starting role in the study of the probability for a random initial set to be lethal).

Related work. Lethal sets have been considered in the literature with various names according the domain of applications. In [CDP + 11, DJR09], they are called irreversible r-conversion sets and infected vertices are called vertices in state 1. In the area of viral marketing, a lethal set is called a (perfect) target set and infected vertices are called active (see [CHY13, CHL + 13]). In [FLL + 04], lethal sets are called "irreversible dynamos (dynamic monopolies)" and infected vertices black or faulty (stemming from the distributed computing field). Note that non-irreversible dynamos have been widely investigated (see [START_REF] Peleg | Local majorities, coalitions and monopolies in graphs: a review[END_REF]).

Computing exactly s r (G) is NP-hard ([CDP + 11, Che09, DJR09] and the hardness result holds even when r = 2 and G has maximal degree ∆, where ∆ is a constant not depending on the size of G (see [START_REF] Chen | On the approximability of influence in social networks[END_REF]). The parameter s r (G) has been studied for several families of graphs including trees [CDP + 11, DJR09, Rie12], d-dimensional grids [BB06, BP98, PS20], chordal graphs [BEPR19, CDP + 11, CHL + 13], hexagonal grids [START_REF] Spence | Dynamic monopolies and feedback vertex sets in hexagonal grids[END_REF], honeycombs graphs [START_REF] Chiang | Target set selection problem for honeycomb networks[END_REF], hypercubes [START_REF] Balogh | Bootstrap percolation on the hypercube[END_REF][START_REF] Morrison | Extremal bounds for bootstrap percolation in the hypercube[END_REF], expanders [START_REF] Coja-Oghlan | Contagious sets in expanders[END_REF], random regular graphs [START_REF] Guggiola | Minimal contagious sets in random regular graphs[END_REF].

Cases of grids and tori. In particular, the most known case is the square grids G n×n with r = 2 as it appears as a popular puzzle regularly in newspapers and is referenced in puzzles books [START_REF] Winkler | Mathematical puzzles: a connoisseur's collection[END_REF][START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF][START_REF] Levitin | Algorithmic puzzles[END_REF]. According to [START_REF] Winkler | Mathematical puzzles: a connoisseur's collection[END_REF], the problem appeared for the first time in the Soviet magazine Kvant around 1986. The value s 2 (G n×n ) = n can be proved with the elegant perimeter argument. Our interest to the problem was revived, in fact, due to a problem proposed in the french newspaper "Le Monde" (Problem 1141, entitled "Le jeu de la viralité", April 2020) in honor to John Conway (who just passed away). This leads us to study the problem of determining the value s 3 (G n×n ) (see examples for small grids in Figure 1. In addition to the formal proofs given later, the reader may verify that these sets, and all constructions throughout the paper, are actually lethal using the software Golly1 ). To the best of our knowledge this problem was considered first in [START_REF] Gabor | Disease processes and bootstrap percolation[END_REF]. The result appears also in [START_REF] Balogh | Random disease on the square grid[END_REF]. In [START_REF] Gabor | Disease processes and bootstrap percolation[END_REF] it is proven that (n 2 + 2n)/3 ≤ s 3 (G n×n ) ≤ (n 2 + 4n)/3 + O(1). The lower bound uses also the perimeter argument. In [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF] (Problem 65, pages 171-172) Bollobás gave the same lower bound for n odd, but a slightly better one for n even. He also proves that for n ≡ 2 (mod 6) the lower bound is attained and in that case s 3 (G n×n ) = (n 2 + 2n + 4)/3 (see Figure 1(f) for n = 8). The case of the grid was also considered in [START_REF] Jr | Irreversible k-threshold processes: Graphtheoretical threshold models of the spread of disease and of opinion[END_REF] where they claim that s 3 (G n×n ) ≤ n 2 /3 + (7n + 55)/12, but the known lower bound of (n 2 -2n + 2)/3 [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF][START_REF] Gabor | Disease processes and bootstrap percolation[END_REF] is larger than than their upper bound for n large enough.

The problem for tori T m×n was considered and solved in [Bol06, FLL + 04, Pet97, Win03] for r = 2, where s 2 (T m×n ) = n+m 2 -1. For the case r = 3, it has been proved that (mn + 1) + 1)/3 ≤ s 3 (T m×n ) ≤ max{ m/3 (n + 1), n/3 (m + 1)} [FLL + 04]. Finally, in [START_REF] Jr | Irreversible k-threshold processes: Graphtheoretical threshold models of the spread of disease and of opinion[END_REF], exact expressions of s 4 (G m×n ) and s 4 (T m×n ) are given.

Other related problems have been considered in the literature like finding the size of a largest inclusion-minimal lethal set [START_REF] Morris | Minimal percolating sets in bootstrap percolation[END_REF][START_REF] Riedl | Largest minimal percolating sets in hypercubes under 2-bootstrap percolation[END_REF]. The speed of convergence was also considered in the square grid (see [START_REF] Benevides | On slowly percolating sets of minimal size in bootstrap percolation[END_REF][START_REF] Benevides | Maximum percolation time in twodimensional bootstrap percolation[END_REF]). Our contributions. In this paper, we study the contamination process in square grids G n×n and square tori T n×n . The tools developed here can be used to get results for non square grids and tori. In Section 2, we formally define the problem and recall the results obtained for r = 2, 4 and some known results for r = 3 that we use throughout the paper. Our main result is the following theorem that deals with an almost tight bound of s 3 (G n×n ).

Theorem 1 Let n ∈ N * . Let LB n = n 2 +2n 3 if n is odd and LB n = n 2 +2n+4 3 if n is even. • s 3 (G n×n ) = LB n if n is even or if n ≡ 5 mod 6 or if n = 2 p -1; • LB n ≤ s 3 (G n×n ) ≤ LB n + 1 if n is odd; • s 3 (G n×n ) = LB n + 1 if n ∈ {9, 13}.
Section 3 is devoted to the proof of the first two items of Theorem 1. In Section 4, we prove the last item of Theorem 1. For the values n = 9 and 13, we prove that the lower bound is not tight using a Linear Program. For n = 9, we also give a combinatorial proof. Then, Section 5 is devoted to settle the problem when r = 3 in tori:

Theorem 2 For every n ≥ 3, s 3 (T n×n ) = n 2 +1 3 .

We conclude in Section 6 by describing several open questions.

Preliminaries

Notations and Problem statement

Let G = (V, E) be a graph. For a vertex v ∈ V , N (v) = {u ∈ V | {u, v} ∈ E} is the neighbourhood of v and d(v) = |N (v)| is the degree of v.
The 2-dimensional (square) grid graph with n rows and n columns is denoted by G n×n . Its vertex set is defined by vertex (i,j) has degree 4. The corners are the vertices with degree at most 2, that is, the vertices (1, 1), (1, n), (n, 1) and (n, n). The border B is the set of vertices with degree at most 3.

V (G n×n ) = {(i, j) | 1 ≤ i ≤ n, 1 ≤ j ≤ n}. Two vertices (i, j) and (i , j ) are adjacent if and only if |i -i | + |j -j | = 1. If 1 < i, j < n,
For n ≥ 3, let also T n×n be the torus with vertex-set {(i, j) | i ∈ Z n and j ∈ Z n }, where Z n denotes the set of integers modulo n denoted 0, 1, . . . , n -1. Vertex (i, j) is adjacent to the 4 vertices (i -1, j), (i + 1, j) (i, j -1) and (i, j + 1).

Given a graph G and a natural number r ∈ N * , we consider the following deterministic process (known as r-neighbour bootstrap percolation) that models the spread of an infection in G. Let D 0 = D be a subset of initially infected vertices and for each step t ≥ 1, let

D t = D t-1 ∪ {v ∈ V : |N (v) ∩ D t-1 | ≥ r}.
For a set D ⊂ V (G), let D = ∞ t=0 D t be the closure of D, i.e., the set of eventually infected vertices in the process that was started from D. A configuration is a pair (G, D) that consists of a graph G together with the subset D of its vertices that are initially infected. Abusing the notation, we call the size of the configuration as the size |D| of the set D.

Any set D ⊆ V is said lethal if D = V . Similarly, a configuration (G, D) is lethal if D is a lethal set. Let s r (G) be the minimum size of a lethal set in G. Since V = V , s r (G) is always well defined. A lethal set (resp. a lethal configuration) is optimal if it is of size s r (G). Note that s 1 (G) = 1 for every connected graph G.

The main goal of this paper is to investigate s 3 (G n×n ) and s 3 (T n×n ), i.e., focusing on square grids and tori for r = 3. Let us first deal with the cases r ∈ {2, 4}.

Cases r ∈ {2, 4}

For completeness, we first precisely recall the known results when r = 2 and give exact results in the case when r = 4.

The following result for the grid G n×n and r = 2 can be considered as folklore and appeared in many books with puzzles [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF][START_REF] Levitin | Algorithmic puzzles[END_REF][START_REF] Winkler | Mathematical puzzles: a connoisseur's collection[END_REF]. The lower-bound is proved using an elegant perimeter argument and an optimal lethal set is obtained by taking the n vertices of the diagonal.

Theorem 3 ([Bol06, LL11, Win03]) Let n ≥ 1, then s 2 (G n×n ) = n.
The result for the torus can be found in Problem 66, page 173 in [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF] and in [FLL

+ 04, Win03]. Theorem 4 ([Bol06, FLL + 04, Win03]) Let n ≥ 1, then s 2 (T n×n ) = n -1.
The case r = 4 was considered in [START_REF] Balogh | Random disease on the square grid[END_REF] where it is only stated that s 4 (G n×n ) ∼ n 2 /2, and has been completely solved in [START_REF] Jr | Irreversible k-threshold processes: Graphtheoretical threshold models of the spread of disease and of opinion[END_REF].

Proposition 5 ([DJR09]

) For every n ≥ 3, we have

• s 4 (G n×n ) = n 2 +4n-4 2 . • s 4 (T n×n ) = n n+1 2 .
2.3 Known results on s 3 (G n×n ) that are used throughout this paper

We first present two properties that we will use after.

Property 6 When r = 3, every lethal set in G n×n contains every corner.

Proof. Let u be a corner of G n×n and let D be a lethal set. Since u has degree at most 2 and requires at least 3 neighbours to be infected, then u ∈ D.

The next property states that, for every two adjacent vertices on the border, at least one must be initially infected in order to eventually infect the whole grid.

Property 7 Let u, v be two adjacent vertices in B of G n×n and let D be a lethal set for r = 3, then D ∩ {u, v} = ∅.

Proof. Let D be a lethal set of G n×n . For purpose of contradiction, let us assume that there are two adjacent vertices u and v of the border (so they have degree at most 3) that are not in D. Then, the first vertex to be contaminated in {u, v} would have at most two contaminated neighbours before being infected, a contradiction.

The following lower bound has been proved in [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF] using the perimeter argument and noting that, for n even, there are four pairs of adjacent infected vertices in B. In particular, the notation LB n defined below will be used throughout the paper. We provide for completeness a sketch of the proof.

Theorem 8 (Problem 65, pages 171-172 in [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF]) Let n ∈ N * . It holds that:

s 3 (G n×n ) ≥ LB n =      n 2 +2n 3 if n is odd, n 2 +2n+4 3
if n is even.

Proof. We rephrase the elegant perimeter's argument used in [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF]. Each vertex has a perimeter 4 and so the initial perimeter of a lethal set is at most 4|D|. In the process of infection, each time a new vertex is infected, the perimeter decreases by at least 2 and the final perimeter is 4n. Hence, we get 4|D| -2(n 2 -|D|) ≥ 4n and so |D| ≥ n 2 +2n 3 . If n is even, by Properties 6 and 7, there are on each side of the border B a pair of adjacent infected vertices. Therefore, the initial perimeter is at most 4|D| -8 and so we get |D| ≥ n 2 +2n+4 3 . This allows to prove the following corollary that we extensively use later.

Corollary 9 Let n ∈ N. LB n+3 -LB n =          2n + 3 when n ≡ 0, 4 (mod 6) 2n + 4 when n ≡ 2 (mod 6) 2n + 6 when n ≡ 5 (mod 6) 2n + 7 when n ≡ 1, 3 (mod 6) LB n+6 -LB n = 4n + 16.
In [START_REF] Bollobás | The art of mathematics: Coffee time in Memphis[END_REF], Bollobás proved that the lower bound LB n is indeed reached in the case n ≡ 2 (mod 6) (see Figure 1(f) for n = 8). We rephrase his result as follows by specifying an extra property (useful later) of some optimal lethal sets.

Theorem 10 ([Bol06]) Let n ≡ 2 (mod 6), then s 3 (G n×n ) = LB n = n 2 +2n+4 3
. Furthermore, there exists an optimal lethal set of G n×n containing the vertices (1, n -1), (2, n), (n -1, 1), and (n, 2).

Various constructions and optimal results

In this section, we present several ways to use (lethal or not) configurations for smaller grids in order to obtain new lethal configurations for larger grids. Each of the different tools that we propose allow us to prove Theorem 1 (but its last item that is proved in next Section). (1, n + 1) and (n + 1, 1), plus the vertices (n + 2, 2j + 2) for every 0 ≤ j ≤ n/2 and (n + 3, 2j + 1) for every 0 ≤ j ≤ n/2 + 1. Symmetrically, D contains the vertices (2j +2, n+2) for every 0 ≤ j ≤ n/2-1 and (2j +1, n+3) for every 0 ≤ j ≤ n/2. See Figure 2 for an illustration. Hence, we have 2n + 6 infected vertices in the last (bottommost) 3 rows and last (rightmost) 3 columns. Overall, |D | = |D| + 2n + 4. Now let us prove that D is a lethal set. The vertices (1, n) and (n, 1) will become infected at the first step because they have 3 infected neighbours initially. Therefore, every vertex of the subgrid G n×n will become infected (as D is a lethal set). At the first step, all the vertices of rows and columns n + 2 and n + 3 are also infected plus the vertices (n + 1, 2) and (2, n + 1). From these last two vertices the infection propagates along row n + 1 and column n + 1, until it reaches the vertex (n + 1, n + 1).

By Corollary 9, we get:

Corollary 12 Let D be a lethal set for G n×n such that {(1, n -1), (2, n), (n -1, 1), (n, 2)} ⊆ D. If n ≡ 0 or 4 (mod 6), then s 3 (G (n+3)×(n+3) ) -LB n+3 ≤ |D| -LB n + 1. If n ≡ 2 (mod 6), then s 3 (G (n+3)×(n+3) ) -LB n+3 ≤ |D| -LB n .
Theorem 13 Let n ≡ 5 (mod 6). Then, s 3 (G n×n ) = LB n = n 2 +2n+1 3 .

Proof.

By Theorem 10, since n -3 ≡ 2 (mod 6), s 3 (G (n-3)×(n-3) ) = LB n-3 . Moreover, there exists an optimal lethal configuration of G (n-3)×(n-3) containing the vertices (n -1, 1), (n, 2), (1, n -1), (2, n). The result follows from the Corollary 12.

3.2 From n even to n + 6 (even) and optimality for every n even Proposition 14 Let n be even. If D is a lethal set in G n×n such that {(1, n -1), (2, n), (n -1, 1), (n, 2)} ⊆ D, then there exists a lethal configuration (G (n+6)×(n+6) , D ) with size |D | = |D| + 4n + 16 and such that {(1, n + 5), (2, n + 6), (n + 5, 1), (n + 6, 2)} ⊆ D .

Proof. From the configuration (G n×n , D), we first construct the configuration (G (n+3)×(n+3) , D ) as in Proposition 11 and then the configuration (G (n+6)×(n+6) , D ) as follows. The restriction of D to the subgrid G n+3×n+3 consisting of the first (topmost) n + 3 rows and first (leftmost) n + 3 columns of G (n+6)×(n+6) will be the set D minus the vertex (n + 3, 3). Then, D contains the following vertices: (n + 4, 2) and (n + 4, 4), (n + 5, 1) plus the vertices (n + 5, 2j + 1) for every 2 ≤ j ≤ n/2 + 2 (note that (n + 5, 3) is not infected) and the vertices (n + 6, 2j + 2) for every 0 ≤ j ≤ n/2 + 2. In addition, D contains the vertices (2j + 1, n + 5) and (2j + 2, n + 6) for every 0 ≤ j ≤ n/2 + 1. Finally, D contains the two corners (n + 6, 1) and (1, n + 6). See Now let us prove that D is a lethal set. The vertices (1, n) and (n, 1) will become infected at the first step because they have 3 infected neighbours initially. Then, every vertex of the subgrid G n×n will become infected (as D is a lethal set). At the first step, all the vertices of columns n + 2, n + 3, n + 5 and n + 6 become infected except (n + 4, n + 2), (n + 4, n + 3) and all the vertices of rows n + 2, n + 3, n + 5 and n + 6 except (n + 2, 3), (n + 3, 3), (n + 5, 3), (n + 6, 3). Vertices (n + 1, 2), (2, n + 1),(n + 1, 2) and (n + 4, 5) are also infected at step 1. From the vertex (2, n + 1) the infection propagates along column n + 1 until it reaches the vertex (n + 1, n + 1) and then along row n+1 until it reaches vertex (n+1, 4). Then vertices (n+1, 3), (n+2, 3), (n+ 3, 3), (n + 4, 3), (n + 5, 3), (n + 6, 3) become infected. From the vertex (n + 4, 5) the infection propagates along row n + 4 until it reaches the vertex (n + 4, n + 4) and then along column n + 4 until it reaches vertex (1, n + 4). See an example in Figure 4.

Remark:

We can do the proof by deleting from D instead of vertex (n + 3, 3) any vertex (n + 3, 2j 0 + 1) with 1 ≤ j 0 ≤ n/2. Then D should contain in row n + 4 the infected vertices: (n + 4, 2j 0 ) and (n + 4, 2j 0 + 2) and in row n + 5 all the vertices (n + 5, 2j + 1) for every 0 ≤ j ≤ n/2 + 2 except vertex (n + 5, 2j 0 + 1). That might be useful to diminish the propagation time.

Theorem 15 Let n be even. Then, s 3 (G n×n ) = LB n . Moreover, there exists an optimal lethal set which contains the vertex (2, 2).

Proof. The theorem is true for n = 2, 4, 6, in which cases, optimal grids can be constructed directly (for n = 4 and 6, see Figure 1). Then, the theorem follows by induction on n (even) using Proposition 14 and Corollary 9. The fact that all the grids contain the vertex (2, 2) will be useful for the proof of the existence of optimal tori (s 3 (T n×n ) = n 2 +1 3 ).

Theorem 16 Let n ≡ 1 or 3 (mod 6). Then, s 3 (G n×n ) ≤ LB n + 1. Moreover, there exists a lethal set of size LB n + 1 which contains the vertex (2, 2). In the left part, initially infected (resp., not infected) vertices are red (resp., white). In the right part, vertices infected at step 1 are in orange and those not infected at the end of step 1 are in white. To get optimal lethal sets for the grids with n even we should also have the corners infected and to get almost optimal for the grids with n odd we should also have the vertex (n, 3) infected. We give now another tool which, while rather simple, allows us to identify a new class of grids (namely, n = 2 p -1) with odd side where the lower bound is tight.

For any configuration (G n×n , D), let (G (2n+1)×(2n+1) , D ) = H(G n×n , D) be the configuration defined as follows. The restriction of D to each of the four connected components obtained from G (2n+1)×(2n+1) by removing its central row and central column (i.e., the (n + 1) th row and (n + 1) th column) is equal to D. Finally, D also contains the vertex (n + 1, n + 1). See Fig. 5 for an illustration.

Lemma 17 If (G n×n , D) is a lethal configuration, then H(G n×n , D) is a lethal configuration.
Proof. Since D is a lethal set for G n×n , each of the component of G (2n+1)×(2n+1) obtained by removing the central row and the central column will be infected independently. Finally, the central row and central column will be infected using the fact that every other vertex and the central one (n + 1, n + 1) are infected.

Definition 18 Let H 1 be the configuration that consists of the grid G 1×1 whose single vertex is infected. For every p > 1, let H p = H(H p-1 ).

Proposition 19 For every p ≥ 1, H p is an optimal lethal configuration for the grid G 2 p -1×2 p -1 with 4 p -1 3 vertices initially infected.

Proof. Since H 1 is clearly lethal, by induction on p and Lemma 17, then H p is lethal for all p. Let D p be the lethal set of H p , then |D p | = 4|D p-1 |+1 and as |D 1 |= 1, we get D p = 4 p -1 3 . Finally, the optimality comes from Theorem 8 that states that for n = 2 p -1, LB n = n(n+2)

3 = 4 p -1 3 .
Theorem 20 For every p ∈ N * , let n = 2 p -1. Then,

s 3 (G n×n ) = LB n = n(n+2) 3 .
4 The lower bound is not always tight

In the case when n is odd such that n ≡ 1, 3 (mod 6) and n = 2 p -1, it remains to decide whether s 3 (G n×n ) equals LB n or LB n + 1. The first two values which are undetermined yet are n = 9 and n = 13. For these values, we prove that the lower bound is not tight using a Linear Program. Finally, for n = 9, we also give a long combinatorial proof.

Useful properties of lethal sets

First, let us present one useful properties that must be satisfied by any lethal set (or more precisely by the complement of any lethal set) of a grid.

Property 21 Let D be a lethal set of the grid G n×n . Let H = V \ D. Then, H induces an acyclic subgraph whose every connected component has at most one vertex on the border.

Proof. For purpose of contradiction, let us first assume that H induces a subgraph containing a cycle C and let u be the first vertex of C contaminated by D. Then, when u becomes infected, it has at most two infected neighbours, a contradiction. Similarly, if H induces a subgraph that contains a path P (with at least two vertices) whose ends are in the border, then the first vertex to be infected in P would have at most 2 already infected neighbours, a contradiction.

Linear Program

We present a Mixed-Integer Linear Program (MILP) for computing s r (G) in any graph G. As initially described in section 2, we consider a step of the contamination process. That is, at every step, all non-infected vertices with at least r infected neighbours become infected. The question addressed in this section is as follows:

Instance : A graph G = (V, E), non-negative integers r and T .

Question : What is the minimum number s T r (G) of initially infected vertices such that the whole graph is contaminated in at most T steps? First, let c x,0 = 0 be a new variable expressing that we consider the new vertex x as non infected. Then, we consider the binary variables y e for e = {u, v} ∈ E(G ), defined as follows: y e = 1 if and only if c u,0 = 0 and c v,0 = 0 (i.e., y e = 1 if and only if e is an edge of H ).

y e + c u,0 + c v,0 ≥ 1 ∀e = {u, v} ∈ E(G ) (9) 2y e + c u,0 + c v,0 ≤ 2 ∀e = {u, v} ∈ E(G ) ( 10
)
y e ∈ {0, 1} ∀e = {u, v} ∈ E(G ) (11)
Then, to ensure that H is acyclic, we leverage upon an efficient formulation usually used to design a Linear Program for computing the Maximum Average Degree of a graph in polynomial time. To this end, we consider the real non-negative variables z e,u and z e,v for every e = {u, v} ∈ E(G ). Intuitively, each edge induced by H distributes a potential of one from each of its end-vertices, and H is acyclic if and only if no vertex receives a potential of at least one.

z e,u + z e,v = y e ∀e = {u, v} ∈ E(G ) (12) e ={w,v} w∈N (v) z e ,v < 1 ∀v ∈ V (G ) (13) z e,u , z e,v ≥ 0 ∀e = {u, v} ∈ E(G ) ( 14
)
Further optimizations. We also provided the MILP with lower and upper bounds on the expected solution. That is, we add constraints of the following form LB ≤ v∈V c v,0 ≤ U B for some given integers LB and U B. We note that the main purpose of the previous MILP is to determine whether the lower bound LB n is tight for the cases not covered by Theorem 1. Therefore, we added some specific constraints which reflect the properties of lethal sets of size LB n . For instance, when n ≡ 1 or 3 (mod 6), by Property 23 (proved in the next subsection) every such lethal set D does not contain two adjacent vertices and a vertex in V \ D cannot be surrounded by four vertices in D. In some cases, we also imposed some further restrictions (such as, in the case when n is odd, that the vertices in the border of the grids are precisely characterized if we expect a lethal set of size LB n ) or explicitly implemented branch and bound algorithms where we specified the values of some vertices.

Overall, the MILP (these LPs) allowed us to obtain best known solutions for every n up to 20 (but 19) and the solutions found helped us at the beginning of our research. So far, the case n = 19 is the smallest size that still resists to the MILP as it provided a solution with LB 19 + 1 vertices initially contaminated, but was not able to terminate when requiring a solution with LB 19 vertices. This is in contrast with the case when n = 13, where the MILP terminates certifying that there are no solutions using LB 13 vertices initially contaminated. In summary, our experiments based on the MILP allowed us as such to show that s 3 (G n×n ) = LB n + 1 for n ∈ {9, 13} (Proposition 22); but the MILP does not terminate for n = 19.

Proposition 22 s 3 (G n×n ) = LB n + 1 if n ∈ {9, 13}.
Proof. The upper bounds comes from Theorem 16. The fact that this is optimal results from the execution of the LP described in this section and that certified that no solutions with LB n vertices exist.

Combinatorial proof for n = 9

We now provide below an ad-hoc combinatorial proof that s 3 (G 9×9 ) = LB 9 + 1; but it seems quite tedious to generalize this proof already for n = 13. We first state a proposition which gives more properties of the vertices of D and V \ D when n ≡ 1 or 3 (mod 6) .

Property 23 Let n ≡ 1 or 3 (mod 6) and let D be a lethal set of size LB n = (n 2 + 2n)/3; then a) there are no two adjacent vertices in D, and b) a vertex in V \ D cannot have 4 neighbours in D.

Proof. We reconsider the proof of Theorem 8 with a more careful analysis. If two vertices of D are adjacent, their perimeter is 6 and not 8 and so the initial perimeter is at most 4|D| -2. So we get 4|D| -2 -2(n 2 -|D|) ≥ 4n and so |D| ≥ (n 2 + 2n + 1)/3 > LB n and that proves property a). If a vertex in V \ D has 4 neighbours in D, then when this vertex is infected the perimeter decreases by 4 and not 2. So in that case we get 4|D| -2(n 2 -|D|) -2 ≥ 4n and so |D| ≥ (n 2 + 2n + 1)/3 > LB n and that proves property b).

Proposition 24 We have s 3 (G 9×9 ) = LB 9 + 1 = 34.

Proof. The upper bounds come from Theorem 16. To prove the proposition, by Theorem 8, it is sufficient to show that there is no lethal set for G 9×9 with 33 vertices. Hence, for purpose of contradiction, let us assume that there exists a lethal set D of size 33 in the grid G 9×9 . The basic idea of the proof is mainly to use Properties 7, 21 and 23 in order to progressively show that some vertices are forced to belong to D (vertices in red in Figure 6) or to V \ D (vertices in yellow in Figure 6). There are few cases to be considered.

By Property 7 and 23,

D ∩ B = {(1, 1), (1, 3), (1, 5), (1, 7), (1, 9), (3, 9), (5, 9), (7, 9), (9, 9)
, (9, 7), (9, 5), (9, 3), (9, 1), (7, 1), (5, 1), (3, 1)}. Then by Property 23(a), (2, 3), (2, 5), (2, 7), (3, 8), (5, 8), (7, 8), (8, 7), (8, 5), (8, 3), (7, 2), (5, 2), (3, 2) are not in D. Then, Property 21 implies that (2, 2) ∈ D (otherwise there will the path (1, 2), (2, 2), (2, 1) in V \D); similarly (2, 8), (8, 2), (8, 8) ∈ D. So far, we may assume that D contains the vertices described in red and does not contain the ones in yellow as shown in Figure 6(a).

Let us now prove two claims very useful for the proof.

Claim 25 At least one vertex in each of the pairs {(2, 4), (2, 6)} {(4, 2), (6, 2)}, {(4, 8), (6, 8)} and {(8, 4), (8, 6)} belongs to D.

Proof of Claim. Suppose it is not true and that for example (2, 4) and (2, 6) are in V \ D. Then there will be the path (1, 4), (2, 4), (2, 5), (2, 6), (1, 6) in V \ D, contradicting Property 21.

Claim 26 For each pair {(2, 4), (4, 2)} {(6, 2), (8, 4)}, {(2, 6), (4, 8)} and {(6, 8), (8, 6)}, the two vertices of this pair have the same status (either both in D or both in V \ D). By Property 23(a), this implies that vertices (3, 4), (3, 6), (4, 7), (6, 7), (7, 6), (7, 4), (6, 3), (4, 3) are not in D. Then, vertices (3, 3), (3, 5), (3, 7), (5, 3), (5, 7), (7, 3), (7, 5), (7, 7) are not in D by Property 23(b). But, then there exists a 16-cycle (3, 3), (3, 4), (3, 5), (3, 6), (3, 7), (4, 7), (5, 7), (6, 7), (7, 7), (7, 6), (7, 5), (7, 4), (7, 3), (6, 3), (5, 3), (4, 3) in V \ D, a contradiction. ∈ D. But, then there is a 8-cycle in V \ D ((5, 3), (5, 4), (5, 5), (6, 5), (7, 5), (7, 4), (7, 3), (6, 3)), a contradiction.

Proof of

-Case (6, 2) / ∈ D (See Figure 6(f)). By Claim 26, (8, 4) / ∈ D. Hence (7, 3) ∈ D to avoid a path from (6, 1) to (9, 4) in V \ D. Then, by Property 23(a), (6, 3) and (7, 4) / ∈ D. Hence, (5, 3), (7, 5) ∈ D to avoid 4-cycles in V \ D, and (6, 4) ∈ D to avoid a path from (6, 1) to (9, 4) in V \ D. Moreover, by Property 23(a), (5, 4) and (6, 5) / ∈ D to avoid adjacent vertices in D. There are already 32 vertices in D and the single remaining (undetermined yet) vertex of D is not sufficient to break all 4-cycles in V \ D, a contradiction.

Tori

In this section, we focus on the square tori. We note that Property 21 proved for the grids holds for any graph. This property was used for tori in [FLL + 04] to prove the following lower bound: An upper-bound of n/3 (n + 1) for s 3 (T n×n ) is also given in [FLL + 04]. Note that it differs from the lower bound by a factor of order n (more precisely, n/3-1 if n ≡ 0 (mod 3), (2n-1)/3 if n ≡ 2 (mod 3) and n if n ≡ 1 (mod 3)). Here, we determine the exact value of s 3 (T n×n ) for every n ≥ 3, as given in Theorem 2.

Proposition 27 ([FLL + 04]) s 3 (T n×n ) ≥ LBT n = n 2 +1 3 . (a) n ≡ 3 [6] (b) n ≡ 1, 5 [6] (c) n ≡ 0 [6] (d) n ≡ 2, 4 [6]
Theorem 28 If n is odd, then s 3 (T n×n ) = LBT n .

Proof. As n is odd, n -1 is even. By Theorem 15, there exists a lethal configuration (G (n-1)×(n-1) , D) of size LB n-1 and such that (2, 2), ⊆ D. We build a lethal configuration (T n×n , D ) as follows.

• Let n ≡ 3 (mod 6). The restriction of D to the subgrid G (n-1)×(n-1) consisting of the last (bottommost) n -1 rows and last (rightmost) n -1 columns of G (n-1)×(n-1) will be the set D minus the corners (1, n). Moreover, D contains the vertex (0, 0) (see Figure 7 • Let n ≡ 1, 5 (mod 6). The restriction of D to the subgrid G (n-1)×(n-1) consisting of the last (bottommost) n -1 rows and last (rightmost) n -1 columns of G (n-1)×(n-1) will be the set D minus the three corners (1, n), (n, 1), (1, 1) and vertex (2, 2). Moreover, D contains the three vertices (0, 1), (1, 0) and (2, 1) (see Figure 7 We claim that D is lethal in both cases. For the first case, the infection reaches all the vertices of the subgrid G (n-1)×(n-1) except (1, n) as D is a lethal set. Then, it propagates along line 0 till (0, n) and so (1, n) becomes infected and then the infection propagates along column 0. For the second case, the infection reaches all the vertices of the subgrid G (n-1)×(n-1) ; indeed vertices (1, 1), (1, n), (2, 2), (2, 3), (n, 1) are infected thanks to (0, 1), (1, 0), (2, 1) and then vertex (1, 2) becomes infected. Then the infection propagates along column 0 till (n, 0) and so (0, 0) becomes infected. Finally the infection propagates along line 0 till (0, n).

Theorem 29 If n is even, then s 3 (T n×n ) = LBT n .

Proof.

• Let n ≡ 0 (mod 6). So n-1 ≡ 5 (mod 6). By Theorem 16, there exists a lethal set D in the grid G (n-1)×(n-1) of size LB n-1 . We construct a lethal configuration (T n×n , D ) as follows.

The restriction of D to the subgrid G (n-1)×(n-1) consisting of the last (bottommost) n-1 rows and last (rightmost) n -1 columns of G (n-1)×(n-1) will be the set D. Moreover, D contains the vertex (0, 0). (see Figure 7 • Let n ≡ 2, 4 (mod 6). So n -1 ≡ 1, 3 (mod 6). By Theorem 16, there exists a lethal set D in the grid G (n-1)×(n-1) of size LB n-1 + 1 containing vertex (2, 2). We construct a lethal configuration (T n×n , D ) as follows. The restriction of D to the subgrid G (n-1)×(n-1) consisting of the last (bottommost) n -1 rows and last (rightmost) n -1 columns of G (n-1)×(n-1) will be the set D minus the vertex (2, 2). Moreover, D contains the vertex (0, 0) (see Figure 7 Similarly to the case where n is odd, we can check that D is lethal in both cases.

Further Work

The first open problem2 would be to completely settle the question of determining s 3 (G n×n ) (either LB n or LB n + 1) for any undetermined n, i.e., for every odd n > 13 such that n ≡ 5 (mod 6) and n = 2 p -1. Note that the first undetermined value is n = 19 for which our Linear Program did not terminate. The next graph class to be considered would be d-dimensional grids for d > 2. Last but not least, it would be interesting to investigate further the question of the speed of the infection, i.e., determining optimal (in terms of size) lethal sets that infect the whole graph as fast (resp., as slow) as possible.

Figure 1 :

 1 Figure 1: Some instances of minimum lethal sets in G n×n when r = 3. The vertices are depicted as small squares. Initially infected (resp., not infected) vertices are red (resp., white).

3. 1

 1 From n even to n + 3 odd and optimality for n ≡ 5 (mod 6)Proposition 11 Let n be even. If D is a lethal set in G n×n containing the vertices (1, n -1), (2, n), (n -1, 1), and (n, 2), then there exists a lethal configuration (G (n+3)×(n+3) , D ) with size |D | = |D| + 2n + 4.

Figure 2 :

 2 Figure 2: Illustration of Proposition 11. The vertices are depicted as small squares (with most vertices inside G n×n as well as their status omitted). Initially infected (resp., not infected) vertices of D are red (resp., white). Orange vertices are the ones that are initially infected in D but not in D .

Figure 3 :

 3 Figure 3: Illustration of Proposition 14. The vertices are depicted as small squares (with most vertices inside G n×n as well as their status omitted). Initially infected (resp., not infected) vertices of D are red (resp., white). Orange vertices are the ones that are initially infected in D but not in D .

  Figures 3 for an illustration. Overall, |D | = |D | + 2n + 12 = D + 4n + 16.

  (a) Infection process at t = 0. (b) Infection process at t = 1.

Figure 4 :

 4 Figure 4: Construction for n = 30. Here we start from the optimal grid G 6×6 (depicted by a blue frame) obtained from the grid G 3×3 (Theorem 21) and apply the construction recursively.In the left part, initially infected (resp., not infected) vertices are red (resp., white). In the right part, vertices infected at step 1 are in orange and those not infected at the end of step 1 are in white. To get optimal lethal sets for the grids with n even we should also have the corners infected and to get almost optimal for the grids with n odd we should also have the vertex (n, 3) infected.

Figure 5 :

 5 Figure 5: Illustration of the configuration H(G n×n , D).

3. 3

 3 From n to 2n + 1 and optimality for n = 2 p -1

  Claim. For purpose of contradiction, let us assume by symmetry that (2, 4) ∈ D and (4, 2) / ∈ D (see Figure 6(b)). By Property 23(b), vertex (3, 3) / ∈ D (otherwise the vertex (3, 2) which belongs to V \ D will have 4 neighbours in D). Then, Property 21 implies that vertex (4, 3) ∈ D (otherwise V \ D would contain a 4-cycle). Moreover, by Claim 25, as (4, 2) / ∈ D, then (6, 2) ∈ D. Now, by Property 23(a), vertices (3, 4), (4, 4), (5, 3) and (6, 3) are not in D. Then, Property 21 implies (5, 4) ∈ D (since otherwise we will have in V \ D the 8-cycle (3, 2), (3, 3), (3, 4), (4, 4), (5, 4), (5, 3), (5, 2), (4, 2)). Then, by Property 23(a), we have (5, 5), (6, 4) / ∈ D. Then, by Property 23(b) (7, 3) / ∈ D (since otherwise (7, 2) would be a vertex

Figure 6 :

 6 Figure 6: Illustrations of Proposition 24 (n = 9). Red vertices are the one that are assumed to belong to the lethal set D of size 33, yellow vertices are assumed to belong to V \ D and white vertices are undetermined yet. Vertices (squares) surrounded by blue correspond to the hypotheses done in the different cases of the proof. Figure (a) is a configuration that is certain if |D| = 33. Figure (b) is the configuration obtained if (2, 4) ∈ D and (4, 2) / ∈ D and leads to a contradiction (Claim 26).Figure (c) corresponds to the first case and leads to a contradiction.Figure (d) corresponds to the second case.Figure (e) (resp., (f )) to the subcase (6, 2) ∈ D (resp. (6, 2) / ∈ D) leading to a contradiction in both subcases.

  Figure 6: Illustrations of Proposition 24 (n = 9). Red vertices are the one that are assumed to belong to the lethal set D of size 33, yellow vertices are assumed to belong to V \ D and white vertices are undetermined yet. Vertices (squares) surrounded by blue correspond to the hypotheses done in the different cases of the proof. Figure (a) is a configuration that is certain if |D| = 33. Figure (b) is the configuration obtained if (2, 4) ∈ D and (4, 2) / ∈ D and leads to a contradiction (Claim 26).Figure (c) corresponds to the first case and leads to a contradiction.Figure (d) corresponds to the second case.Figure (e) (resp., (f )) to the subcase (6, 2) ∈ D (resp. (6, 2) / ∈ D) leading to a contradiction in both subcases.

  Figure 6: Illustrations of Proposition 24 (n = 9). Red vertices are the one that are assumed to belong to the lethal set D of size 33, yellow vertices are assumed to belong to V \ D and white vertices are undetermined yet. Vertices (squares) surrounded by blue correspond to the hypotheses done in the different cases of the proof. Figure (a) is a configuration that is certain if |D| = 33. Figure (b) is the configuration obtained if (2, 4) ∈ D and (4, 2) / ∈ D and leads to a contradiction (Claim 26).Figure (c) corresponds to the first case and leads to a contradiction.Figure (d) corresponds to the second case.Figure (e) (resp., (f )) to the subcase (6, 2) ∈ D (resp. (6, 2) / ∈ D) leading to a contradiction in both subcases.

  Figure 6: Illustrations of Proposition 24 (n = 9). Red vertices are the one that are assumed to belong to the lethal set D of size 33, yellow vertices are assumed to belong to V \ D and white vertices are undetermined yet. Vertices (squares) surrounded by blue correspond to the hypotheses done in the different cases of the proof. Figure (a) is a configuration that is certain if |D| = 33. Figure (b) is the configuration obtained if (2, 4) ∈ D and (4, 2) / ∈ D and leads to a contradiction (Claim 26).Figure (c) corresponds to the first case and leads to a contradiction.Figure (d) corresponds to the second case.Figure (e) (resp., (f )) to the subcase (6, 2) ∈ D (resp. (6, 2) / ∈ D) leading to a contradiction in both subcases.

• case 2 :

 2 In at least one of the pairs {(2, 4), (2, 6)} {(4, 2), (6, 2)}, {(4, 8), (6, 8)} {(8, 4), (8, 6)} one vertex belongs to D and the other not. By symmetry suppose (2, 4) ∈ D and (2, 6) / ∈ D. By Claim 26, as (2, 4) ∈ D, then (4, 2) ∈ D. By Property 23(a) (3, 4) / ∈ D and (4, 3) / ∈ D. By Claim 26, as (2, 6) / ∈ D, then (4, 8) / ∈ D. Hence, by Claim 25, (6, 8) ∈ D and again by Claim 26, (8, 6) ∈ D. Moreover, by Property 23(a) (6, 7) and (7, 6) are not in D. Now, Property 21 implies (3, 7) ∈ D, since otherwise there would be a path from (1, 6) to (4, 9) in V \ D. Then, Property 23(a) implies that (3, 6) and (4, 7) / ∈ D. Then, by Property 21, (4, 6) ∈ D again to avoid a path from (1, 6) to (4, 9) in V \ D and then, by Property 23(a) (4, 5) and (5, 6) / ∈ D. Then, vertices (3, 5) and (5, 7) need to be in D to avoid 4-cycle in V \ D. See Figure 6(d) for the configuration reached so far. There are two subcases to be considered. -Case (6, 2) ∈ D (see Figure 6(e)). By Claim 26, (8, 4) ∈ D and so by Property 23(a), (6, 3) and (7, 4) / ∈ D. Then, Property 23(b), (7, 3) / ∈ D (otherwise (8, 3) would have 4 neighbours in D). Then (6, 4) must be in D to avoid a 4-cycle in V \ D and so, by Property 23(a), (5, 4), (6, 5) / ∈ D to avoid adjacent vertices in D. At this point, D already contains 31 vertices. Then to avoid 4-cycles in V \ D either (4, 4) ∈ D or both (3, 3) and (5, 3) ∈ D; similarly either (6, 6) ∈ D or both (5, 5) and (7, 5) ∈ D. Therefore, to get |D| = 33 we need to have (4, 4) ∈ D and (6, 6) ∈ D and the other vertices (5, 3), (5, 5), (7, 5) /

Figure 7 :

 7 Figure 7: Illustration of Theorem 28 and Theorem 29 for the torus T n×n . The vertices are depicted as small squares. Red squares are those of a lethal set D of G (n-1)×(n-1) . Orange squares are deleted from D and not infected in the torus. Blue vertices are extra infected vertices in the torus. In Figure 7(b) (resp. 7(d)), we start from the optimal grid G 4×4 (resp. G 6×6 ) and apply recursively the construction of proposition 14 (resp. plus proposition 11).

= n 2 +3 3 =

 3 (a)). So, |D | = |D|. We have |D| = LB n-1 = (n-1) 2 +2(n-1)+4 3 LBT n .

=

  (b)). So, |D | = |D| -1. We have |D| = LB n-1 = (n-1) 2 +2(n-1)+6 3 = n 2 +5 3 . So, |D | = n 2 +2 3 LBT n .

=

  (c)). So, |D | = |D| + 1. We have |D| = LB n-1 = (n-1) 2 +2(n-1)+1 3 = n 2 3 . So, |D | = n 2 +3 3 LBT n .

=

  (d)). So, |D | = |D|. We have |D| = LB n-1 + 1 = (n-1) 2 +2(n-, |D | = |D| = n 2 +2 3 LBT n .

http://golly.sourceforge.net/

Recently, the problem was solved in[START_REF] Peter | Extremal bounds for threeneighbour bootstrap percolation in dimensions two and three[END_REF]. In particular, the authors show that s3(Gn×n) = LBn + 1 when n is odd and not congruent to 5 (mod 6) or of the form 2 p -1 for p ≥ 1.

* This work has been supported by the French government through the UCA JEDI (ANR-15-IDEX-01) and EUR DS4H (ANR-17-EURE-004) Investments in the Future projects, by the SticAm-Sud project GALOP, and by the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior -Brasil (CAPES) -Finance Code 001 and CNPq (Proc 315042/2021-4).

Note that, for every k ∈ N: s r (G) ≤ k if and only if s

We formulate the problem as the MILP below, which computes an optimal solution for s T r (G). The main variables are the binary variables c v,t for v ∈ V and t ∈ {1, ..., T }, defined as follows: c v,t = 1 if the vertex v is infected after the t th step of the contamination process and 0 otherwise.

We describe hereafter the different constraints (1-6) of the MILP, starting by the objective function:

(1) Minimize the number of initially infected vertices.

(2) After T steps, all the vertices are infected.

(3) An infected vertex remains infected.

(4) A non infected vertex with less than r infected neighbors cannot become infected.

(5) Every vertex with a degree strictly smaller than r must be initially infected (case for instance of the corners of a grid G n×n when r = 3 (Property 6)).

(6) If two adjacent vertices have degree r, then at least one must be initially infected (case for instance of two adjacent vertices of the border of a grid G n×n when r = 3, (Property 7)).

Subject to

c w,t-1 ∀v ∈ V, t ∈ {1, ..., T } (4)

We note that the above cuts were not sufficient to make the MILP terminate (in sufficiently reasonable time) for G = G n×n except for some small values of n. Therefore, to speedup the search, we propose further optimization cuts which hold under certain conditions on G.

Further cuts if r ≥ 3 and and G = G n×n . Let r ≥ 3. Consider the graph G obtained from G by adding a new vertex x adjacent to every vertex of the border of G. Let H be the subgraph induced by H and x. By Property 21, if D is a lethal set, then H = V \ D is acyclic, and moreover, every connected component of H has at most one vertex on the border. Note that H satisfies both these properties if and only if H is acyclic.

We introduce the next constraints (9-14) to express this property.