Congruence of Theorem 107 in the dimension bound

The assembly of [Kol07, Theorem 107] (Hironaka.Resolution.Algebraic.MarkedOrderReduction.Theorem107) reads the dimension bound n through the class proofs, through which input BO_{n,d} it applies — and, in Step 3, through the phase count of the monomial run realize (Hironaka.Monomial). So two instances of the assembly, at stages n and n' ≤ n, fed inputs bo, bo' that agree at EVERY order d on the triples of both classes, take the same value at every marked triple of the smaller class:

• Step 1 (step1_congr) and Step 2 (step2_congr) of [Kol07, 111]: the rounds are the inputs' values at the round triples (X, N(I), E) and (X, N(I)^m + I^s, E) — equal by the agreement — and the loops are followed in lockstep by induction on a bound for the loop variable, the induced marked triple after a round transported along the equality of the rounds;
• Step 3 (step3Seq_congr): the input family step3Family T is the triple's, and the realized run does not depend on the bound (PieceFamily.realize_eq_of_le);
• the assembly (bmoSeq_congr, functor_congr, data_congr): the three steps concatenated, the triples after Steps 1 and 2 transported along the equalities of the steps.

theorem Hironaka.BMO.step1Round_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) (hd : m ≤ roundOrder T) : step1Round bo T hT hd = step1Round bo' T hT' hd

A round of Step 1 of [Kol07, 111] at stages n and n' ≤ n is the same sequence — the inputs agree at (X, N(I), E).

theorem Hironaka.BMO.step1_congr_aux {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (l : ℕ) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : roundOrder T ≤ l → ↑(step1 bo T hT) = ↑(step1 bo' T hT')

The induction behind step1_congr: on a bound l for the loop variable, following the recursion of step1.

theorem Hironaka.BMO.step1_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : ↑(step1 bo T hT) = ↑(step1 bo' T hT')

Congruence of Step 1 of [Kol07, 111] in the dimension bound: Step 1 at stages n and n' ≤ n, from inputs agreeing at every order, coincides on a marked triple of both classes.

theorem Hironaka.BMO.step2Round_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) (hs : 0 < sepOrder T) : step2Round bo T hT hs = step2Round bo' T hT' hs

A round of Step 2 of [Kol07, 111] at stages n and n' ≤ n is the same sequence — the inputs agree at (X, N(I)^m + I^s, E).

theorem Hironaka.BMO.step2_congr_aux {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (l : ℕ) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : sepOrder T ≤ l → ↑(step2 bo T hT) = ↑(step2 bo' T hT')

The induction behind step2_congr: on a bound l for the separation order, following the recursion of step2.

theorem Hironaka.BMO.step2_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : ↑(step2 bo T hT) = ↑(step2 bo' T hT')

Congruence of Step 2 of [Kol07, 111] in the dimension bound: Step 2 at stages n and n' ≤ n, from inputs agreeing at every order, coincides on a marked triple of both classes.

theorem Hironaka.BMO.step3Seq_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (hle : n' ≤ n) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : step3Seq T hT = step3Seq T hT'

Step 3 of [Kol07, 111] (order reduction for the monomial part) of a marked triple does not depend on the dimension bound — PieceFamily.realize_eq_of_le on the triple's input family.

theorem Hironaka.BMO.bmoSeq_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (hle : n' ≤ n) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : bmoSeq bo T hT = bmoSeq bo' T hT'

Congruence of the assembled sequence BMO_{n,m}(X, I, m, E) of [Kol07, Theorem 107; 111] in the dimension bound: at stages n and n' ≤ n, from inputs agreeing at every order, it coincides on a marked triple of both classes — Step 1 by step1_congr, Step 2 on the (then equal) induced triple by step2_congr, Step 3 by step3Seq_congr.

theorem Hironaka.BMO.functor_congr {k : Type u} [Field k] [CharZero k] {n n' m : ℕ} (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hagree : ∀ (d : ℕ) (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (hle : n' ≤ n) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : (functor bo m).seq T hT = (functor bo' m).seq T hT'

Congruence of the functor of [Kol07, Theorem 107] in the dimension bound: BMO_{n,m} and BMO_{n',m} (n' ≤ n), from inputs agreeing at every order, take the same value at a marked triple of the smaller class.

theorem Hironaka.BMO.data_congr {n n' m : ℕ} (hle : n' ≤ n) (bo : (d : ℕ) → BOData n d) (bo' : (d : ℕ) → BOData n' d) (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) (hboind' : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo' d).functor k).IndifferentToEmptyMembers) (hagree : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : AlgebraicGeometry.Triple k) (h₁ : AlgebraicGeometry.Triple.BOClass n d T) (h₂ : AlgebraicGeometry.Triple.BOClass n' d T), ((bo d).functor k).seq T h₁ = ((bo' d).functor k).seq T h₂) (k : Type u) [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T) : ((data bo hboind).functor k).seq T hT = ((data bo' hboind').functor k).seq T hT'

Congruence of [Kol07, Theorem 107] as data (BMO.data) in the dimension bound: at stages n and n' ≤ n, from inputs agreeing at every order d on the triples of both classes, it takes the same value at a marked triple of both classes.