A globally positive coordinate lift of the S5 reference map

Adding the same scalar to every coordinate does not change the deviation map. We choose a finite vertex-wise offset large enough that the full coordinate lift is strictly positive on the entire order-complex realization. This gives a manifestly zero-free straight-line homotopy from the upper child map to the reference obstruction map.

noncomputable def NRR.AAK.referenceCoordinateAbsBound {p : ℕ} (hp : Nat.Prime p) : ℝ

A finite bound for all coordinates of the original reference coordinate lift at vertices.

Equations

• NRR.AAK.referenceCoordinateAbsBound hp = 1 + ∑ c : NRR.BarredPermutation p, ∑ i : Fin p, |(NRR.AAK.referenceCoordinateMap hp).vertexValue c i|

theorem NRR.AAK.referenceCoordinateAbsBound_pos {p : ℕ} (hp : Nat.Prime p) : 0 < referenceCoordinateAbsBound hp

theorem NRR.AAK.referenceCoordinate_vertex_lt_bound {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (i : Fin p) : |(referenceCoordinateMap hp).vertexValue c i| < referenceCoordinateAbsBound hp

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

Globally positive coordinate lift of the S5 reference deviation map.

Equations

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

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

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

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

Adding a common offset leaves the deviation map unchanged.

theorem NRR.AAK.positiveReferenceIndex_eq_referenceIndex {p : ℕ} (hp : Nat.Prime p) : FoxNeuwirthOrderComplex.AffinePrismObstruction.positiveIndex hp (positiveReferenceCoordinateMap hp) = FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceIndex hp

Positive local indices of the shifted reference map equal the S5 reference indices.