Global descent interface for the endpoint-stack last-vertex assignment

The local last-vertex map from EndpointStackLastVertexCore assigns a coarse endpoint value to each local vertex occurrence of one one-step subdivision cylinder. To obtain a genuine collar assignment these local values must agree on every pair of symmetry-decorated occurrences which represent the same geometric cylinder point.

This file packages that exact compatibility condition, proves that it is sufficient to descend the local values to the global vertex quotient and then to the diagonal scalar-parameter quotient, and recovers the local cell values and cellwise origin avoidance. No compatibility assumption is hidden: the required compatibility theorem is OneStepLastVertexCompatible.

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.Cells {p : ℕ} (hp : Nat.Prime p) (N : ℕ) : ExplicitAffineRelativeCollar.RelativeAffineCellSystem hp N (N + 1) (N + 1) 0

The one-step endpoint cylinder used throughout this module.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.selectedPoint {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : (Cells hp A.level).VertexSlot) : Realization p

Coarse endpoint realization vertex selected at one local one-step-cylinder occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.decoratedSelectedPoint {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp A.level)) : Realization p

Selected endpoint point on a symmetry-decorated occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.selectedVector {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : (Cells hp A.level).VertexSlot) : Fin p → ℝ

Coarse endpoint value selected at one local one-step-cylinder vertex occurrence.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.decoratedSelectedVector {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp A.level)) : Fin p → ℝ

Value on a symmetry-decorated local occurrence.

Equations

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

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.OneStepLastVertexPointCompatible {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) : Prop

Pure geometric compatibility statement for the endpoint-stack last-vertex retraction. Two decorated occurrences of one global cylinder vertex must select the same decorated endpoint realization vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.decoratedSelectedVector_eq_map {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp A.level)) : decoratedSelectedVector hp A s = A.map (decoratedSelectedPoint hp A s)

Decorated selected vectors are samples of the global approximation map at decorated selected points.

def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.OneStepLastVertexCompatible {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) : Prop

Exact global overlap condition required for the local last-vertex values to descend.

This is the simplicial-carrier compatibility theorem in value form. It says that two decorated local occurrences representing the same geometric cylinder point select the same equivariant endpoint value.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.oneStepLastVertexCompatible_of_pointCompatible {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hpoint : OneStepLastVertexPointCompatible hp A) : OneStepLastVertexCompatible hp A

The geometric point-compatibility theorem implies the value-compatibility theorem.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.globalSelectedVector {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (Cells hp A.level) → Fin p → ℝ

Under the exact overlap theorem, the selected vectors descend to global collar vertices.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.globalSelectedVector_mk {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp A.level)) : globalSelectedVector hp A hcompat ⟦s⟧ = decoratedSelectedVector hp A s

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.globalSelectedVector_smul {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (g : ↥(PrimeSymmetry p)) (x : ExplicitAffineRelativeCollar.Parameters.GlobalVertex hp (Cells hp A.level)) : globalSelectedVector hp A hcompat (g • x) = g • globalSelectedVector hp A hcompat x

The descended global vector assignment is prime-equivariant.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.selectedSiteValue {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (s : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (Cells hp A.level)) : ℝ

Scalar site value obtained from the descended global vector assignment.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.selectedSiteValue_eq_of_orbitRel {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) {a b : ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (Cells hp A.level)} (hab : (MulAction.orbitRel (↥(PrimeSymmetry p)) (ExplicitAffineRelativeCollar.Parameters.ScalarSite hp (Cells hp A.level))) a b) : selectedSiteValue hp A hcompat a = selectedSiteValue hp A hcompat b

The selected scalar site value is constant on diagonal prime orbits.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.assignment {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) : ExplicitAffineRelativeCollar.Parameters.Assignment hp (Cells hp A.level)

Genuine compatible equivariant assignment obtained from the local last-vertex values.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.vectorValue_assignment_sample {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (s : (Cells hp A.level).VertexSlot) : ExplicitAffineRelativeCollar.Parameters.vectorValue hp (Cells hp A.level) (assignment hp A hcompat) (ExplicitAffineRelativeCollar.Parameters.sampleVertex hp (Cells hp A.level) s) = selectedVector hp A s

The descended assignment reconstructs the intended selected value at every local slot.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.localVertexMap_assignment_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (q : (Cells hp A.level).Cell) (i : Fin (p + 1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp A.level) (assignment hp A hcompat) q).value i = A.map (RefinedAffineMap.vertex hp A.level q.1 (EndpointStackLastVertexCore.endpointIndex hp q.2 i))

Local vertex map of the descended assignment is exactly the simplex-local last-vertex map.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackGlobalDescent.assignment_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepLastVertexCompatible hp A) (q : (Cells hp A.level).Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp A.level) (assignment hp A hcompat) q).AvoidsOrigin

Every one-step endpoint-stack cell of the globally descended assignment avoids the origin.