Explicit refined approximations at the two reference endpoints

The refined approximation interface permits level zero. At level zero the refined chart is the original maximal-simplex chart, so sampling a globally affine vertex map and extending it affinely recovers the same map. This gives explicit regular approximations of both shifted S5 reference lifts. The positive lift has exactly the S5 orbit count; the negative lift has no positive-ray intersections.

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.zeroRefinementWord (p : ℕ) : RefinementWord p 0

The unique level-zero refinement word.

Equations

• NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.zeroRefinementWord p i = i.elim0

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.refinementWord_zero_eq {p : ℕ} (rho : RefinementWord p 0) : rho = zeroRefinementWord p

Every level-zero refinement word is the canonical empty word.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.chart_zero {p : ℕ} (hp : Nat.Prime p) (q : TopCell hp 0) : chart hp 0 q = (ReferenceAffineOrbitCount.topRepr hp q.1).realizationContinuousMap

A level-zero refined chart is the original maximal-simplex chart.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.value_zero_ofCoordinateAffineVertexMap {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (q : TopCell hp 0) (w : StandardSimplex (p - 1)) : value hp 0 (ofCoordinateAffineVertexMap F) q w = F.globalValue ((chart hp 0 q) (StandardSimplex.toDelta w))

At level zero, sampling and affine interpolation recover an original affine vertex map.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.determinant_zero_ofCoordinateAffineVertexMap {p : ℕ} (hp : Nat.Prime p) (F : CoordinateAffineVertexMap p) (q : TopCell hp 0) : determinant hp 0 (ofCoordinateAffineVertexMap F) q = (CoordinateAffineVertexMap.deviation hp F).determinant (ReferenceAffineOrbitCount.topRepr hp q.1)

The level-zero determinant of an original affine vertex map is its ordinary simplex determinant.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.positiveReference_localIndex_zero {p : ℕ} (hp : Nat.Prime p) (q : TopCell hp 0) : localIndex hp 0 (ofCoordinateAffineVertexMap (AAK.positiveEquivariantReferenceCoordinateMap hp)) q = ReferenceAffineOrbitCount.referenceIndex hp q.1

Positive-reference local indices at level zero are exactly the S5 reference indices.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.positiveReference_zeroCount_zero {p : ℕ} (hp : Nat.Prime p) : zeroCount hp 0 (ofCoordinateAffineVertexMap (AAK.positiveEquivariantReferenceCoordinateMap hp)) = (PrimeOrbitCycle.orbitCycle hp).zeroCount (ReferenceAffineOrbitCount.referenceIndex hp)

The positive level-zero refined count is the S5 reference orbit count.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.negativeReference_localIndex_zero {p : ℕ} (hp : Nat.Prime p) (q : TopCell hp 0) : localIndex hp 0 (ofCoordinateAffineVertexMap (AAK.negativeEquivariantReferenceCoordinateMap hp)) q = 0

The negative shifted reference has no positive local intersection on any level-zero top simplex.

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.negativeReference_zeroCount_zero {p : ℕ} (hp : Nat.Prime p) : zeroCount hp 0 (ofCoordinateAffineVertexMap (AAK.negativeEquivariantReferenceCoordinateMap hp)) = 0

The negative level-zero refined count is zero.

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.positiveReferenceApproximation {p : ℕ} (hp : Nat.Prime p) : RegularApproximation hp (ofCoordinateAffineVertexMap (AAK.positiveEquivariantReferenceCoordinateMap hp))

Explicit regular approximation of the positive reference lift.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.negativeReferenceApproximation {p : ℕ} (hp : Nat.Prime p) : RegularApproximation hp (ofCoordinateAffineVertexMap (AAK.negativeEquivariantReferenceCoordinateMap hp))

Explicit regular approximation of the negative reference lift.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.positiveReferenceApproximation_zeroCount {p : ℕ} (hp : Nat.Prime p) : (positiveReferenceApproximation hp).zeroCount = (PrimeOrbitCycle.orbitCycle hp).zeroCount (ReferenceAffineOrbitCount.referenceIndex hp)

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.RefinedAffineMap.negativeReferenceApproximation_zeroCount {p : ℕ} (hp : Nat.Prime p) : (negativeReferenceApproximation hp).zeroCount = 0