Local last-vertex retraction for endpoint subdivision cylinders

This file proves the simplex-local geometric core needed by the endpoint-stack construction. For a point of a standard simplex, lastSupportIndex is the largest vertex index carrying a nonzero barycentric coordinate. Applied to every vertex of the recursive one-step cylinder, it selects a coarse endpoint vertex. Pushing barycentric weights through this finite selector gives an explicit coarse-simplex barycentric point. Consequently every affine combination of selected endpoint values is exactly a value of the supplied endpoint PL approximation and is therefore zero-free.

The global descent condition requires these local choices to agree for occurrences of the same geometric stack vertex in different refined top cells. This overlap compatibility yields an Assignment on the quotient of global collar vertices.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.deltaSupport {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : Finset (Fin (d + 1))

Nonzero barycentric-coordinate support of a point of the standard simplex.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.deltaSupport x = {i : Fin (d + 1) | x i ≠ 0}

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.mem_deltaSupport_iff {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) (i : Fin (d + 1)) : i ∈ deltaSupport x ↔ x i ≠ 0

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.deltaSupport_nonempty {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : (deltaSupport x).Nonempty

A standard-simplex point has nonempty coordinate support.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : Fin (d + 1)

Largest index in the nonzero barycentric support.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex_mem {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : lastSupportIndex x ∈ deltaSupport x

The selected last support index is genuinely in the support.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex_ne_zero {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) : x (lastSupportIndex x) ≠ 0

The selected coordinate is nonzero.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex_eq_of_eq {d : ℕ} {x y : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)} (hxy : x = y) : lastSupportIndex x = lastSupportIndex y

The selector depends only on the barycentric point, so it is automatically compatible with any two local descriptions having the same standard-simplex coordinate.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.deltaSupport_vertex {d : ℕ} (i : Fin (d + 1)) : deltaSupport (SphereOddDegree.FiniteSimplex.vertex i) = {i}

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex_vertex {d : ℕ} (i : Fin (d + 1)) : lastSupportIndex (SphereOddDegree.FiniteSimplex.vertex i) = i

The last-support selector fixes every original simplex vertex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.lastSupportIndex_ne_of_coordinate_eq_zero {d : ℕ} (x : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)) (k : Fin (d + 1)) (hk : x k = 0) : lastSupportIndex x ≠ k

If one coordinate vanishes, the last-support selector cannot choose that coordinate.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.localLastIndex (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (i : Fin (d + 2)) : Fin (d + 1)

Coarse endpoint vertex selected at a local vertex of the recursive one-step cylinder.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.localLastIndex_lower (d : ℕ) (i : Fin (d + 1)) : localLastIndex d (RelativeSubdivisionCylinderCombinatorics.lowerCell d) i.succ = i

The selector fixes the coarse lower-boundary vertices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.localLastIndex_eq_of_spatial_eq {d : ℕ} {q r : RelativeSubdivisionCylinderCombinatorics.Cell d} {i j : Fin (d + 2)} (h : (RelativeSubdivisionCylinderCombinatorics.vertex d q i).1 = (RelativeSubdivisionCylinderCombinatorics.vertex d r j).1) : localLastIndex d q i = localLastIndex d r j

Local occurrences with the same spatial barycentric point have the same selected index.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.localLastIndex_side_ne_deleted (d : ℕ) (k : Fin (d + 2)) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (i : Fin (d + 2)) : localLastIndex (d + 1) (RelativeSubdivisionCylinderCombinatorics.sideCell d k q) i.succ ≠ k

Every non-apex vertex of a recursively embedded side selects a vertex of that side.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.endpointIndex {p : ℕ} (hp : Nat.Prime p) (q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (i : Fin (p + 1)) : Fin (p - 1 + 1)

Reinterpret the selected local index in the ambient p-vertex endpoint simplex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.retractedWeight (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta d)

Push the barycentric weights of a cylinder cell through its finite last-vertex selector.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.endpointCylinderWeight {p : ℕ} (hp : Nat.Prime p) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1 + 1))

Transport ambient endpoint weights to the recursive cylinder's vertex indexing.

Equations

• NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.endpointCylinderWeight hp w = ⟨fun (i : Fin (p - 1 + 1 + 1)) => w (Fin.cast ⋯ i), ⋯⟩

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.endpointRetractedWeight {p : ℕ} (hp : Nat.Prime p) (q : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (p - 1))

Retraction specialized to the ambient prime-cardinality simplex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.retractedWeight_lower_apply_of_zero (d : ℕ) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (hzero : w 0 = 0) (j : Fin (d + 1)) : (retractedWeight d (RelativeSubdivisionCylinderCombinatorics.lowerCell d) w) j = w j.succ

On the lower boundary facet, pushing weights through the selector is exactly the original coarse barycentric coordinate vector.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.upperLastIndex (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (i : Fin (d + 1)) : Fin (d + 1)

Last-vertex map on the vertices of one barycentric top simplex.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.localLastIndex_upper (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (i : Fin (d + 1)) : localLastIndex d (RelativeSubdivisionCylinderCombinatorics.upperCell d pi) i.succ = upperLastIndex d pi i

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.retractedWeight_upper_apply_of_zero (d : ℕ) (pi : Equiv.Perm (Fin (d + 1))) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (hzero : w 0 = 0) (j : Fin (d + 1)) : (retractedWeight d (RelativeSubdivisionCylinderCombinatorics.upperCell d pi) w) j = ∑ i : Fin (d + 1), if upperLastIndex d pi i = j then w i.succ else 0

On an upper boundary facet, the retracted weights are the pushforward by the ordinary last-vertex map of that barycentric simplex.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.affine_sum_selected_eq_retracted {n : ℕ} (d : ℕ) (q : RelativeSubdivisionCylinderCombinatorics.Cell d) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta (d + 1))) (V : Fin (d + 1) → Fin n → ℝ) : (fun (c : Fin n) => ∑ i : Fin (d + 2), w i * V (localLastIndex d q i) c) = fun (c : Fin n) => ∑ j : Fin (d + 1), (retractedWeight d q w) j * V j c

Regrouping identity for affine values after the last-vertex retraction.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.affine_selectedEndpointValue_eq_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (N : ℕ) (hN : N = A.level) (q : RefinedAffineMap.TopCell hp N) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : (fun (c : Fin p) => ∑ i : Fin (p + 1), w i * A.map (RefinedAffineMap.vertex hp N q (endpointIndex hp r i)) c) = RefinedAffineMap.value hp N A.map q (StandardSimplex.ofDelta (endpointRetractedWeight hp r w))

The local affine interpolation of selected endpoint values is exactly an endpoint PL value at an explicit retracted barycentric point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackLastVertexCore.affine_selectedEndpointValue_ne_zero {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : RefinedAffineMap.TopCell hp A.level) (r : RelativeSubdivisionCylinderCombinatorics.Cell (p - 1)) (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) : (fun (c : Fin p) => ∑ i : Fin (p + 1), w i * A.map (RefinedAffineMap.vertex hp A.level q (endpointIndex hp r i)) c) ≠ 0

Every simplex-local one-step endpoint-stack cell obtained from the last-vertex selector avoids the origin. This is the quantitative geometric core of the endpoint-stack construction.