Survival of the upper anchor in a proper-face refinement

An unselected cumulative atom supplies an upper-layer local generator. The other generators witnessing old reducedness still have active copies, so their join together with this upper generator is the old upper node.

theorem EGZ.FlagDecomposition.FaceRefinement.upper_isReducedElement_of_unselected {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (selected : FpCoord p d → Prop) (hp : Odd p) (x : Φ.flag.Node) (hred : Φ.IsReducedElement x) (houtside : ∃ (v : FpCoord p d), Φ.cumulativeWeight x v ≠ 0 ∧ ¬selected v) : (decomposition Φ anchor selected hp).IsReducedElement (upper Φ anchor selected hp x)

A reduced old node remains reduced upstairs when some cumulative atom at that node is not moved to the lower layer.

theorem EGZ.FlagDecomposition.FaceRefinement.exists_unselected_of_ne_top {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (Γ : (Φ.flag.polytope anchor).Face) (hΓ : Γ ≠ ⊤) : ∃ (v : FpCoord p d), Φ.cumulativeWeight anchor v ≠ 0 ∧ ¬Φ.faceSelector anchor Γ v

A proper face leaves an unselected cumulative atom.

theorem EGZ.FlagDecomposition.FaceRefinement.face_upperAnchor_isReduced {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) (anchor : Φ.flag.Node) (hp : Odd p) (Γ : (Φ.flag.polytope anchor).Face) (hΓ : Γ ≠ ⊤) (hred : Φ.IsReducedElement anchor) : (decomposition Φ anchor (Φ.faceSelector anchor Γ) hp).IsReducedElement (upper Φ anchor (Φ.faceSelector anchor Γ) hp anchor)

The upper anchor of a proper-face refinement survives restriction to the reduced nodes.