Affine prism obstruction on the prime-orbit cycle

This module isolates the exact finite-dimensional content of Step S6.

For a coordinate-valued affine map on the Fox--Neuwirth order complex, the zero-sum part is represented in fixed difference coordinates. A zero of the difference map has a well-defined common coordinate mean. The obstruction counts, with the S4 cycle coefficients and the local orientation index, only those zeros whose common mean is positive.

At the lower endpoint every child value is negative, so the positive count is zero. At the upper endpoint every child value is positive, so the positive count agrees with the ordinary deviation zero count. A finite affine prism supplies an incidence transgression between the positive-index cochains at its endpoints; finite Stokes then proves equality of the orbit counts.

The final structure in this file records only the two transgression statements still required from an equivariant affine approximation: local prisms away from the projected full-zero set and an upper-end prism from the S5 reference map. It does not contain a separator or assume local constancy as a field.

theorem NRR.StandardSimplex.exists_pos {d : ℕ} (w : StandardSimplex d) : ∃ (i : Fin (d + 1)), 0 < ↑w i

Every barycentric point has at least one strictly positive coordinate.

structure NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap (p : ℕ) : Type

Coordinate-valued vertex data, before splitting into deviation and mean.

• vertexValue : BarredPermutation p → Fin p → ℝ

  The coordinate vector assigned to each barred-permutation vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.value {p : ℕ} (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) : Fin p → ℝ

Affine interpolation of the full coordinate vector on one maximal simplex.

Equations

• F.value s w i = ∑ j : Fin (p - 1 + 1), ↑w j * F.vertexValue (↑s j) i

noncomputable def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.globalValue {p : ℕ} (F : CoordinateAffineVertexMap p) (x : Realization p) : Fin p → ℝ

Global piecewise-affine coordinate map on the barycentric realization.

Equations

• F.globalValue x i = ∑ c : NRR.BarredPermutation p, ↑x c * F.vertexValue c i

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.globalValue_vertex {p : ℕ} (F : CoordinateAffineVertexMap p) (c : BarredPermutation p) : F.globalValue (Realization.vertex c) = F.vertexValue c

The global affine map agrees with the vertex data on realization vertices.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.continuous_globalValue {p : ℕ} (F : CoordinateAffineVertexMap p) : Continuous F.globalValue

The global affine map is continuous on the finite barycentric realization.

noncomputable def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.deviation {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) : AffineVertexMap p (p - 1)

Fixed difference-coordinate representation of the zero-sum/deviation part.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.mean (p : ℕ) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) : ℝ

Mean of the affine coordinate vector.

Equations

• NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.mean p F s w = (NRR.coordinateMean p) (F.value s w)

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.deviation_value_apply {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (r : Fin (p - 1)) : (deviation hp F).value s w r = F.value s w (ReferenceAffineOrbitCount.coordinateLabel hp r) - F.value s w (ReferenceAffineOrbitCount.lastLabel hp)

Difference coordinates commute with affine interpolation.

def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.HasPositiveInteriorZero {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) : Prop

A positive zero is a relative-interior zero of the deviation map at which the common coordinate mean is positive.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.hasPositiveInteriorZeroDecidable {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) : Decidable (HasPositiveInteriorZero hp F s)

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.positiveLocalZeroIndex {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) : ZMod p

Signed local contribution of a positive deviation zero.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.value_neg_of_vertex_neg {p : ℕ} (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (hneg : ∀ (c : BarredPermutation p) (i : Fin p), F.vertexValue c i < 0) (i : Fin p) : F.value s w i < 0

If every coordinate at every vertex is negative, every affine coordinate is negative.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.value_pos_of_vertex_pos {p : ℕ} (F : CoordinateAffineVertexMap p) (s : Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (hpos : ∀ (c : BarredPermutation p) (i : Fin p), 0 < F.vertexValue c i) (i : Fin p) : 0 < F.value s w i

If every coordinate at every vertex is positive, every affine coordinate is positive.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.not_hasPositiveInteriorZero_of_vertex_neg {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (hneg : ∀ (c : BarredPermutation p) (i : Fin p), F.vertexValue c i < 0) (s : Simplex p (p - 1)) : ¬HasPositiveInteriorZero hp F s

A coordinatewise-negative affine map has no positive zero.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.hasPositiveInteriorZero_iff_of_vertex_pos {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (hpos : ∀ (c : BarredPermutation p) (i : Fin p), 0 < F.vertexValue c i) (s : Simplex p (p - 1)) : HasPositiveInteriorZero hp F s ↔ (deviation hp F).HasInteriorZero s

For a coordinatewise-positive affine map, every deviation zero has positive mean.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.positiveLocalZeroIndex_eq_zero_of_vertex_neg {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (hneg : ∀ (c : BarredPermutation p) (i : Fin p), F.vertexValue c i < 0) (s : Simplex p (p - 1)) : positiveLocalZeroIndex hp F s = 0

Negative endpoint local indices vanish.

theorem NRR.FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.positiveLocalZeroIndex_eq_localZeroIndex_of_vertex_pos {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (hpos : ∀ (c : BarredPermutation p) (i : Fin p), 0 < F.vertexValue c i) (s : Simplex p (p - 1)) : positiveLocalZeroIndex hp F s = (deviation hp F).localZeroIndex s

At a positive endpoint the positive local index is the ordinary deviation local index.

noncomputable def NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.positiveIndex {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) : PrimeOrbitCycle.TopOrbit hp → ZMod p

Positive local-index cochain on the S4 top-orbit representatives.

Equations

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

structure NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.Transgression {p : ℕ} (hp : Nat.Prime p) (F₀ F₁ : CoordinateAffineVertexMap p) : Type

An affine prism transgression is the finite Stokes datum produced by the signed zero set in one parameter prism.

• facetIndex : PrimeOrbitCycle.FacetOrbit hp → ZMod p

  Facet-orbit indices whose coboundary records the change of positive index.

• index_difference : positiveIndex hp F₁ - positiveIndex hp F₀ = (PrimeOrbitCycle.orbitCycle hp).coboundary self.facetIndex

theorem NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.Transgression.zeroCount_eq {p : ℕ} {hp : Nat.Prime p} {F₀ F₁ : CoordinateAffineVertexMap p} (H : Transgression hp F₀ F₁) : (PrimeOrbitCycle.orbitCycle hp).zeroCount (positiveIndex hp F₀) = (PrimeOrbitCycle.orbitCycle hp).zeroCount (positiveIndex hp F₁)

An affine prism preserves the positive orbit count.

structure NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.LocalPrismFamily {p : ℕ} {X : Type u_1} [TopologicalSpace X] (hp : Nat.Prime p) (carrier : Set X) : Type u_1

A complement-index family equipped with local affine prisms. The local prism relation is strictly stronger than the desired local constancy of the scalar count.

• map (z : X) : z ∈ carrierᶜ → CoordinateAffineVertexMap p

  The coordinate-valued vertex map assigned to each point outside the excluded carrier.

• local_prism (z : X) (hz : z ∈ carrierᶜ) : ∃ (U : Set X) (hUout : U ⊆ carrierᶜ), IsOpen U ∧ z ∈ U ∧ ∀ (w : X) (hw : w ∈ U), Nonempty (Transgression hp (self.map z hz) (self.map w ⋯))

noncomputable def NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.LocalPrismFamily.value {p : ℕ} {X : Type u_1} [TopologicalSpace X] {hp : Nat.Prime p} {carrier : Set X} (D : LocalPrismFamily hp carrier) (z : X) (hz : z ∈ carrierᶜ) : ZMod p

Scalar orbit obstruction value.

Equations

• D.value z hz = (NRR.FoxNeuwirthOrderComplex.PrimeOrbitCycle.orbitCycle hp).zeroCount (NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.positiveIndex hp (D.map z hz))

theorem NRR.FoxNeuwirthOrderComplex.AffinePrismObstruction.LocalPrismFamily.locally_constant {p : ℕ} {X : Type u_1} [TopologicalSpace X] {hp : Nat.Prime p} {carrier : Set X} (D : LocalPrismFamily hp carrier) (z : X) (hz : z ∈ carrierᶜ) : ∃ (U : Set X) (hUout : U ⊆ carrierᶜ), IsOpen U ∧ z ∈ U ∧ ∀ (w : X) (hw : w ∈ U), D.value w ⋯ = D.value z hz

Finite Stokes makes the scalar obstruction locally constant.

noncomputable def NRR.FoxNeuwirthOrderComplex.childCoordinateVertexMap {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (z : BodySpace K A × ↑SignedInterval) : CoordinateAffineVertexMap p

Vertex sampling of the actual child test map on the order-complex vertices.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.childCoordinateVertexMap_left_neg {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (c : BarredPermutation p) (i : Fin p) : (childCoordinateVertexMap hp hA phi (C, SignedInterval.left)).vertexValue c i < 0

Vertex values are strictly negative at the lower endpoint.

theorem NRR.FoxNeuwirthOrderComplex.childCoordinateVertexMap_right_pos {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) (c : BarredPermutation p) (i : Fin p) : 0 < (childCoordinateVertexMap hp hA phi (C, SignedInterval.right)).vertexValue c i

Vertex values are strictly positive at the upper endpoint.

theorem NRR.FoxNeuwirthOrderComplex.childPositiveIndex_left_eq_zero {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : AffinePrismObstruction.positiveIndex hp (childCoordinateVertexMap hp hA phi (C, SignedInterval.left)) = 0

The lower positive-index cochain is identically zero.

theorem NRR.FoxNeuwirthOrderComplex.childPositiveIndex_right_eq_deviationIndex {p : ℕ} {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hp : Nat.Prime p) (hA : 0 < A) (phi : NiceMV (BodySpace K (A / ↑p))) (C : BodySpace K A) : AffinePrismObstruction.positiveIndex hp (childCoordinateVertexMap hp hA phi (C, SignedInterval.right)) = fun (q : PrimeOrbitCycle.TopOrbit hp) => (CoordinateAffineVertexMap.deviation hp (childCoordinateVertexMap hp hA phi (C, SignedInterval.right))).localZeroIndex (ReferenceAffineOrbitCount.topRepr hp q)

At the upper endpoint, the positive-index cochain is the ordinary deviation-index cochain.