Injective parent maps below the selected level #
Every newly created lower node lies strictly above the selected anchor's level. Thus nodes at or below that level come from upper copies, on which the parent map is injective. Complete refinement additionally removes the upper anchor, so no such low node can have the selected anchor as parent.
Forgetting the layer is injective on upper-layer nodes.
theorem
EGZ.FlagDecomposition.reducedSubdivisionMap_node_injective
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(hp : Odd p)
:
theorem
EGZ.FlagDecomposition.PrunedWeights.cleanedSubdivisionMap_node_injective
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
(D : Φ.PrunedWeights)
(hp : Odd p)
:
theorem
EGZ.FlagDecomposition.FaceRefinement.normalized_low_layer_ne_zero
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hΓ : Γ ≠ ⊤)
(L : ℕ)
(hL : L ≤ Φ.level anchor)
(x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node)
(hx : (normalized Φ anchor Γ hp C hmod hcenter).level x ≤ L)
:
theorem
EGZ.FlagDecomposition.FaceRefinement.normalized_parent_injOn_low
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(Φ : FlagDecomposition p d f)
(anchor : Φ.flag.Node)
(Γ : (Φ.flag.polytope anchor).Face)
(hp : Odd p)
(C :
(x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) →
IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x))
(hmod :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
Function.Injective ⇑((Rechart.chart (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C x).modp p))
(hcenter :
∀ (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node),
∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hΓ : Γ ≠ ⊤)
(L : ℕ)
(hL : L ≤ Φ.level anchor)
:
Set.InjOn ⇑(normalizedSubdivisionMap Φ anchor Γ hp C hmod hcenter).node
{x : (normalized Φ anchor Γ hp C hmod hcenter).flag.Node | (normalized Φ anchor Γ hp C hmod hcenter).level x ≤ L}
No two output nodes at or below the selected level share an old parent. This does not require minimality of the input.
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_low_layer_ne_zero
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hcount : 0 < D.count)
(L : ℕ)
(hL : L ≤ Φ.level anchor)
(x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node)
(hx : (D.normalized hp hδ hsmall C hmod hcenter).level x ≤ L)
:
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_parent_injOn_low
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hcount : 0 < D.count)
(L : ℕ)
(hL : L ≤ Φ.level anchor)
:
Set.InjOn ⇑(D.normalizedSubdivisionMap hp hδ hsmall C hmod hcenter).node
{x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node | (D.normalized hp hδ hsmall C hmod hcenter).level x ≤ L}
theorem
EGZ.FlagDecomposition.CompletePreparation.normalized_low_parent_ne_anchor
{p d : ℕ}
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
{Φ : FlagDecomposition p d f}
{anchor : Φ.flag.Node}
{t : ℕ → ℕ}
{δ : ℝ}
(D : Φ.CompletePreparation anchor t δ)
(hp : Odd p)
(hδ : 0 ≤ δ)
(hsmall : 3 ^ (d + 1) * δ < 1)
(C : (x : (D.diagram hp hδ hsmall).Node) → IntegerLatticeChart ((D.diagram hp hδ hsmall).support x))
(hmod :
∀ (x : (D.diagram hp hδ hsmall).Node), Function.Injective ⇑((IntegralAffineMap.ofIntAffineMap (C x).map).modp p))
(hcenter : ∀ (x : (D.diagram hp hδ hsmall).Node), ∀ q ∈ (C x).coordinateSupport, IsCenteredLift p q)
(hcount : 0 < D.count)
(L : ℕ)
(hL : L ≤ Φ.level anchor)
(x : (D.normalized hp hδ hsmall C hmod hcenter).flag.Node)
(hx : (D.normalized hp hδ hsmall C hmod hcenter).level x ≤ L)
:
Complete refinement deletes the old upper anchor, and all its new lower copies have larger level. Hence the anchor has no low-level child.