Equivariant full-coordinate lift of the S5 reference map

The fixed-last-coordinate lift is convenient for calculations but obscures equivariance. Here the reference map is lifted before choosing difference coordinates: non-top cells use all block indices, while top cells use the full triangular rank vector. Taking differences against the last label recovers exactly the S5 map. Relabelling acts by the same coordinate permutation, so this lift is genuinely prime-equivariant.

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

Equivariant full-coordinate lift of the S5 affine reference map.

Equations

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

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

Its fixed difference-coordinate map is the S5 reference map.

theorem NRR.AAK.equivariantReferenceCoordinateMap_vertex_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (c : BarredPermutation p) (i : Fin p) : (equivariantReferenceCoordinateMap hp).vertexValue (g • c) i = (equivariantReferenceCoordinateMap hp).vertexValue c ((Equiv.symm ((PrimeSymmetry.toPerm p) g)) i)

Vertex data transform by coordinate relabelling.

theorem NRR.AAK.equivariantReferenceCoordinateMap_global_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (x : FoxNeuwirthOrderComplex.Realization p) : (equivariantReferenceCoordinateMap hp).globalValue (g • x) = g • (equivariantReferenceCoordinateMap hp).globalValue x

The global full-coordinate reference map is prime-equivariant.

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

A finite uniform vertex bound for the equivariant lift.

Equations

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

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

theorem NRR.AAK.equivariantReference_vertex_lt_bound {p : ℕ} (hp : Nat.Prime p) (c : BarredPermutation p) (i : Fin p) : |(equivariantReferenceCoordinateMap hp).vertexValue c i| < equivariantReferenceAbsBound hp

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

Globally positive equivariant reference lift.

Equations

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

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

Globally negative equivariant reference lift.

Equations

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

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

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

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

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

theorem NRR.AAK.positiveEquivariantReferenceCoordinateMap_global_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (x : FoxNeuwirthOrderComplex.Realization p) : (positiveEquivariantReferenceCoordinateMap hp).globalValue (g • x) = g • (positiveEquivariantReferenceCoordinateMap hp).globalValue x

theorem NRR.AAK.negativeEquivariantReferenceCoordinateMap_global_smul {p : ℕ} (hp : Nat.Prime p) (g : ↥(PrimeSymmetry p)) (x : FoxNeuwirthOrderComplex.Realization p) : (negativeEquivariantReferenceCoordinateMap hp).globalValue (g • x) = g • (negativeEquivariantReferenceCoordinateMap hp).globalValue x

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

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

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

Positive local indices agree with S5 because the deviation is unchanged.