Explicit affine relative collars and boundary-restricted genericity polynomials

This module defines the affine-cell interface used by the relative-cobordism construction.

A RelativeAffineCellSystem is finite proof-carrying data for a genuine simplicial cylinder: its top cells are prime-orbit representatives with ordered geometric vertices, injective affine charts, and coefficients. Prime equivariance is reconstructed from symmetry-decorated local vertex occurrences rather than by imposing an action on the chosen orbit representatives. A FoxNeuwirthRelativeAffineCollar adds the exact signed facet-incidence formula for independently subdivided lower and upper boundaries.

The second half of the file constructs the global point-coordinate orbit quotient directly from those explicit cells. Horizontal parameter orbits are frozen. All other interior and spatial-side orbits remain movable. Facet-determinant and codimension-two-minor polynomials are then restricted to the movable polynomial ring. Evaluation of a restricted polynomial is proved to be evaluation of the corresponding determinant after replacing only movable data.

Existence of the relative barycentric cylinder and nontriviality of the restricted polynomials are handled by the dedicated geometric and boundary-aware algebraic modules. Purely horizontal codimension-two minors are governed by stable endpoint transversality rather than the movable genericity family.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.IsHorizontalPoint {p : ℕ} (z : EquivariantPrismVertexParameters.CylinderPoint p) : Prop

A cylinder point belongs to one of the two fixed horizontal boundary layers.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.IsHorizontalPoint z = (↑z.time = 0 ∨ ↑z.time = 1)

Genuine finite affine-cell data

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M L : ℕ) : Type 1

A finite family of nondegenerate affine p-simplex representatives in the realization cylinder. The representatives are already taken modulo prime symmetry; equivariant global vertex parameters are reconstructed below by adjoining a symmetry decoration to every local occurrence. The four level fields record the two fixed endpoint triangulations, a common interior level, and a time-refinement level.

• lower_le_common : N₀ ≤ M
• upper_le_common : N₁ ≤ M
• Cell : Type

  The finite type of affine cells forming the relative collar.

• cell_nonempty : Nonempty self.Cell
• instCellFintype : Fintype self.Cell
• instCellDecidableEq : DecidableEq self.Cell
• coefficient : self.Cell → ZMod p

  The coefficient of each collar cell in the prime residue field.

• vertex : self.Cell → Fin (p + 1) → EquivariantPrismVertexParameters.CylinderPoint p

  The cylinder point assigned to each vertex of a collar cell.

• chart : self.Cell → ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p) → EquivariantPrismVertexParameters.CylinderPoint p

  The affine simplex chart parametrizing each collar cell.

• chart_vertex (q : self.Cell) (i : Fin (p + 1)) : self.chart q (SphereOddDegree.FiniteSimplex.vertex i) = self.vertex q i
• chart_spatial_affine (q : self.Cell) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) (c : BarredPermutation p) : ↑(self.chart q w).spatial c = ∑ i : Fin (p + 1), w i * ↑(self.vertex q i).spatial c
• chart_time_affine (q : self.Cell) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(self.chart q w).time = ∑ i : Fin (p + 1), w i * ↑(self.vertex q i).time
• chart_injective (q : self.Cell) : Function.Injective (self.chart q)
• vertex_injective (q : self.Cell) : Function.Injective (self.vertex q)
• vertex_orbit_injective (q : self.Cell) (g : ↥(PrimeSymmetry p)) (i j : Fin (p + 1)) : g • self.vertex q i = self.vertex q j → g = 1 ∧ i = j

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.VertexSlot {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

One local vertex occurrence of one explicit relative collar cell.

Equations

• C.VertexSlot = (C.Cell × Fin (p + 1))

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.vertexSlotFintype {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype C.VertexSlot

Equations

• C.vertexSlotFintype = inferInstance

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.vertexSlotDecidableEq {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq C.VertexSlot

Equations

• C.vertexSlotDecidableEq = inferInstance

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.FacetOccurrence {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

One local facet occurrence, indexed by its omitted vertex.

Equations

• C.FacetOccurrence = (C.Cell × Fin (p + 1))

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetOccurrenceFintype {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype C.FacetOccurrence

Equations

• C.facetOccurrenceFintype = inferInstance

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetOccurrenceDecidableEq {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq C.FacetOccurrence

Equations

• C.facetOccurrenceDecidableEq = inferInstance

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.slotPoint {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : C.VertexSlot) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric point at a local cell vertex occurrence.

Equations

• C.slotPoint s = C.vertex s.1 s.2

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetSignature {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : Fin p → EquivariantPrismVertexParameters.CylinderPoint p

Ordered geometric vertex tuple of the facet obtained by omitting o.2.

Equations

• C.facetSignature o i = C.vertex o.1 (o.2.succAbove i)

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetSetoid {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Setoid C.FacetOccurrence

Two facet occurrences represent the same oriented quotient facet when one ordered geometric signature is the simultaneous prime translate of the other. This is the facet-orbit relation required by the Fox--Neuwirth orbit cycle: spatial side faces cancel after passage to the prime quotient, not necessarily as identical facets of the chosen top-cell representatives.

Equations

• C.facetSetoid = { r := fun (a b : C.FacetOccurrence) => ∃ (g : ↥(NRR.PrimeSymmetry p)), (fun (i : Fin p) => g • C.facetSignature a i) = C.facetSignature b, iseqv := ⋯ }

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.Facet {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Finite ordered prime-orbit facets of the explicit relative collar.

Equations

• C.Facet = Quotient C.facetSetoid

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetFintype {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype C.Facet

Equations

• C.facetFintype = Fintype.ofFinite C.Facet

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetDecidableEq {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq C.Facet

Equations

• C.facetDecidableEq = Classical.decEq C.Facet

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetClass {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : C.Facet

Quotient facet represented by a local occurrence.

Equations

• C.facetClass o = ⟦o⟧

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.alternatingSign {p : ℕ} (k : Fin (p + 1)) : ZMod p

Alternating boundary sign attached to an omitted local vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.alternatingSign k = (-1) ^ ↑k

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.facetIncidence {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : C.Facet) : ZMod p

Total signed incidence coefficient of one ordered prime-orbit facet.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.IsLowerFacetOccurrence {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : Prop

A local facet occurrence lies in the fixed lower horizontal boundary.

Equations

• C.IsLowerFacetOccurrence o = ∀ (i : Fin p), ↑(C.facetSignature o i).time = 0

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.IsUpperFacetOccurrence {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (o : C.FacetOccurrence) : Prop

A local facet occurrence lies in the fixed upper horizontal boundary.

Equations

• C.IsUpperFacetOccurrence o = ∀ (i : Fin p), ↑(C.facetSignature o i).time = 1

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.IsLowerFacet {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : C.Facet → Prop

Lower-horizontal status is well-defined on ordered quotient-facet classes because prime symmetry preserves the interval coordinate.

Equations

• C.IsLowerFacet = Quotient.lift C.IsLowerFacetOccurrence ⋯

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.IsUpperFacet {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) : C.Facet → Prop

Upper-horizontal status is well-defined on ordered quotient-facet classes because prime symmetry preserves the interval coordinate.

Equations

• C.IsUpperFacet = Quotient.lift C.IsUpperFacetOccurrence ⋯

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCellSystem.IsHorizontalFacet {p N₀ N₁ M L : ℕ} {hp : Nat.Prime p} (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : C.Facet) : Prop

A geometric facet is horizontal when it belongs to either fixed endpoint boundary.

Equations

• C.IsHorizontalFacet s = (C.IsLowerFacet s ∨ C.IsUpperFacet s)

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M L : ℕ) : Type 1

A proof-carrying relative affine collar. The boundary coefficient fields encode the exact upper-minus-lower horizontal boundary formula after all internal and side signatures are collected. The structure does not assume pairwise cancellation: an arbitrary number of occurrences may share a signature.

• cells : RelativeAffineCellSystem hp N₀ N₁ M L

  The affine cell system underlying the relative collar.

• lowerBoundaryCoefficient : self.cells.Facet → ZMod p

  The coefficient assigned to each lower boundary facet.

• upperBoundaryCoefficient : self.cells.Facet → ZMod p

  The coefficient assigned to each upper boundary facet.

• lower_zero_of_not_lower (s : self.cells.Facet) : ¬self.cells.IsLowerFacet s → self.lowerBoundaryCoefficient s = 0
• upper_zero_of_not_upper (s : self.cells.Facet) : ¬self.cells.IsUpperFacet s → self.upperBoundaryCoefficient s = 0
• incidence_eq_boundary (s : self.cells.Facet) : self.cells.facetIncidence s = self.upperBoundaryCoefficient s - self.lowerBoundaryCoefficient s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar.nonhorizontal_incidence_zero {p : ℕ} {hp : Nat.Prime p} {N₀ N₁ M L : ℕ} (C : FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L) (s : C.cells.Facet) (hs : ¬C.cells.IsHorizontalFacet s) : C.cells.facetIncidence s = 0

Every nonhorizontal geometric facet has zero total signed incidence.

Exact endpoint identification

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.lowerCylinderPoint {p : ℕ} (x : Realization p) : EquivariantPrismVertexParameters.CylinderPoint p

Embed a realization point in the lower horizontal boundary of the cylinder.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.upperCylinderPoint {p : ℕ} (x : Realization p) : EquivariantPrismVertexParameters.CylinderPoint p

Embed a realization point in the upper horizontal boundary of the cylinder.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.lowerCylinderPoint_time {p : ℕ} (x : Realization p) : ↑(lowerCylinderPoint x).time = 0

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.upperCylinderPoint_time {p : ℕ} (x : Realization p) : ↑(upperCylinderPoint x).time = 1

structure NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M L : ℕ) extends NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.FoxNeuwirthRelativeAffineCollar hp N₀ N₁ M L : Type 1

A relative affine collar whose horizontal boundary chain is exactly the independently refined Fox--Neuwirth orbit cycle. The endpoint maps need not be injective: several refined top cells may represent the same geometric prime-orbit facet, and their coefficients are then collected by the pairing identities. This is the chain-level identification required by Stokes and avoids imposing an artificial choice of a unique quotient-facet representative.

• cells : RelativeAffineCellSystem hp N₀ N₁ M L
• lowerBoundaryCoefficient : self.cells.Facet → ZMod p
• upperBoundaryCoefficient : self.cells.Facet → ZMod p
• lower_zero_of_not_lower (s : self.cells.Facet) : ¬self.cells.IsLowerFacet s → self.lowerBoundaryCoefficient s = 0
• upper_zero_of_not_upper (s : self.cells.Facet) : ¬self.cells.IsUpperFacet s → self.upperBoundaryCoefficient s = 0
• incidence_eq_boundary (s : self.cells.Facet) : self.cells.facetIncidence s = self.upperBoundaryCoefficient s - self.lowerBoundaryCoefficient s
• lowerFacet : RefinedAffineMap.TopCell hp N₀ → self.cells.Facet

  Identify each lower refined top cell with its collar boundary facet.

• upperFacet : RefinedAffineMap.TopCell hp N₁ → self.cells.Facet

  Identify each upper refined top cell with its collar boundary facet.

• lowerFacet_isLower (q : RefinedAffineMap.TopCell hp N₀) : self.cells.IsLowerFacet (self.lowerFacet q)
• upperFacet_isUpper (q : RefinedAffineMap.TopCell hp N₁) : self.cells.IsUpperFacet (self.upperFacet q)
• lowerFacet_exhaustive (s : self.cells.Facet) : self.cells.IsLowerFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₀), self.lowerFacet q = s
• upperFacet_exhaustive (s : self.cells.Facet) : self.cells.IsUpperFacet s → ∃ (q : RefinedAffineMap.TopCell hp N₁), self.upperFacet q = s
• lowerBoundaryPairing_eq (W : self.cells.Facet → ZMod p) : ∑ s : self.cells.Facet, self.lowerBoundaryCoefficient s * W s = ∑ q : RefinedAffineMap.TopCell hp N₀, RefinedAffineMap.coefficient hp N₀ q * W (self.lowerFacet q)
• upperBoundaryPairing_eq (W : self.cells.Facet → ZMod p) : ∑ s : self.cells.Facet, self.upperBoundaryCoefficient s * W s = ∑ q : RefinedAffineMap.TopCell hp N₁, RefinedAffineMap.coefficient hp N₁ q * W (self.upperFacet q)
• lowerFacetOccurrenceVertex_eq (q : RefinedAffineMap.TopCell hp N₀) (o : self.cells.FacetOccurrence) : self.cells.facetClass o = self.lowerFacet q → ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), self.cells.facetSignature o i = g • lowerCylinderPoint (RefinedAffineMap.vertex hp N₀ q (Fin.cast ⋯ i))
• upperFacetOccurrenceVertex_eq (q : RefinedAffineMap.TopCell hp N₁) (o : self.cells.FacetOccurrence) : self.cells.facetClass o = self.upperFacet q → ∃ (g : ↥(PrimeSymmetry p)), ∀ (i : Fin p), self.cells.facetSignature o i = g • upperCylinderPoint (RefinedAffineMap.vertex hp N₁ q (Fin.cast ⋯ i))

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar.exists_lowerTopCell {p : ℕ} {hp : Nat.Prime p} {N₀ N₁ M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M L) (s : C.cells.Facet) (hs : C.cells.IsLowerFacet s) : ∃ (q : RefinedAffineMap.TopCell hp N₀), C.lowerFacet q = s

Every lower horizontal quotient facet is represented by at least one level-N₀ refined orbit cell. Uniqueness is intentionally not required; the endpoint chain pairing collects repeated geometric representatives with their signed coefficients.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.EndpointIdentifiedRelativeAffineCollar.exists_upperTopCell {p : ℕ} {hp : Nat.Prime p} {N₀ N₁ M L : ℕ} (C : EndpointIdentifiedRelativeAffineCollar hp N₀ N₁ M L) (s : C.cells.Facet) (hs : C.cells.IsUpperFacet s) : ∃ (q : RefinedAffineMap.TopCell hp N₁), C.upperFacet q = s

Every upper horizontal quotient facet is represented by at least one level-N₁ refined orbit cell.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RelativeAffineCollarExists {p : ℕ} (hp : Nat.Prime p) (N₀ N₁ M L : ℕ) : Prop

Existence proposition for the genuine relative affine collar. In contrast with the previous raw interface, this proposition cannot be inhabited by an empty cell family or by a collar whose horizontal boundary is unrelated to the supplied Fox--Neuwirth subdivision levels.

Equations

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

Global vertices and boundary-frozen parameters

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Symmetry-decorated local vertex occurrences.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp C = (↥(NRR.PrimeSymmetry p) × C.VertexSlot)

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverVertexSlotFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (CoverVertexSlot hp C)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverVertexSlotFintype hp C = inferInstance

@[instance_reducible]

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverVertexSlotDecidableEq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq (CoverVertexSlot hp C)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverVertexSlotDecidableEq hp C = inferInstance

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverPoint {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : CoverVertexSlot hp C) : EquivariantPrismVertexParameters.CylinderPoint p

Geometric point represented by a decorated local occurrence.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverPoint hp C s = s.1 • C.slotPoint s.2

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverVertexSetoid {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Setoid (CoverVertexSlot hp C)

Equality of geometric cylinder points identifies duplicate local occurrences.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.GlobalVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Finite global vertices of the explicit relative affine collar.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalVertexFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (GlobalVertex hp C)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalVertexDecidableEq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq (GlobalVertex hp C)

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.actCoverVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot hp C) : CoverVertexSlot hp C

Left multiplication on the symmetry decoration.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.actCoverVertex hp C g s = (g * s.1, s.2)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.coverPoint_actCoverVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (g : ↥(PrimeSymmetry p)) (s : CoverVertexSlot hp C) : coverPoint hp C (actCoverVertex hp C g s) = g • coverPoint hp C s

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalVertexAction {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : MulAction (↥(PrimeSymmetry p)) (GlobalVertex hp C)

Prime symmetry acts on global relative-collar vertices.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalPoint {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : GlobalVertex hp C → EquivariantPrismVertexParameters.CylinderPoint p

Actual geometric point represented by a global vertex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalPoint_mk {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : CoverVertexSlot hp C) : globalPoint hp C ⟦s⟧ = coverPoint hp C s

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalPoint_smul {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp C) : globalPoint hp C (g • x) = g • globalPoint hp C x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.sampleVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : C.VertexSlot) : GlobalVertex hp C

Global vertex represented by an undecorated local slot.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.sampleVertex hp C s = ⟦(1, s)⟧

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.globalPoint_sampleVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (s : C.VertexSlot) : globalPoint hp C (sampleVertex hp C s) = C.slotPoint s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.sampleVertex_eq_of_slotPoint_eq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {s t : C.VertexSlot} (h : C.slotPoint s = C.slotPoint t) : sampleVertex hp C s = sampleVertex hp C t

Geometrically equal local slots determine the same global sampled vertex.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.ScalarSite {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Point-coordinate sites before quotienting by diagonal prime symmetry.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.Parameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

One scalar parameter per diagonal prime orbit.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.parameterFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (Parameter hp C)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.parameterDecidableEq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq (Parameter hp C)

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.IsFrozenVertex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : GlobalVertex hp C) : Prop

A global vertex is frozen precisely on one of the two horizontal boundaries.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.isFrozenVertex_smul {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp C) : IsFrozenVertex hp C (g • x) ↔ IsFrozenVertex hp C x

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.IsFrozenParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Parameter hp C → Prop

Frozen status is well-defined on diagonal parameter orbits.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.FrozenParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Frozen horizontal scalar parameter orbits.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.MovableParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Movable interior and spatial-side scalar parameter orbits.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.frozenParameterFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (FrozenParameter hp C)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.movableParameterFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (MovableParameter hp C)

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.Assignment {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

A full compatible equivariant scalar assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.replaceMovable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) : Assignment hp C

Replace only movable values, retaining the horizontal boundary assignment literally.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.replaceMovable_eq_base {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) {q : Parameter hp C} (hq : IsFrozenParameter hp C q) : replaceMovable hp C base move q = base q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.replaceMovable_eq_move {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) (q : MovableParameter hp C) : replaceMovable hp C base move ↑q = move q

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.FullPolynomialRing {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Full polynomial ring before fixing the horizontal boundary.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.MovablePolynomialRing {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Polynomial ring in movable parameter orbits only.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.relativeVariable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (q : Parameter hp C) : MovablePolynomialRing hp C

Substitute frozen variables by their base constants and retain movable variables.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.restrictPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) : FullPolynomialRing hp C →+* MovablePolynomialRing hp C

Restriction homomorphism to the boundary-relative movable polynomial ring.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.eval_relativeVariable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) (q : Parameter hp C) : (MvPolynomial.eval move) (relativeVariable hp C base q) = replaceMovable hp C base move q

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.eval_restrictPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) (P : FullPolynomialRing hp C) : (MvPolynomial.eval move) ((restrictPolynomial hp C base) P) = (MvPolynomial.eval (replaceMovable hp C base move)) P

Evaluation after restriction equals evaluation at the reconstructed boundary-relative full assignment.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.scalarValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Assignment hp C) (x : GlobalVertex hp C) (j : Fin p) : ℝ

Scalar value reconstructed at a global vertex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.scalarValue hp C a x j = a ⟦(x, j)⟧

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.vectorValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Assignment hp C) (x : GlobalVertex hp C) : Fin p → ℝ

Vector value reconstructed at a global vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.vectorValue_smul {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Assignment hp C) (g : ↥(PrimeSymmetry p)) (x : GlobalVertex hp C) : vectorValue hp C a (g • x) = g • vectorValue hp C a x

Every assignment reconstructs a prime-equivariant vector assignment.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.endpointAdjustedSiteValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) (s : ScalarSite hp C) : ℝ

Scalar endpoint-adjusted sample attached to one point-coordinate site. Interior sites sample the supplied zero-free homotopy. Sites on the two horizontal boundaries instead sample the actual endpoint approximations whose refined counts are being compared.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.endpointAdjustedSiteValue_eq_of_orbitRel {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) {a b : ScalarSite hp C} (hab : (MulAction.orbitRel (↥(PrimeSymmetry p)) (ScalarSite hp C)) a b) : endpointAdjustedSiteValue hp C H A₀ A₁ a = endpointAdjustedSiteValue hp C H A₀ A₁ b

Endpoint-adjusted samples are constant on diagonal prime orbits.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.endpointAdjustedAssignment {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) : Assignment hp C

Distinguished compatible assignment which agrees with the two supplied endpoint approximations on the horizontal boundary and with the zero-free homotopy at every other sampled vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.vectorValue_endpointAdjustedAssignment_lower {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) (x : GlobalVertex hp C) (hx : ↑(globalPoint hp C x).time = 0) : vectorValue hp C (endpointAdjustedAssignment hp C H A₀ A₁) x = A₀.map (globalPoint hp C x).spatial

Reconstructing the endpoint-adjusted assignment on the lower horizontal boundary gives the supplied lower approximation exactly.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.vectorValue_endpointAdjustedAssignment_upper {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) (x : GlobalVertex hp C) (hx : ↑(globalPoint hp C x).time = 1) : vectorValue hp C (endpointAdjustedAssignment hp C H A₀ A₁) x = A₁.map (globalPoint hp C x).spatial

Reconstructing the endpoint-adjusted assignment on the upper horizontal boundary gives the supplied upper approximation exactly.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.vectorValue_endpointAdjustedAssignment_interior {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) {F₀ F₁ : EquivariantCoordinateHomotopy.ZeroFreeMap hp} (H : EquivariantCoordinateHomotopy.ZeroFreeHomotopy hp F₀ F₁) (A₀ : RefinedAffineMap.RegularApproximation hp F₀.map) (A₁ : RefinedAffineMap.RegularApproximation hp F₁.map) (x : GlobalVertex hp C) (hx₀ : ↑(globalPoint hp C x).time ≠ 0) (hx₁ : ↑(globalPoint hp C x).time ≠ 1) : vectorValue hp C (endpointAdjustedAssignment hp C H A₀ A₁) x = H.map (globalPoint hp C x).toProd

Away from both horizontal boundaries, reconstructing the endpoint-adjusted assignment gives the original homotopy sample.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.localValue_eq_of_slotPoint_eq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Assignment hp C) {s t : C.VertexSlot} (h : C.slotPoint s = C.slotPoint t) : vectorValue hp C a (sampleVertex hp C s) = vectorValue hp C a (sampleVertex hp C t)

Local values agree whenever two local slots represent the same geometric point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Parameters.replaceMovable_horizontal_localValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Assignment hp C) (move : MovableParameter hp C → ℝ) (s : C.VertexSlot) (hs : IsHorizontalPoint (C.slotPoint s)) : vectorValue hp C (replaceMovable hp C base move) (sampleVertex hp C s) = vectorValue hp C base (sampleVertex hp C s)

Replacing movable parameters leaves a horizontal local vertex unchanged.

Full and boundary-restricted determinant polynomials

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.scalarPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : Parameters.GlobalVertex hp C) (j : Fin p) : Parameters.FullPolynomialRing hp C

Coordinate variable attached to one global vertex and one output coordinate.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.scalarPolynomial hp C x j = MvPolynomial.X ⟦(x, j)⟧

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.vectorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (x : Parameters.GlobalVertex hp C) : Fin p → Parameters.FullPolynomialRing hp C

Polynomial coordinate vector at a global vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.localVertexPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (i : Fin (p + 1)) : Fin p → Parameters.FullPolynomialRing hp C

Polynomial coordinate vector at one local explicit-cell vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.deviationPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (y : Fin p → Parameters.FullPolynomialRing hp C) (r : Fin (p - 1)) : Parameters.FullPolynomialRing hp C

Fixed deviation coordinate in the full polynomial ring.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.localVertexMap {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) : AffinePositiveRayBoundary.VertexMap p

Real local vertex map reconstructed from an assignment.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.assignmentEvalHom {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) : Parameters.FullPolynomialRing hp C →+* ℝ

Evaluation at a full assignment as a ring homomorphism.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.assignmentEvalHom hp C a = MvPolynomial.eval₂Hom (RingHom.id ℝ) a

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_scalarPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (x : Parameters.GlobalVertex hp C) (j : Fin p) : (MvPolynomial.eval a) (scalarPolynomial hp C x j) = Parameters.scalarValue hp C a x j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_vectorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (x : Parameters.GlobalVertex hp C) (j : Fin p) : (MvPolynomial.eval a) (vectorPolynomial hp C x j) = Parameters.vectorValue hp C a x j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_localVertexPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (i : Fin (p + 1)) (j : Fin p) : (MvPolynomial.eval a) (localVertexPolynomial hp C q i j) = Parameters.vectorValue hp C a (Parameters.sampleVertex hp C (q, i)) j

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_deviationPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (y : Fin p → Parameters.FullPolynomialRing hp C) (r : Fin (p - 1)) : (MvPolynomial.eval a) (deviationPolynomial hp C y r) = AffinePositiveRayBoundary.VertexMap.deviation hp (fun (j : Fin p) => (MvPolynomial.eval a) (y j)) r

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.facetMatrixPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (k : Fin (p + 1)) : Matrix (Fin p) (Fin p) (Parameters.FullPolynomialRing hp C)

Polynomial augmented deviation matrix on the facet omitting k.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.facetDeterminantPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (k : Fin (p + 1)) : Parameters.FullPolynomialRing hp C

Full-variable facet determinant polynomial.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.map_facetMatrixPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (k : Fin (p + 1)) : (assignmentEvalHom hp C a).mapMatrix (facetMatrixPolynomial hp C q k) = AffinePositiveRayBoundary.VertexMap.facetMatrix hp (localVertexMap hp C a q) k

Evaluation of the polynomial facet matrix gives the real facet matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_facetDeterminantPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (k : Fin (p + 1)) : (MvPolynomial.eval a) (facetDeterminantPolynomial hp C q k) = AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (localVertexMap hp C a q) k

Evaluation of the full facet polynomial is the actual local facet determinant.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.CodimTwoFace (p : ℕ) : Type

Ordered codimension-two face type.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.codimTwoVertex {p : ℕ} (hp : Nat.Prime p) (f : CodimTwoFace p) (i : Fin (p - 1)) : Fin (p + 1)

Retained local vertex after the two ordered omissions.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.codimTwoDeviationMatrixPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (f : CodimTwoFace p) : Matrix (Fin (p - 1)) (Fin (p - 1)) (Parameters.FullPolynomialRing hp C)

Polynomial deviation matrix on an ordered codimension-two face.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.codimTwoMinorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (f : CodimTwoFace p) : Parameters.FullPolynomialRing hp C

Full-variable codimension-two deviation minor.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.codimTwoDeviationMatrix {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (f : CodimTwoFace p) : Matrix (Fin (p - 1)) (Fin (p - 1)) ℝ

Corresponding real deviation matrix.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.map_codimTwoDeviationMatrixPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (f : CodimTwoFace p) : (assignmentEvalHom hp C a).mapMatrix (codimTwoDeviationMatrixPolynomial hp C q f) = codimTwoDeviationMatrix hp C a q f

Evaluation of the polynomial codimension-two matrix gives the real matrix.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_codimTwoMinorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) (q : C.Cell) (f : CodimTwoFace p) : (MvPolynomial.eval a) (codimTwoMinorPolynomial hp C q f) = (codimTwoDeviationMatrix hp C a q f).det

Evaluation of the full codimension-two polynomial is the actual determinant.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.restrictedFacetDeterminantPolynomial {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)) : Parameters.MovablePolynomialRing hp C

Boundary-restricted facet determinant polynomial.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.restrictedCodimTwoMinorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (q : C.Cell) (f : CodimTwoFace p) : Parameters.MovablePolynomialRing hp C

Boundary-restricted codimension-two minor polynomial.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_restrictedFacetDeterminantPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (q : C.Cell) (k : Fin (p + 1)) : (MvPolynomial.eval move) (restrictedFacetDeterminantPolynomial hp C base q k) = AffinePositiveRayBoundary.VertexMap.facetDeterminant hp (localVertexMap hp C (Parameters.replaceMovable hp C base move) q) k

Exact restricted evaluation identity for facet determinants.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_restrictedCodimTwoMinorPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (q : C.Cell) (f : CodimTwoFace p) : (MvPolynomial.eval move) (restrictedCodimTwoMinorPolynomial hp C base q f) = (codimTwoDeviationMatrix hp C (Parameters.replaceMovable hp C base move) q f).det

Exact restricted evaluation identity for codimension-two minors.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.IsLowerHorizontalCodimTwo {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (f : CodimTwoFace p) : Prop

An ordered codimension-two face is purely lower horizontal.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.IsUpperHorizontalCodimTwo {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (f : CodimTwoFace p) : Prop

An ordered codimension-two face is purely upper horizontal.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.IsPurelyHorizontalCodimTwo {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (f : CodimTwoFace p) : Prop

Purely horizontal codimension-two faces are excluded from the movable full-minor family.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.MovableCodimTwoIndex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Movable codimension-two indices.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.movableCodimTwoIndexFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (MovableCodimTwoIndex hp C)

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.movableCodimTwoIndexDecidableEq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq (MovableCodimTwoIndex hp C)

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.RelativeGenericityIndex {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Type

Relative genericity indices: all local facets, plus only non-purely-horizontal codimension-two faces.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.relativeGenericityIndexFintype {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : Fintype (RelativeGenericityIndex hp C)

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.relativeGenericityIndexFintype hp C = inferInstance

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.relativeGenericityIndexDecidableEq {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) : DecidableEq (RelativeGenericityIndex hp C)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.restrictedGenericityPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) : RelativeGenericityIndex hp C → Parameters.MovablePolynomialRing hp C

Combined boundary-restricted genericity polynomial family.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.genericityValue {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (a : Parameters.Assignment hp C) : RelativeGenericityIndex hp C → ℝ

Real determinant family corresponding to a full boundary-relative assignment.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.Polynomials.eval_restrictedGenericityPolynomial {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (base : Parameters.Assignment hp C) (move : Parameters.MovableParameter hp C → ℝ) (i : RelativeGenericityIndex hp C) : (MvPolynomial.eval move) (restrictedGenericityPolynomial hp C base i) = genericityValue hp C (Parameters.replaceMovable hp C base move) i

Evaluation identity for the combined relative genericity family.