Route B: the actual selected local vector block

This file records the collar-specific fact required by the vector-fiber repair of Steps 4 and 5. At one local vertex, the p coordinate sites determine p distinct scalar-orbit parameters. Moreover, frozen status depends only on the geometric vertex, not on the coordinate.

The proof uses the vertex_orbit_injective field of RelativeAffineCellSystem; it does not assume freeness of the quotient action without justification.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.localParameter_injective {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) : Function.Injective fun (z : Fin (p + 1) × Fin p) => RelativeGenericity.localParameter hp C q z.1 z.2

The local scalar-orbit parameter map is injective in both the vertex and coordinate indices.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.isFrozenParameter_localParameter_iff {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (i : Fin (p + 1)) (j : Fin p) : Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C q i j) ↔ IsHorizontalPoint (C.vertex q i)

Frozen status of a local scalar parameter is independent of its coordinate index.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.localParameter_movable_of_one_coordinate {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (q : C.Cell) (i : Fin (p + 1)) (j₀ j : Fin p) (h : ¬Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C q i j₀)) : ¬Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C q i j)

If one coordinate at a local vertex is movable, then every coordinate at that vertex is movable.

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.vectorParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (j : Fin p) : Parameters.MovableParameter hp C

The complete movable p-coordinate block belonging to the retained local vertex selected by a mixed-face case.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.vectorParameter_injective {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Function.Injective (vectorParameter hp C κ)

The selected vector block consists of pairwise distinct movable orbit parameters.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.vectorParameter_coordinate {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : vectorParameter hp C κ κ.coordinate = selectedParameter hp C κ

The scalar parameter used in Step 4 is one coordinate of the full selected vector block.