Route B: canonical split of the selected local vector block

For a MixedFaceCase, the p scalar coordinates at the selected retained vertex are pairwise distinct movable quotient-orbit parameters. This file uses their range as a canonical selected index subtype and splits the complete movable product into selected and complementary coordinates.

This construction requires no additional coordinate-equivalence hypothesis.

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

Predicate selecting precisely the p movable scalar-orbit parameters of one retained local vertex.

Equations

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

@[instance_reducible]

noncomputable instance NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.isSelectedVectorParameterDecidable {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : DecidablePred (IsSelectedVectorParameter hp C κ)

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.SelectedVectorParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Type

The selected scalar-orbit index subtype.

Equations

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

@[reducible, inline]

abbrev NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.RemainingMovableParameter {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : Type

The complementary movable scalar-orbit index subtype.

Equations

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

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

The coordinate map is an equivalence from Fin p onto the selected range.

Equations

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

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.vectorParameterEquiv_apply_val {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (j : Fin p) : ↑((vectorParameterEquiv hp C κ) j) = vectorParameter hp C κ j

noncomputable def NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : MovableParameterSpace hp C ≃ᵐ (SelectedVectorParameter hp C κ → ℝ) × (RemainingMovableParameter hp C κ → ℝ)

Canonical measurable coordinate split into the selected block and its complement.

Equations

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

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit_measurePreserving {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) : MeasureTheory.MeasurePreserving (⇑(parameterSplit hp C κ)) MeasureTheory.volume MeasureTheory.volume

The canonical split preserves finite-product Lebesgue measure.

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit_apply_selected {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (x : MovableParameterSpace hp C) (q : SelectedVectorParameter hp C κ) : ((parameterSplit hp C κ) x).1 q = x ↑q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit_apply_remaining {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (x : MovableParameterSpace hp C) (q : RemainingMovableParameter hp C κ) : ((parameterSplit hp C κ) x).2 q = x ↑q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit_symm_apply_selected {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (y : (SelectedVectorParameter hp C κ → ℝ) × (RemainingMovableParameter hp C κ → ℝ)) (q : SelectedVectorParameter hp C κ) : (parameterSplit hp C κ).symm y ↑q = y.1 q

@[simp]

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.parameterSplit_symm_apply_remaining {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (y : (SelectedVectorParameter hp C κ → ℝ) × (RemainingMovableParameter hp C κ → ℝ)) (q : RemainingMovableParameter hp C κ) : (parameterSplit hp C κ).symm y ↑q = y.2 q

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

The local parameter at the selected vertex and coordinate j belongs to the selected block.

theorem NRR.FoxNeuwirthOrderComplex.EquivariantPrismStableRelativeBoundary.ExplicitAffineRelativeCollar.RouteB.MixedFaceCase.localParameter_not_selected_of_vertex_ne {p N₀ N₁ M L : ℕ} (hp : Nat.Prime p) (C : RelativeAffineCellSystem hp N₀ N₁ M L) (κ : MixedFaceCase hp C) (i : Fin (p + 1)) (hi : i ≠ κ.retained) (j : Fin p) (hmovable : ¬Parameters.IsFrozenParameter hp C (RelativeGenericity.localParameter hp C κ.cell i j)) : ¬IsSelectedVectorParameter hp C κ ⟨RelativeGenericity.localParameter hp C κ.cell i j, hmovable⟩

A local scalar site at another vertex of the same cell cannot belong to the selected block.