Composition of boundary-relative facet targets

Lower-relative targets propagate through a stack composition: the left cells reuse their target, while every right cell is strictly away from the external lower boundary and may use the universal triangular facet witness. Reversal gives upper-relative targets. A final lower/upper composition then produces targets respecting the exact frozen-parameter predicate.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.facetMatrix_witnessTarget {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetMatrix hp { value := EquivariantPrismGenericityNonzero.facetWitnessTarget hp k } k = fun (r c : Fin p) => Fin.lastCases 1 (fun (s : Fin (p - 1)) => Fin.lastCases 0 (fun (t : Fin (p - 1)) => if s = t then 1 else 0) ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) c)) ((AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp) r)

The facet matrix of the universal triangular target. Both the row and the column index are reindexed by augmentedRowEquiv, which is the dimension used inside facetMatrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.facetWitnessTarget_determinant {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp { value := EquivariantPrismGenericityNonzero.facetWitnessTarget hp k } k = 1

The universal triangular facet target has determinant one.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.facetWitnessTarget_determinant_ne_zero {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) : AffinePositiveRayBoundary.VertexMap.facetDeterminant hp { value := EquivariantPrismGenericityNonzero.facetWitnessTarget hp k } k ≠ 0

Universal target determinant is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.lowerFacetTargets_combined_left {p N₀ N₁ : ℕ} (hp : Nat.Prime p) {Nmid M₀ L₀ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hC : RouteBEndpointFacetTargets.LowerFacetTargets hp C a) : RouteBEndpointFacetTargets.LowerFacetTargets hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)

Lower-relative targets survive composition with an arbitrary right collar.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.UpperFacetTargets {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) : Prop

Upper-relative version of the facet-target property.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.upperFacetTargets_reverse {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (hC : RouteBEndpointFacetTargets.LowerFacetTargets hp C a) : UpperFacetTargets hp (ExplicitAffineRelativeCollarReverse.reverseCells C) (ExplicitAffineRelativeCollarAssignmentReverse.reverseAssignment C a)

Reversal turns lower-relative targets into upper-relative targets.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.FrozenFacetTargets {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) : Prop

Target-level form of exact frozen-boundary compatibility.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.frozenFacetTargets_combined {p N₀ N₁ : ℕ} (hp : Nat.Prime p) {Nmid M₀ L₀ M₁ L₁ : ℕ} (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ Nmid M₀ L₀) (D : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp Nmid N₁ M₁ L₁) (a : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (b : ExplicitAffineRelativeCollar.Parameters.Assignment hp D) (hseam : ExplicitAffineRelativeCollarAssignmentCompose.SeamCompatible C D (ExplicitAffineRelativeCollar.Parameters.vectorValue hp C a) (ExplicitAffineRelativeCollar.Parameters.vectorValue hp D b)) (hC : RouteBEndpointFacetTargets.LowerFacetTargets hp C a) (hD : UpperFacetTargets hp D b) : FrozenFacetTargets hp (ExplicitAffineRelativeCollarCompose.combinedCells C D) (ExplicitAffineRelativeCollarAssignmentCompose.combinedAssignment C D a b hseam)

Lower- and upper-relative targets combine into exact frozen-relative targets.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.RouteBFacetTargetComposition.allFacetRegularityWitnesses_of_frozenFacetTargets {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N₀ N₁ M L) (base : ExplicitAffineRelativeCollar.Parameters.Assignment hp C) (h : FrozenFacetTargets hp C base) : ExplicitAffineRelativeCollar.RouteB.AllFacetRegularityWitnesses hp C base

Frozen-relative targets give the pointwise regularity witnesses consumed by Route B.