Coordinate lift of the S5 reference deviation map

The S5 model is expressed in fixed difference coordinates. This module adds one full coordinate whose value is fixed, producing a coordinate-valued affine map with exactly the same deviation map and the same positive local-index cochain.

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

S5 reference data expressed as a coordinate-valued affine map.

Equations

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

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

The deviation of the coordinate reference map is exactly the S5 reference map.

theorem NRR.AAK.referenceCoordinateMap_value_eq_one_of_deviation_zero {p : ℕ} (hp : Nat.Prime p) (s : FoxNeuwirthOrderComplex.Simplex p (p - 1)) (w : StandardSimplex (p - 1)) (hzero : ∀ (r : Fin (p - 1)), (FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.deviation hp (referenceCoordinateMap hp)).value s w r = 0) (i : Fin p) : (referenceCoordinateMap hp).value s w i = 1

At a deviation zero of the lifted reference map, every full coordinate equals one.

theorem NRR.AAK.referenceCoordinateMap_hasPositive_iff {p : ℕ} (hp : Nat.Prime p) (s : FoxNeuwirthOrderComplex.Simplex p (p - 1)) : FoxNeuwirthOrderComplex.CoordinateAffineVertexMap.HasPositiveInteriorZero hp (referenceCoordinateMap hp) s ↔ (FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.referenceMap hp).HasInteriorZero s

Positive zeros of the lifted reference map are exactly the ordinary S5 reference zeros.

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

The positive-index cochain of the coordinate lift is the S5 reference-index cochain.