A globally negative coordinate lift of the S5 reference map

Subtracting a common scalar from every coordinate does not change the deviation map. The negative lift is used as the lower-end comparison map in S6. Its positive-ray count is zero, while its deviation map remains the regular S5 reference map.

noncomputable def NRR.AAK.negativeReferenceCoordinateMap {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.CoordinateAffineVertexMap p

Globally negative coordinate lift of the S5 reference deviation map.

Equations

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

theorem NRR.AAK.negativeReferenceCoordinateMap_vertex_neg {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (i : Fin p) : (negativeReferenceCoordinateMap hp).vertexValue c i < 0

theorem NRR.AAK.negativeReferenceCoordinateMap_global_neg {p : ℕ} (hp : Nat.Prime p) (x : FoxNeuwirthOrderComplex.Realization p) (i : Fin p) : (negativeReferenceCoordinateMap hp).globalValue x i < 0

theorem NRR.AAK.negativeReferenceCoordinateMap_deviation {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.deviation hp (negativeReferenceCoordinateMap hp) = FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceMap hp

Subtracting a common offset leaves the deviation map unchanged.

theorem NRR.AAK.negativeReferencePositiveIndex_eq_zero {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.AffinePrismObstruction.positiveIndex hp (negativeReferenceCoordinateMap hp) = 0

The negative reference has zero positive local-index cochain.