Strict level increase after face refinement and minimalization

The face operation first splits atoms while retaining old coordinates. Minimalizing the resulting lower anchor identifies its lattice rank with the dimension of the selected proper face. Its represented space must then shrink, giving the strict level increase used in termination.

theorem EGZ.FlagDecomposition.FaceRefinement.lowerAnchor_rechart_rank_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hΓ : Γ.carrier ⊂ (Φ.flag.polytope anchor).carrier) : (C (lowerAnchor Φ anchor hp Γ)).rank < Φ.flag.rank anchor

A proper face gives a strictly smaller support-generated lattice at the lower anchor, even if the input coordinates were not minimal.

theorem EGZ.FlagDecomposition.FaceRefinement.lowerAnchor_rechart_level_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hinj : ∀ (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Γ : Γ.carrier ⊂ (Φ.flag.polytope anchor).carrier) : Φ.level anchor < (Rechart.decomposition (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C hp hinj hcenter).level (lowerAnchor Φ anchor hp Γ)

Strict increase at the lower anchor after changing to minimal support-generated coordinates.

theorem EGZ.FlagDecomposition.FaceRefinement.lower_rechart_level_lt {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hinj : ∀ (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Γ : Γ.carrier ⊂ (Φ.flag.polytope anchor).carrier) (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) (hx : (↑↑x).2 = 0) : Φ.level anchor < (Rechart.decomposition (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C hp hinj hcenter).level x

Every surviving lower-layer node has strictly larger level than the old anchor.

theorem EGZ.FlagDecomposition.FaceRefinement.upper_rechart_level_eq {p d : ℕ} [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (C : (x : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).flag.Node) → IntegerLatticeChart ((decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).liftedSupport x)) (hinj : ∀ (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Φ : Φ.IsMinimal) (x : Φ.flag.Node) : (Rechart.decomposition (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp) C hp hinj hcenter).level (upper Φ anchor (Φ.faceSelector anchor Γ) hp x) = Φ.level x

Upper levels are unchanged when the input was already minimal: both their cumulative support and their lifted support remain the original ones.