Fine prism assignments for compatible chart homotopies

A compatible chart homotopy can be sampled on the fully refined staircase prism without first constructing a global continuous quotient map. Decorated chart compatibility is exactly the condition needed to descend local samples to global collar vertices.

Because there are finitely many base prism charts, compactness gives a positive norm margin and a uniform modulus of continuity. Iterated barycentric subdivision then makes the affine interpolation of the samples remain within half that margin. The resulting middle-prism assignment is origin-free and its two horizontal boundaries are the exact endpoint chart maps.

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.nonempty_standardSimplex (d : ℕ) : Nonempty (StandardSimplex d)

The project simplex presentation is nonempty.

instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.compactSpace_standardSimplex (d : ℕ) : CompactSpace (StandardSimplex d)

The project simplex presentation is compact.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.basePrismValue {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (q : SubdivisionPrismCharts.BasePrismCell hp N) (w : StandardSimplex p) : Fin p → ℝ

Value of a chart homotopy on one unrefined staircase chart.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.continuous_staircasePoint {p : ℕ} (hp : Nat.Prime p) (k : Fin p) : Continuous fun (w : StandardSimplex p) => SubdivisionPrismCharts.staircasePoint hp k w

The staircase chart is continuous.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.continuous_staircasePoint_ofDelta {p : ℕ} (hp : Nat.Prime p) (k : Fin p) : Continuous fun (w : ↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p)) => SubdivisionPrismCharts.staircasePoint hp k (StandardSimplex.ofDelta w)

The staircase chart is continuous in the topological-simplex presentation.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.basePrismValueMap {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (q : SubdivisionPrismCharts.BasePrismCell hp N) : C(↑(SphereOddDegree.AffineBarycentricSubdivision.Delta p), Fin p → ℝ)

Continuous base-prism value.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.refinedPrismValue {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : StandardSimplex p) : Fin p → ℝ

Value on a fully refined prism chart.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.refinedPrismValue_eq {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (w : StandardSimplex p) : refinedPrismValue hp J L q w = J.value q.1.1 (SubdivisionPrismCharts.staircasePoint hp q.1.2 (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L q.2) (StandardSimplex.toDelta w)))).1 (SubdivisionPrismCharts.staircasePoint hp q.1.2 (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L q.2) (StandardSimplex.toDelta w)))).2

The refined value is the chart homotopy evaluated at the represented prism point.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.localVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (s : (RelativeCollarMiddlePrism.cellSystem hp N L).VertexSlot) : Fin p → ℝ

Local sample at one prism vertex.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.decoratedVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (RelativeCollarMiddlePrism.cellSystem hp N L)) : Fin p → ℝ

Prime-decorated local prism sample.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.decoratedVector_eq_of_coverPoint_eq {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) {a b : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (RelativeCollarMiddlePrism.cellSystem hp N L)} (hab : ExplicitAffineRelativeCollar.Parameters.coverPoint hp (RelativeCollarMiddlePrism.cellSystem hp N L) a = ExplicitAffineRelativeCollar.Parameters.coverPoint hp (RelativeCollarMiddlePrism.cellSystem hp N L) b) : decoratedVector hp J L a = decoratedVector hp J L b

Refined prism samples agree on every shared decorated geometric vertex.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.globalVector {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (RelativeCollarMiddlePrism.cellSystem hp N L) → Fin p → ℝ

Global prism vector by quotient descent.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.globalVector_smul {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (RelativeCollarMiddlePrism.cellSystem hp N L)) : globalVector hp J L (g • x) = g • globalVector hp J L x

Equivariance of the descended middle-prism vector.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.assignment {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (RelativeCollarMiddlePrism.cellSystem hp N L)

Compatible assignment obtained from chart-homotopy samples.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.localVertexMap_assignment_value {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (i : Fin (p + 1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (assignment hp J L) q).value i = refinedPrismValue hp J L q (StandardSimplex.ofDelta (SphereOddDegree.FiniteSimplex.vertex i))

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.exists_positive_norm_margin {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) : ∃ (M : ℝ), 0 < M ∧ ∀ (q : SubdivisionPrismCharts.BasePrismCell hp N) (w : StandardSimplex p), M ≤ ‖basePrismValue hp J q w‖

A positive norm margin valid on every base chart of a compatible chart homotopy.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.exists_refinement_oscillation {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) {eps : ℝ} (heps : 0 < eps) : ∃ (L : ℕ), ∀ (q : SubdivisionPrismCharts.PrismCell hp N L) (u v : StandardSimplex p), dist (refinedPrismValue hp J L q u) (refinedPrismValue hp J L q v) < eps

Sufficient prism refinement makes every chart-homotopy value oscillate by less than eps on one refined prism cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.norm_affineValue_sub_refinedPrismValue_le {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (q : SubdivisionPrismCharts.PrismCell hp N L) (eps : ℝ) (hosc : ∀ (u v : StandardSimplex p), dist (refinedPrismValue hp J L q u) (refinedPrismValue hp J L q v) < eps) (w : StandardSimplex p) : ‖(ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (assignment hp J L) q).affineValue w - refinedPrismValue hp J L q w‖ ≤ eps

Affine interpolation of samples differs from the chart homotopy by at most the cell oscillation.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.exists_refinement_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) : ∃ (L : ℕ), ∀ (q : SubdivisionPrismCharts.PrismCell hp N L), (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (RelativeCollarMiddlePrism.cellSystem hp N L) (assignment hp J L) q).AvoidsOrigin

A sufficiently fine compatible chart-homotopy prism assignment avoids the origin on every cell.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.lower_boundary_value {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (s : (RelativeCollarMiddlePrism.cellSystem hp N L).VertexSlot) (hs : ↑((RelativeCollarMiddlePrism.cellSystem hp N L).slotPoint s).time = 0) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp N L) (assignment hp J L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (RelativeCollarMiddlePrism.cellSystem hp N L) s) = K0.value s.1.1.1 (SubdivisionPrismCharts.staircasePoint hp s.1.1.2 (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L s.1.2) (SphereOddDegree.FiniteSimplex.vertex s.2)))).1

Exact lower boundary value of the middle assignment.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.CompatibleRefinedChartHomotopyPrism.upper_boundary_value {p : ℕ} (hp : Nat.Prime p) {N : ℕ} {K0 K1 : CompatibleRefinedChartHomotopy.ChartMap hp N} (J : CompatibleRefinedChartHomotopy.ChartHomotopy hp N K0 K1) (L : ℕ) (s : (RelativeCollarMiddlePrism.cellSystem hp N L).VertexSlot) (hs : ↑((RelativeCollarMiddlePrism.cellSystem hp N L).slotPoint s).time = 1) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (RelativeCollarMiddlePrism.cellSystem hp N L) (assignment hp J L) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (RelativeCollarMiddlePrism.cellSystem hp N L) s) = K1.value s.1.1.1 (SubdivisionPrismCharts.staircasePoint hp s.1.1.2 (StandardSimplex.ofDelta ((SphereOddDegree.AffineBarycentricSubdivision.affineCompMap p L s.1.2) (SphereOddDegree.FiniteSimplex.vertex s.2)))).1

Exact upper boundary value of the middle assignment.