Realizing local facet witnesses with frozen boundary parameters

A local target may prescribe arbitrary vectors at movable vertices, but must agree with the base assignment at frozen vertices. Injectivity of the local scalar-parameter map then lets us realize that target by one global movable-parameter assignment. This is the algebraic adapter used by the concrete endpoint-stack facet witnesses.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.LocalTargetRespectsFrozen {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (target : Fin (p + 1) → Fin p → ℝ) : Prop

A local target respects the relative boundary when it agrees with the base assignment at every frozen local scalar site.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.localTargetMove {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (target : Fin (p + 1) → Fin p → ℝ) : Parameters.MovableParameter hp C → ℝ

Movable assignment realizing one prescribed local target. Outside the selected local cell it retains the base movable value.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.localTargetMove_localParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (target : Fin (p + 1) → Fin p → ℝ) (i : Fin (p + 1)) (j : Fin p) (hmovable : ¬Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C q i j)) : localTargetMove hp C base q target ⟨RelativeGenericity.localParameter hp C q i j, hmovable⟩ = target i j

At every movable local scalar site, localTargetMove returns the prescribed coordinate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.localVertexMap_replaceMovable_localTargetMove {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (target : Fin (p + 1) → Fin p → ℝ) (hfrozen : LocalTargetRespectsFrozen hp C base q target) : Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base (localTargetMove hp C base q target)) q = { value := target }

Reconstructing the full assignment from localTargetMove realizes the target at every local vertex, provided the target respects frozen sites.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.exists_facetRegularityWitness_of_localTarget {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (k : Fin (p + 1)) (target : Fin (p + 1) → Fin p → ℝ) (hfrozen : LocalTargetRespectsFrozen hp C base q target) (hdet : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp { value := target } k ≠ 0) : ∃ (x : Parameters.MovableParameter hp C → ℝ), AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (Polynomials.localVertexMap hp C (Parameters.replaceMovable hp C base x) q) k ≠ 0

A boundary-respecting local target with nonzero selected facet determinant gives the pointwise witness consumed by AllFacetRegularityWitnesses.