Global descent interface for affine-pullback endpoint-stack values

The composable simplex-local convention assigns to every one-step-cylinder vertex the value of the parent endpoint PL map at that vertex's spatial barycentric point. This file packages the exact shared-face compatibility theorem needed for those values to descend through the global vertex and prime-orbit quotients. The compatibility theorem lets the quotient assignment reconstruct the simplex-local affine-pullback values, so origin avoidance follows from EndpointStackAffinePullbackEndpointStackAffinePullbackCore.affine_pullbackEndpointValue_ne_zero.

The upper values are the ordinary PL values at the next barycentric-subdivision vertices. Hence this convention is seam-compatible under iteration.

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.parentIndex (p : ℕ) : Fin (p - 1 + 1) → Fin (p - 1 + 1)

Parent vertex index used by the local affine-pullback formulas.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.cylinderIndex {p : ℕ} (hp : Nat.Prime p) : Fin (p + 1) → Fin (p - 1 + 2)

Identify global cylinder vertex indices with their local dimension-normalized indices.

Equations

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

@[reducible, inline]

noncomputable abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.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.EndpointStackAffinePullbackDescent.pullbackVector {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : (Cells hp A.level).VertexSlot) : Fin p → ℝ

Parent-PL pullback value 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.EndpointStackAffinePullbackDescent.decoratedPullbackVector {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 → ℝ

Prime-decorated local pullback value.

Equations

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

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

Exact shared-face theorem required for the affine-pullback values to define a global vertex assignment. It states the geometric carrier compatibility: parent endpoint PL formulas agree on every shared refined face and commute with the prime action.

Equations

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

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.localSpatialWeight {p : ℕ} (hp : Nat.Prime p) (N : ℕ) (s : (Cells hp N).VertexSlot) : StandardSimplex (p - 1)

Spatial standard-simplex point represented by one local one-step-cylinder vertex.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.pullbackVector_eq_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (s : (Cells hp A.level).VertexSlot) : pullbackVector hp A s = RefinedAffineMap.value hp A.level A.map s.1.1 (localSpatialWeight hp A.level s)

A local pullback vector is literally the parent refined affine value at the represented spatial point.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.oneStepAffinePullbackCompatible {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) : OneStepAffinePullbackCompatible hp A

The affine-pullback convention satisfies the required global shared-face compatibility. The proof uses the chart-independent carrier theorem and equivariance of the sampled endpoint map.

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

Compatible affine-pullback values descend to global collar vertices.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.globalPullbackVector_mk {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible hp A) (s : ExplicitAffineRelativeCollar.Parameters.CoverVertexSlot hp (Cells hp A.level)) : globalPullbackVector hp A hcompat ⟦s⟧ = decoratedPullbackVector hp A s

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

The descended global vector assignment is prime-equivariant.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.pullbackSiteValue {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible 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.EndpointStackAffinePullbackDescent.pullbackSiteValue_eq_of_orbitRel {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible 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) : pullbackSiteValue hp A hcompat a = pullbackSiteValue hp A hcompat b

The scalar site value is constant on diagonal prime orbits.

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

Genuine compatible equivariant assignment obtained from affine pullback.

Equations

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

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

Canonical one-step affine-pullback assignment, with compatibility discharged internally.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.vectorValue_assignment_sample {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible 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) = pullbackVector hp A s

The quotient assignment reconstructs the intended local pullback value.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.localVertexMap_assignment_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible 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 = EndpointStackAffinePullbackCore.pullbackVertexValue (p - 1) q.2 (fun (j : Fin (p - 1 + 1)) => A.map (RefinedAffineMap.vertex hp A.level q.1 (parentIndex p j))) (cylinderIndex hp i)

Local vertex values of the descended assignment are exactly the simplex-local affine pullback.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.assignment_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (hcompat : OneStepAffinePullbackCompatible 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 affine-pullback cell of the descended assignment avoids the origin.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.localVertexMap_canonicalAssignment_value {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : (Cells hp A.level).Cell) (i : Fin (p + 1)) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp A.level) (canonicalAssignment hp A) q).value i = EndpointStackAffinePullbackCore.pullbackVertexValue (p - 1) q.2 (fun (j : Fin (p - 1 + 1)) => A.map (RefinedAffineMap.vertex hp A.level q.1 (parentIndex p j))) (cylinderIndex hp i)

Local values of the canonical assignment use the affine-pullback formula.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.EndpointStackAffinePullbackDescent.canonicalAssignment_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) {F : RefinedAffineMap.ContinuousCoordinateMap p} (A : RefinedAffineMap.RegularApproximation hp F) (q : (Cells hp A.level).Cell) : (ExplicitAffineRelativeCollar.Polynomials.localVertexMap hp (Cells hp A.level) (canonicalAssignment hp A) q).AvoidsOrigin

Every cell of the canonical one-step assignment avoids the origin.