Congruence of Lemma 102 and Theorem 103 in the dimension bound #
The constructions of Lemma 102 and Theorem 103 (Hironaka.BoundaryClearing,
Hironaka.OrderReduction) read the dimension bound n ONLY through the class proofs and through
the choice of the inductive input applied — never as data. So two instances of the same
construction, at stages n and n' ≤ n, fed inductive inputs that AGREE on the marked triples of
dimension ≤ n' − 1 (where both are evaluated), take the same value at every triple of the smaller
class. This module proves the congruences on VALUES, heterogeneous in the stage (both class proofs
are arguments):
Hironaka.BD.bdData_congr— the data of [Kol07, Lemma 102]: at mark0both functors arezeroFunctor(no inductive input); at markm + 1both aredataFunctor, which evaluates the input ONCE, at the restricted marked triple of dimension≤ n' − 1(rawSeq), where the agreement hypothesis applies.Hironaka.BO.step21Seq_congr,step22Functor_congr,step2Seq_congr,maxContactCase_congr— Step 2 of the proof of [Kol07, Theorem 103] (the maximal contact case, [Kol07, 104]), by induction along the Step 2.1 recursion and the case split of the re-tuned Step 2.2, the dependent Step 2.2 input triple handled by generalising over the Step 2.1 sequence.Hironaka.BO.functor_congr— Theorem 103 itself:BO_{n,m}is the globalization of the local functor along local covers (OrderSeqAssignment.globalize, never unfolded); RESTRICTED to the stage-n'class (OrderSeqAssignment.restrict), the stage-nfunctor agrees with the stage-n'local functor on the local triples (functor_seq_localClassat stagenthroughTriple.boClass_mono, thenmaxContactCase_congr) and commutes with surjective open-immersion coproducts, so the uniqueness of the extension in [Kol07, Theorem 105] (globalization_unique) identifies it with the stage-n'functor.Hironaka.BO.data_congr— Theorem 103 as data (BO.data) atbdData.
Congruence of the data of [Kol07, Lemma 102] in the dimension bound: bdData at stages n and
n' ≤ n, from inductive inputs that agree on the marked triples of dimension ≤ n' − 1, take the
same value at a triple of both classes. At mark 0 both functors are zeroFunctor (no input); at
mark m + 1 both are dataFunctor, nil below the mark and at the mark rawSeq with the input
evaluated ONCE, at the restricted marked triple — of dimension ≤ n' − 1 by
hasDimLE_restrictedTriple at stage n'.
Congruence of Step 2.1 of [Kol07, 104] in the dimension bound: the Step 2.1 states at stages n
and n' ≤ n, from Lemma 102 data that agree pointwise on the triples of both classes, coincide (as
carried sequences) — by induction on the number of rounds: the round at a position of E is the
datum's value at the induced triple, equal by hbd; beyond the last position both states are
unchanged.
Congruence of Step 2.2 of [Kol07, 104] in the dimension bound: the re-tuned Lemma 102
(step22Functor) at stages n and n' ≤ n takes the same value at a triple of both classes — at
the mark both are the datum at s(m) on the tuned triple (hbd), below it both are nil.
Step 2 at stage n', generalised over its Step 2.1 sequence S₂ with S₂ equal to the Step
2.1 sequence at stage n (the dependent Step 2.2 input triple is handled by this generalisation):
it is Step 2 at stage n.
Congruence of Step 2 of the proof of [Kol07, Theorem 103] in the dimension bound: Step 2 for a
smooth hypersurface of maximal contact, at stages n and n' ≤ n with pointwise agreeing Lemma 102
data, coincide — Step 2.1 by step21Seq_congr, Step 2.2 on the (then equal) input triple by
step22Functor_congr.
Congruence of Steps 1–2 of the proof of [Kol07, Theorem 103] in the dimension bound: the
maximal-contact case BO^H_{n,m} at stages n and n' ≤ n, with pointwise agreeing Lemma 102
data, coincide — at the mark by step2Seq_congr on the tuned triple, below it both are nil.
Congruence of the functor of [Kol07, Theorem 103] in the dimension bound (Step 3 of its proof
and the uniqueness of [Kol07, Theorem 105]): BO_{n,m} and BO_{n',m} (n' ≤ n), from pointwise
agreeing Lemma 102 data, take the same value at a triple of the smaller class. The stage-n functor
restricted to BOClass n' m agrees with the stage-n' LOCAL functor on the local triples
(functor_seq_localClass at stage n through boClass_mono, localFunctor_seq,
maxContactCase_congr) and commutes with surjective open-immersion coproducts
(functor_commutesWithSmoothSurjections, restricted), as does the stage-n' functor;
globalization_unique at the stage-n' classes identifies the two functors. globalize is never
unfolded.
Congruence of [Kol07, Theorem 103] as data (BO.data) in the dimension bound: at stages n and
n' ≤ n, from inductive inputs that agree on the marked triples of dimension ≤ n' − 1, it takes
the same value at a triple of both classes — functor_congr at bdData, whose congruence is
bdData_congr.