The affine positive-ray boundary identity

This is the local PL intersection theorem required by S6. An affine map from a p-simplex to ℝ^p, transverse on every facet and avoiding the origin, meets the open positive diagonal ray in an oriented compact interval (or not at all). Hence the signed positive-ray intersections of its oriented facets add to zero.

The proof is elementary finite-dimensional linear algebra. In fixed difference coordinates the zero set of the deviation map is an affine line. Cramer's rule identifies the signs of its facet endpoints with the alternating facet determinants. The full-origin avoidance hypothesis makes the coordinate mean have a constant sign along the interval.

structure NRR.AffinePositiveRayBoundary.VertexMap (p : ℕ) : Type

Vertex values of one affine p-simplex in the full coordinate representation.

• value : Fin (p + 1) → Fin p → ℝ

  The full coordinate vector assigned to each vertex of the affine simplex.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.affineValue {p : ℕ} (V : VertexMap p) (w : StandardSimplex p) : Fin p → ℝ

Full affine interpolation.

Equations

• V.affineValue w r = ∑ i : Fin (p + 1), ↑w i * V.value i r

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.deviation {p : ℕ} (hp : Nat.Prime p) (y : Fin p → ℝ) (r : Fin (p - 1)) : ℝ

Fixed difference coordinate.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.mean (p : ℕ) (y : Fin p → ℝ) : ℝ

Mean coordinate.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.mean p y = (NRR.coordinateMean p) y

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetValue {p : ℕ} (V : VertexMap p) (k : Fin (p + 1)) (i : Fin p) : Fin p → ℝ

Restriction to the facet omitting vertex k.

Equations

• V.facetValue k i = V.value (k.succAbove i)

def NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv {p : ℕ} (hp : Nat.Prime p) : Fin p ≃ Fin (p - 1 + 1)

Reindex the p augmented rows as the p - 1 deviation rows followed by the constant row.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp = (Fin.castOrderIso ⋯).toEquiv

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetMatrix {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : Matrix (Fin p) (Fin p) ℝ

Augmented deviation matrix of an oriented facet.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetDeterminant {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : ℝ

Facet determinant.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k = (NRR.AffinePositiveRayBoundary.VertexMap.facetMatrix hp V k).det

def NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex {p : ℕ} (i : Fin p) : Fin (p - 1 + 1)

Canonical embedding of the p facet-vertex indices into the coordinate type of StandardSimplex (p - 1). For positive p this is an equivalence; the inclusion form keeps facetAffineValue meaningful without adding a positivity hypothesis to its public API.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i = Fin.castLE ⋯ i

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetAffineValue {p : ℕ} (V : VertexMap p) (k : Fin (p + 1)) (w : StandardSimplex (p - 1)) : Fin p → ℝ

Full-coordinate affine interpolation on a facet.

Equations

• V.facetAffineValue k w r = ∑ i : Fin p, ↑w (NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i) * V.facetValue k i r

def NRR.AffinePositiveRayBoundary.VertexMap.FacetHasPositiveRayIntersection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : Prop

A relative-interior intersection of a facet with the positive diagonal ray.

Equations

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

@[instance_reducible]

noncomputable instance NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersectionDecidable {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : Decidable (FacetHasPositiveRayIntersection hp V k)

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersectionDecidable hp V k = Classical.propDecidable (NRR.AffinePositiveRayBoundary.VertexMap.FacetHasPositiveRayIntersection hp V k)

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetIndex {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : ZMod p

Signed positive-ray intersection number of one oriented facet.

Equations

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

def NRR.AffinePositiveRayBoundary.VertexMap.AvoidsOrigin {p : ℕ} (V : VertexMap p) : Prop

The affine simplex avoids the full origin.

Equations

• V.AvoidsOrigin = ∀ (w : NRR.StandardSimplex p), V.affineValue w ≠ 0

def NRR.AffinePositiveRayBoundary.VertexMap.FacetRegular {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Prop

Facet transversality.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.FacetRegular hp V = ∀ (k : Fin (p + 1)), NRR.AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k ≠ 0

def NRR.AffinePositiveRayBoundary.VertexMap.AvoidsCodimTwoDeviationZero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Prop

The deviation-zero affine line does not meet a codimension-two face of the simplex. This is the general-position condition needed to rule out a ray endpoint at the intersection of two facets. Facet regularity alone does not imply this condition.

Equations

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

def NRR.AffinePositiveRayBoundary.VertexMap.AvoidsPositiveRayCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Prop

Positive-ray-relative codimension-two avoidance. Degenerate deviation-zero points with negative mean are irrelevant to the open positive ray and are intentionally permitted.

Equations

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

structure NRR.AffinePositiveRayBoundary.VertexMap.PositiveRayGeneralPosition {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Prop

Exact local hypotheses needed by positive-ray Stokes. This is weaker than GeneralPosition: it excludes codimension-two degeneracy only on the positive part of the deviation-zero line.

• facetRegular : FacetRegular hp V
• avoidsPositiveRayCodimTwo : AvoidsPositiveRayCodimTwo hp V
• avoidsOrigin : V.AvoidsOrigin

structure NRR.AffinePositiveRayBoundary.VertexMap.GeneralPosition {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Prop

Exact local general-position hypotheses for unrestricted deviation-zero intersection theory.

• facetRegular : FacetRegular hp V
• avoidsCodimTwo : AvoidsCodimTwoDeviationZero hp V
• avoidsOrigin : V.AvoidsOrigin

theorem NRR.AffinePositiveRayBoundary.VertexMap.GeneralPosition.toPositiveRayGeneralPosition {p : ℕ} {hp : Nat.Prime p} {V : VertexMap p} (hgp : GeneralPosition hp V) : PositiveRayGeneralPosition hp V

Unrestricted codimension-two avoidance implies the positive-ray-relative condition.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.augmentedDeviationMatrix {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Matrix (Fin p) (Fin (p + 1)) ℝ

The rectangular augmented deviation matrix. Its final row is the barycentric-sum row and its preceding rows are the fixed deviation coordinates. Deleting column k gives the oriented facet matrix.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.signedMaximalMinor {p : ℕ} (A : Matrix (Fin p) (Fin (p + 1)) ℝ) (k : Fin (p + 1)) : ℝ

The signed maximal minor of a p × (p+1) matrix obtained by deleting column k.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.signedMaximalMinor A k = (-1) ^ ↑k * (A.submatrix id k.succAbove).det

theorem NRR.AffinePositiveRayBoundary.VertexMap.row_dot_signedMaximalMinor_eq_zero {p : ℕ} (A : Matrix (Fin p) (Fin (p + 1)) ℝ) (r : Fin p) : ∑ k : Fin (p + 1), A r k * signedMaximalMinor A k = 0

Laplace expansion with a repeated row: every row of a p × (p+1) matrix annihilates its vector of signed maximal minors. This is the rectangular cofactor-kernel identity used below.

theorem NRR.AffinePositiveRayBoundary.VertexMap.augmentedDeviationMatrix_minor {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : (augmentedDeviationMatrix hp V).submatrix id k.succAbove = facetMatrix hp V k

Deleting a column from the augmented deviation matrix gives the corresponding facet matrix.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : ℝ

Cofactor direction of the affine deviation-zero line.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection hp V k = (-1) ^ ↑k * NRR.AffinePositiveRayBoundary.VertexMap.facetDeterminant hp V k

theorem NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection_eq_signedMaximalMinor {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : cofactorDirection hp V k = signedMaximalMinor (augmentedDeviationMatrix hp V) k

The project cofactor direction is exactly the signed-maximal-minor vector of the augmented deviation matrix.

theorem NRR.AffinePositiveRayBoundary.VertexMap.augmentedDeviationMatrix_mul_cofactorDirection_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (r : Fin p) : ∑ k : Fin (p + 1), augmentedDeviationMatrix hp V r k * cofactorDirection hp V k = 0

Every row of the augmented deviation matrix annihilates the cofactor direction.

def NRR.AffinePositiveRayBoundary.VertexMap.constantRow {p : ℕ} (hp : Nat.Prime p) : Fin p

Index of the final (constant) row of the augmented deviation matrix.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.constantRow hp = (NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp).symm (Fin.last (p - 1))

def NRR.AffinePositiveRayBoundary.VertexMap.deviationRow {p : ℕ} (hp : Nat.Prime p) (q : Fin (p - 1)) : Fin p

Index of a deviation row in the augmented deviation matrix.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.deviationRow hp q = (NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp).symm q.castSucc

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.augmentedDeviationMatrix_constantRow {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : augmentedDeviationMatrix hp V (constantRow hp) k = 1

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.augmentedDeviationMatrix_deviationRow {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (q : Fin (p - 1)) (k : Fin (p + 1)) : augmentedDeviationMatrix hp V (deviationRow hp q) k = deviation hp (V.value k) q

theorem NRR.AffinePositiveRayBoundary.VertexMap.sum_cofactorDirection_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : ∑ k : Fin (p + 1), cofactorDirection hp V k = 0

The cofactor direction preserves the barycentric sum.

theorem NRR.AffinePositiveRayBoundary.VertexMap.weighted_deviation_sum_cofactorDirection_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (q : Fin (p - 1)) : ∑ k : Fin (p + 1), cofactorDirection hp V k * deviation hp (V.value k) q = 0

The cofactor direction lies in the kernel of every deviation row.

theorem NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection_ne_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (k : Fin (p + 1)) : cofactorDirection hp V k ≠ 0

Under facet regularity, every coordinate of the cofactor direction is nonzero.

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetMatrix_zero_apply {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (r i : Fin p) : facetMatrix hp V 0 r i = augmentedDeviationMatrix hp V r i.succ

The facet matrix omitting vertex 0 is the tail-column block of the augmented matrix.

theorem NRR.AffinePositiveRayBoundary.VertexMap.eq_zero_of_zero_at_zero_of_augmented_rows_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (z : Fin (p + 1) → ℝ) (hz0 : z 0 = 0) (hzrows : ∀ (r : Fin p), ∑ k : Fin (p + 1), augmentedDeviationMatrix hp V r k * z k = 0) : z = 0

A vector in the augmented-row kernel is zero if its zeroth coordinate is zero. The remaining coordinates form a vector annihilated by the facet matrix omitting vertex 0; facet regularity makes that square matrix nonsingular.

theorem NRR.AffinePositiveRayBoundary.VertexMap.eq_smul_cofactorDirection_of_augmented_rows_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (x : Fin (p + 1) → ℝ) (hx : ∀ (r : Fin p), ∑ k : Fin (p + 1), augmentedDeviationMatrix hp V r k * x k = 0) : ∃ (t : ℝ), x = t • cofactorDirection hp V

The augmented-row kernel is the one-dimensional span of the cofactor direction. The scalar is fixed by the zeroth coordinate; subtracting that multiple leaves a kernel vector with zeroth coordinate zero, hence the zero vector by the preceding nonsingularity lemma.

theorem NRR.AffinePositiveRayBoundary.VertexMap.eq_constantRow_or_eq_deviationRow {p : ℕ} (hp : Nat.Prime p) (r : Fin p) : r = constantRow hp ∨ ∃ (q : Fin (p - 1)), r = deviationRow hp q

Every row of the augmented matrix is either the final barycentric-sum row or one of the preceding deviation rows.

theorem NRR.AffinePositiveRayBoundary.VertexMap.deviation_affineValue_eq_weighted_sum {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (q : Fin (p - 1)) : deviation hp (V.affineValue w) q = ∑ k : Fin (p + 1), ↑w k * deviation hp (V.value k) q

Deviation commutes with barycentric affine interpolation.

theorem NRR.AffinePositiveRayBoundary.VertexMap.coordinate_eq_lastLabel_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (y : Fin p → ℝ) (hdev : ∀ (q : Fin (p - 1)), deviation hp y q = 0) (i : Fin p) : y i = y (FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lastLabel hp)

Vanishing fixed deviations force every full coordinate to equal the distinguished final coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.mean_eq_lastLabel_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (y : Fin p → ℝ) (hdev : ∀ (q : Fin (p - 1)), deviation hp y q = 0) : mean p y = y (FoxNeuwirthOrderComplex.ReferenceAffineOrbitCount.lastLabel hp)

On the fixed-deviation-zero locus, the coordinate mean is the common coordinate value.

theorem NRR.AffinePositiveRayBoundary.VertexMap.coordinateDeviation_eq_zero_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (y : Fin p → ℝ) (hdev : ∀ (q : Fin (p - 1)), deviation hp y q = 0) : (coordinateDeviation ⋯) y = 0

The standard full-coordinate deviation vanishes whenever all fixed differences vanish.

theorem NRR.AffinePositiveRayBoundary.VertexMap.coordinate_eq_zero_of_deviation_eq_zero_of_mean_eq_zero {p : ℕ} (hp : Nat.Prime p) (y : Fin p → ℝ) (hdev : ∀ (q : Fin (p - 1)), deviation hp y q = 0) (hmean : mean p y = 0) : y = 0

Fixed deviations together with zero mean determine the zero full-coordinate vector.

theorem NRR.AffinePositiveRayBoundary.VertexMap.mean_affineValue_eq_weighted_sum (p : ℕ) (V : VertexMap p) (w : StandardSimplex p) : mean p (V.affineValue w) = ∑ k : Fin (p + 1), ↑w k * mean p (V.value k)

The coordinate mean commutes with barycentric affine interpolation.

theorem NRR.AffinePositiveRayBoundary.VertexMap.sub_eq_smul_cofactorDirection_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w₀ w₁ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hw₁ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₁) q = 0) : ∃ (t : ℝ), (fun (k : Fin (p + 1)) => ↑w₁ k - ↑w₀ k) = t • cofactorDirection hp V

Two barycentric points with deviation-zero affine values differ by a scalar multiple of the cofactor direction. Their coordinate difference has barycentric sum zero and is annihilated by every deviation row, so the augmented-kernel uniqueness theorem applies.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (k : Fin (p + 1)) : ℝ

Barycentric coordinate of the cofactor line through w at parameter t.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate hp V w t k = ↑w k + t * NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection hp V k

def NRR.AffinePositiveRayBoundary.VertexMap.LineFeasible {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) : Prop

Parameters for which the cofactor line remains in the standard simplex. The barycentric sum is automatic because the cofactor direction has coordinate sum zero, so feasibility consists only of the coordinatewise nonnegativity inequalities.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.LineFeasible hp V w t = ∀ (k : Fin (p + 1)), 0 ≤ NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate hp V w t k

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.positiveCofactorIndices {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Finset (Fin (p + 1))

Indices at which the cofactor direction points into the simplex as the parameter increases.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.positiveCofactorIndices hp V = {k : Fin (p + 1) | 0 < NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection hp V k}

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.negativeCofactorIndices {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Finset (Fin (p + 1))

Indices at which the cofactor direction points out of the simplex as the parameter increases.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.negativeCofactorIndices hp V = {k : Fin (p + 1) | NRR.AffinePositiveRayBoundary.VertexMap.cofactorDirection hp V k < 0}

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_pos_cofactorDirection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) : ∃ (k : Fin (p + 1)), 0 < cofactorDirection hp V k

A nonzero vector with zero coordinate sum has a positive coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_neg_cofactorDirection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) : ∃ (k : Fin (p + 1)), cofactorDirection hp V k < 0

A nonzero vector with zero coordinate sum has a negative coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.positiveCofactorIndices_nonempty {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) : (positiveCofactorIndices hp V).Nonempty

The positive cofactor-index finset is nonempty under facet regularity.

theorem NRR.AffinePositiveRayBoundary.VertexMap.negativeCofactorIndices_nonempty {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) : (negativeCofactorIndices hp V).Nonempty

The negative cofactor-index finset is nonempty under facet regularity.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.positiveThresholds {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) : Finset ℝ

Lower-bound candidates contributed by positive cofactor coordinates.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.negativeThresholds {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) : Finset ℝ

Upper-bound candidates contributed by negative cofactor coordinates.

Equations

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

theorem NRR.AffinePositiveRayBoundary.VertexMap.positiveThresholds_nonempty {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : (positiveThresholds hp V w).Nonempty

The lower-threshold finset is nonempty.

theorem NRR.AffinePositiveRayBoundary.VertexMap.negativeThresholds_nonempty {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : (negativeThresholds hp V w).Nonempty

The upper-threshold finset is nonempty.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ℝ

Greatest lower bound imposed by the positive cofactor coordinates.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter hp V hregular w = (NRR.AffinePositiveRayBoundary.VertexMap.positiveThresholds hp V w).max' ⋯

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.upperParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ℝ

Least upper bound imposed by the negative cofactor coordinates.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.upperParameter hp V hregular w = (NRR.AffinePositiveRayBoundary.VertexMap.negativeThresholds hp V w).min' ⋯

theorem NRR.AffinePositiveRayBoundary.VertexMap.positive_threshold_le_lowerParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : 0 < cofactorDirection hp V k) : -↑w k / cofactorDirection hp V k ≤ lowerParameter hp V hregular w

Every positive-coordinate threshold lies below the chosen lower endpoint.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperParameter_le_negative_threshold {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : cofactorDirection hp V k < 0) : upperParameter hp V hregular w ≤ -↑w k / cofactorDirection hp V k

Every negative-coordinate threshold lies above the chosen upper endpoint.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_spec {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ∃ (k : Fin (p + 1)), 0 < cofactorDirection hp V k ∧ lowerParameter hp V hregular w = -↑w k / cofactorDirection hp V k

The lower endpoint is attained by a positive cofactor coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperParameter_spec {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ∃ (k : Fin (p + 1)), cofactorDirection hp V k < 0 ∧ upperParameter hp V hregular w = -↑w k / cofactorDirection hp V k

The upper endpoint is attained by a negative cofactor coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate_nonneg_iff_of_pos {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (k : Fin (p + 1)) (hk : 0 < cofactorDirection hp V k) : 0 ≤ lineCoordinate hp V w t k ↔ -↑w k / cofactorDirection hp V k ≤ t

For a positive direction coordinate, nonnegativity is the corresponding lower-bound inequality on the line parameter.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate_nonneg_iff_of_neg {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (k : Fin (p + 1)) (hk : cofactorDirection hp V k < 0) : 0 ≤ lineCoordinate hp V w t k ↔ t ≤ -↑w k / cofactorDirection hp V k

For a negative direction coordinate, nonnegativity is the corresponding upper-bound inequality on the line parameter.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineFeasible_iff_mem_Icc {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (t : ℝ) : LineFeasible hp V w t ↔ t ∈ Set.Icc (lowerParameter hp V hregular w) (upperParameter hp V hregular w)

The cofactor line meets the simplex exactly on the closed interval between the finite lower and upper parameters.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineFeasible_set_eq_Icc {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : {t : ℝ | LineFeasible hp V w t} = Set.Icc (lowerParameter hp V hregular w) (upperParameter hp V hregular w)

Set-level form of the line--simplex interval classification.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineFeasible_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) : LineFeasible hp V w 0

Parameter zero is feasible because it is the original simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_le_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lowerParameter hp V hregular w ≤ 0

The lower endpoint is at most zero.

theorem NRR.AffinePositiveRayBoundary.VertexMap.zero_le_upperParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : 0 ≤ upperParameter hp V hregular w

The upper endpoint is at least zero.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_le_upperParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lowerParameter hp V hregular w ≤ upperParameter hp V hregular w

The finite lower endpoint does not exceed the finite upper endpoint.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_feasible {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : LineFeasible hp V w (lowerParameter hp V hregular w)

The lower endpoint is feasible.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperParameter_feasible {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : LineFeasible hp V w (upperParameter hp V hregular w)

The upper endpoint is feasible.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointIndex {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : Fin (p + 1)

Chosen coordinate attaining the lower endpoint.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointIndex hp V hregular w = Classical.choose ⋯

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointIndex {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : Fin (p + 1)

Chosen coordinate attaining the upper endpoint.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointIndex hp V hregular w = Classical.choose ⋯

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointIndex_pos {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : 0 < cofactorDirection hp V (lowerEndpointIndex hp V hregular w)

The lower endpoint coordinate has positive cofactor direction.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointIndex_neg {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : cofactorDirection hp V (upperEndpointIndex hp V hregular w) < 0

The upper endpoint coordinate has negative cofactor direction.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_eq_threshold {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lowerParameter hp V hregular w = -↑w (lowerEndpointIndex hp V hregular w) / cofactorDirection hp V (lowerEndpointIndex hp V hregular w)

Formula for the lower endpoint parameter at its chosen coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperParameter_eq_threshold {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : upperParameter hp V hregular w = -↑w (upperEndpointIndex hp V hregular w) / cofactorDirection hp V (upperEndpointIndex hp V hregular w)

Formula for the upper endpoint parameter at its chosen coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_coordinate_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lineCoordinate hp V w (lowerParameter hp V hregular w) (lowerEndpointIndex hp V hregular w) = 0

The chosen lower-endpoint coordinate vanishes.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_coordinate_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lineCoordinate hp V w (upperParameter hp V hregular w) (upperEndpointIndex hp V hregular w) = 0

The chosen upper-endpoint coordinate vanishes.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (ht : LineFeasible hp V w t) : StandardSimplex p

A feasible line parameter gives a barycentric point of the standard simplex.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint hp V w t ht = ⟨fun (k : Fin (p + 1)) => NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate hp V w t k, ⋯⟩

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_apply {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (ht : LineFeasible hp V w t) (k : Fin (p + 1)) : ↑(lineSimplexPoint hp V w t ht) k = lineCoordinate hp V w t k

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate_eq_of_sub_eq_smul_cofactorDirection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w₀ w₁ : StandardSimplex p) (t : ℝ) (hsub : (fun (k : Fin (p + 1)) => ↑w₁ k - ↑w₀ k) = t • cofactorDirection hp V) (k : Fin (p + 1)) : lineCoordinate hp V w₀ t k = ↑w₁ k

A scalar-multiple description of the barycentric difference identifies the second point with its coordinatewise position on the cofactor line through the first point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_lineSimplexPoint_eq_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w₀ w₁ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hw₁ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₁) q = 0) : ∃ (t : ℝ) (ht : LineFeasible hp V w₀ t), w₁ = lineSimplexPoint hp V w₀ t ht

Every zero-deviation simplex point lies on the feasible cofactor line through any chosen zero-deviation base point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_lineParameter_mem_Icc_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w₀ w₁ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hw₁ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₁) q = 0) : ∃ t ∈ Set.Icc (lowerParameter hp V hregular w₀) (upperParameter hp V hregular w₀), ∃ (ht : LineFeasible hp V w₀ t), w₁ = lineSimplexPoint hp V w₀ t ht

Closed-interval form of the classification of all zero-deviation simplex points.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineCoordinate_parameter_unique {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) {t₀ t₁ : ℝ} (hline : (fun (k : Fin (p + 1)) => lineCoordinate hp V w t₀ k) = fun (k : Fin (p + 1)) => lineCoordinate hp V w t₁ k) : t₀ = t₁

The cofactor-line parameter is unique under facet regularity.

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_unique_lineParameter_of_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w₀ w₁ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hw₁ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₁) q = 0) : ∃! t : ℝ, ∃ (ht : LineFeasible hp V w₀ t), w₁ = lineSimplexPoint hp V w₀ t ht

The feasible cofactor-line representation of a zero-deviation simplex point is unique.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (t : ℝ) (ht : LineFeasible hp V w t) (q : Fin (p - 1)) : deviation hp (V.affineValue (lineSimplexPoint hp V w t ht)) q = 0

If the base point has zero deviation, every feasible point on the cofactor line also has zero deviation.

theorem NRR.AffinePositiveRayBoundary.VertexMap.deviation_eq_zero_iff_exists_lineSimplexPoint_eq {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w₀ w₁ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) : (∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₁) q = 0) ↔ ∃ (t : ℝ) (ht : LineFeasible hp V w₀ t), w₁ = lineSimplexPoint hp V w₀ t ht

Exact classification of the deviation-zero simplex locus by feasible cofactor-line points.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.cofactorMeanSlope {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : ℝ

Slope of the coordinate mean along the cofactor line.

Equations

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

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_mean_eq {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (t : ℝ) (ht : LineFeasible hp V w t) : mean p (V.affineValue (lineSimplexPoint hp V w t ht)) = mean p (V.affineValue w) + t * cofactorMeanSlope hp V

The coordinate mean along the feasible cofactor line is affine in the line parameter.

theorem NRR.AffinePositiveRayBoundary.VertexMap.mean_ne_zero_of_deviation_eq_zero_of_avoidsOrigin {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : mean p (V.affineValue w) ≠ 0

Origin avoidance makes the mean nonzero at every deviation-zero simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_mean_ne_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (t : ℝ) (ht : LineFeasible hp V w t) : mean p (V.affineValue (lineSimplexPoint hp V w t ht)) ≠ 0

Origin avoidance makes the mean nonzero everywhere on a feasible deviation-zero cofactor line.

theorem NRR.AffinePositiveRayBoundary.VertexMap.exists_affine_zero_between_of_opposite_signs (a b t₀ t₁ : ℝ) (ht : t₀ ≤ t₁) (hopposite : a + t₀ * b < 0 ∧ 0 < a + t₁ * b ∨ 0 < a + t₀ * b ∧ a + t₁ * b < 0) : ∃ t ∈ Set.Icc t₀ t₁, a + t * b = 0

An affine real function with opposite endpoint signs has a zero between the endpoints.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_mean_pos_iff_of_le {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (t₀ t₁ : ℝ) (ht₀ : LineFeasible hp V w t₀) (ht₁ : LineFeasible hp V w t₁) (ht : t₀ ≤ t₁) : 0 < mean p (V.affineValue (lineSimplexPoint hp V w t₀ ht₀)) ↔ 0 < mean p (V.affineValue (lineSimplexPoint hp V w t₁ ht₁))

Along an ordered pair of feasible parameters, origin avoidance forces the mean to have the same positive/nonpositive classification at both points.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineSimplexPoint_mean_pos_iff {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (t₀ t₁ : ℝ) (ht₀ : LineFeasible hp V w t₀) (ht₁ : LineFeasible hp V w t₁) : 0 < mean p (V.affineValue (lineSimplexPoint hp V w t₀ ht₀)) ↔ 0 < mean p (V.affineValue (lineSimplexPoint hp V w t₁ ht₁))

The mean has one constant sign on the entire feasible deviation-zero interval.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_unique_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (j : Fin (p + 1)) (hj : lineCoordinate hp V w (lowerParameter hp V hregular w) j = 0) : j = lowerEndpointIndex hp V hregular w

Under codimension-two avoidance, the chosen lower endpoint is the unique vanishing coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_unique_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (j : Fin (p + 1)) (hj : lineCoordinate hp V w (upperParameter hp V hregular w) j = 0) : j = upperEndpointIndex hp V hregular w

Under codimension-two avoidance, the chosen upper endpoint is the unique vanishing coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_unique_zero_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (lowerParameter hp V hregular w) ⋯))) (j : Fin (p + 1)) (hj : lineCoordinate hp V w (lowerParameter hp V hregular w) j = 0) : j = lowerEndpointIndex hp V hregular w

On the positive part of the deviation-zero line, the chosen lower endpoint is the unique vanishing coordinate under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_unique_zero_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (upperParameter hp V hregular w) ⋯))) (j : Fin (p + 1)) (hj : lineCoordinate hp V w (upperParameter hp V hregular w) j = 0) : j = upperEndpointIndex hp V hregular w

On the positive part of the deviation-zero line, the chosen upper endpoint is the unique vanishing coordinate under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_coordinate_pos_of_ne_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (lowerParameter hp V hregular w) ⋯))) (j : Fin (p + 1)) (hj : j ≠ lowerEndpointIndex hp V hregular w) : 0 < lineCoordinate hp V w (lowerParameter hp V hregular w) j

Every nonomitted lower-endpoint coordinate is positive when that endpoint lies on the positive ray.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_coordinate_pos_of_ne_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (upperParameter hp V hregular w) ⋯))) (j : Fin (p + 1)) (hj : j ≠ upperEndpointIndex hp V hregular w) : 0 < lineCoordinate hp V w (upperParameter hp V hregular w) j

Every nonomitted upper-endpoint coordinate is positive when that endpoint lies on the positive ray.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_coordinate_pos_of_ne {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (j : Fin (p + 1)) (hj : j ≠ lowerEndpointIndex hp V hregular w) : 0 < lineCoordinate hp V w (lowerParameter hp V hregular w) j

Every nonvanishing coordinate at the lower endpoint is strictly positive.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_coordinate_pos_of_ne {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (j : Fin (p + 1)) (hj : j ≠ upperEndpointIndex hp V hregular w) : 0 < lineCoordinate hp V w (upperParameter hp V hregular w) j

Every nonvanishing coordinate at the upper endpoint is strictly positive.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointIndex_ne_upperEndpointIndex {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : lowerEndpointIndex hp V hregular w ≠ upperEndpointIndex hp V hregular w

The two endpoint coordinates are distinct because their cofactor signs are opposite.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerParameter_lt_upperParameter {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : lowerParameter hp V hregular w < upperParameter hp V hregular w

Under codimension-two avoidance, the feasible parameter interval is nondegenerate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_classification {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : 0 < cofactorDirection hp V (lowerEndpointIndex hp V hregular w) ∧ lineCoordinate hp V w (lowerParameter hp V hregular w) (lowerEndpointIndex hp V hregular w) = 0 ∧ ∀ (j : Fin (p + 1)), lineCoordinate hp V w (lowerParameter hp V hregular w) j = 0 → j = lowerEndpointIndex hp V hregular w

Complete endpoint classification: the lower endpoint has one vanishing coordinate with positive cofactor direction, and no other coordinate vanishes.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_classification {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : cofactorDirection hp V (upperEndpointIndex hp V hregular w) < 0 ∧ lineCoordinate hp V w (upperParameter hp V hregular w) (upperEndpointIndex hp V hregular w) = 0 ∧ ∀ (j : Fin (p + 1)), lineCoordinate hp V w (upperParameter hp V hregular w) j = 0 → j = upperEndpointIndex hp V hregular w

Complete endpoint classification: the upper endpoint has one vanishing coordinate with negative cofactor direction, and no other coordinate vanishes.

def NRR.AffinePositiveRayBoundary.VertexMap.facetIndexEquiv {p : ℕ} (hp : Nat.Prime p) : Fin (p - 1 + 1) ≃ Fin p

For prime p, the coordinate type of StandardSimplex (p - 1) is canonically identified with the p vertices of a facet.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.facetIndexEquiv hp = (NRR.AffinePositiveRayBoundary.VertexMap.augmentedRowEquiv hp).symm

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetIndexEquiv_facetCoordinateIndex {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : (facetIndexEquiv hp) (facetCoordinateIndex i) = i

The generic facet-coordinate inclusion is inverse to facetIndexEquiv for prime p.

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex_facetIndexEquiv {p : ℕ} (hp : Nat.Prime p) (i : Fin (p - 1 + 1)) : facetCoordinateIndex ((facetIndexEquiv hp) i) = i

The reverse composite is also the identity.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) : StandardSimplex (p - 1)

Restrict a simplex point whose k-th coordinate vanishes to barycentric coordinates on the facet omitting vertex k.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates hp w k hk = ⟨fun (i : Fin (p - 1 + 1)) => ↑w (k.succAbove ((NRR.AffinePositiveRayBoundary.VertexMap.facetIndexEquiv hp) i)), ⋯⟩

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates_apply {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) (i : Fin (p - 1 + 1)) : ↑(facetCoordinates hp w k hk) i = ↑w (k.succAbove ((facetIndexEquiv hp) i))

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates_facetCoordinateIndex {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) (i : Fin p) : ↑(facetCoordinates hp w k hk) (facetCoordinateIndex i) = ↑w (k.succAbove i)

Reading the restricted point at the coordinate corresponding to facet vertex i recovers the original simplex coordinate at k.succAbove i.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates_unique {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) (u : StandardSimplex (p - 1)) (hu : ∀ (i : Fin p), ↑u (facetCoordinateIndex i) = ↑w (k.succAbove i)) : u = facetCoordinates hp w k hk

The restricted facet point is the unique facet-coordinate vector recovering all non-k coordinates of the original simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates_isInterior {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) (hpos : ∀ (j : Fin (p + 1)), j ≠ k → 0 < ↑w j) : (facetCoordinates hp w k hk).IsInterior

If k is the unique zero coordinate of w, the restricted facet coordinates are in the relative interior of the facet simplex.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetAffineValue_facetCoordinates {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) : V.facetAffineValue k (facetCoordinates hp w k hk) = V.affineValue w

Affine interpolation of the restricted facet coordinates agrees with full-simplex affine interpolation at the original point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.deviation_facetAffineValue_facetCoordinates {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) (q : Fin (p - 1)) : deviation hp (V.facetAffineValue k (facetCoordinates hp w k hk)) q = deviation hp (V.affineValue w) q

Deviation values are likewise unchanged by facet-coordinate conversion.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) : StandardSimplex p

Embed barycentric coordinates on the facet omitting k into the full simplex by inserting a zero at coordinate k. The prime hypothesis identifies the p facet vertices with the coordinate type of StandardSimplex (p - 1).

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet hp k u = ⟨k.insertNth 0 fun (i : Fin p) => ↑u (NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinateIndex i), ⋯⟩

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_omitted_eq_zero {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) : ↑(fullSimplexOfFacet hp k u) k = 0

The inserted coordinate is zero.

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_succAbove {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (i : Fin p) : ↑(fullSimplexOfFacet hp k u) (k.succAbove i) = ↑u (facetCoordinateIndex i)

Every non-omitted coordinate recovers the corresponding facet coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_succAbove_facetIndexEquiv {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (i : Fin (p - 1 + 1)) : ↑(fullSimplexOfFacet hp k u) (k.succAbove ((facetIndexEquiv hp) i)) = ↑u i

Recovery stated directly in the native coordinate type of the facet simplex.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_pos_of_ne {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (hu : u.IsInterior) (j : Fin (p + 1)) (hj : j ≠ k) : 0 < ↑(fullSimplexOfFacet hp k u) j

An interior facet point is strictly positive at every full-simplex coordinate other than the inserted zero coordinate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_eq_zero_iff {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (hu : u.IsInterior) (j : Fin (p + 1)) : ↑(fullSimplexOfFacet hp k u) j = 0 ↔ j = k

For an interior facet point, the inserted coordinate is the unique zero coordinate of its full-simplex embedding.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetCoordinates_fullSimplexOfFacet {p : ℕ} (hp : Nat.Prime p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) : facetCoordinates hp (fullSimplexOfFacet hp k u) k ⋯ = u

Restricting the full-simplex embedding back to the same facet recovers the original facet point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_facetCoordinates {p : ℕ} (hp : Nat.Prime p) (w : StandardSimplex p) (k : Fin (p + 1)) (hk : ↑w k = 0) : fullSimplexOfFacet hp k (facetCoordinates hp w k hk) = w

Conversely, embedding the facet coordinates of a full simplex point with zero k-th coordinate recovers that full simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.affineValue_fullSimplexOfFacet {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) : V.affineValue (fullSimplexOfFacet hp k u) = V.facetAffineValue k u

Affine interpolation of an embedded facet point agrees with affine interpolation on the facet. This is the inverse direction of facetAffineValue_facetCoordinates.

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.deviation_affineValue_fullSimplexOfFacet {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (q : Fin (p - 1)) : deviation hp (V.affineValue (fullSimplexOfFacet hp k u)) q = deviation hp (V.facetAffineValue k u) q

Fixed-deviation coordinates are preserved by embedding a facet point into the full simplex.

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.mean_affineValue_fullSimplexOfFacet {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) : mean p (V.affineValue (fullSimplexOfFacet hp k u)) = mean p (V.facetAffineValue k u)

The mean coordinate is preserved by embedding a facet point into the full simplex.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (hu : ∀ (q : Fin (p - 1)), deviation hp (V.facetAffineValue k u) q = 0) (q : Fin (p - 1)) : deviation hp (V.affineValue (fullSimplexOfFacet hp k u)) q = 0

A facet point with zero fixed deviations gives a full-simplex point with zero fixed deviations.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_mean_pos {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (hu : 0 < mean p (V.facetAffineValue k u)) : 0 < mean p (V.affineValue (fullSimplexOfFacet hp k u))

A positive-mean facet point gives a positive-mean full-simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.fullSimplexOfFacet_positiveRayData {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) (u : StandardSimplex (p - 1)) (hdev : ∀ (q : Fin (p - 1)), deviation hp (V.facetAffineValue k u) q = 0) (hmean : 0 < mean p (V.facetAffineValue k u)) : (∀ (q : Fin (p - 1)), deviation hp (V.affineValue (fullSimplexOfFacet hp k u)) q = 0) ∧ 0 < mean p (V.affineValue (fullSimplexOfFacet hp k u))

The deviation-zero and positive-mean data of a positive-ray facet witness transfer together to its full-simplex embedding.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointSimplexPoint {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : StandardSimplex p

The simplex point at the lower feasible parameter.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointSimplexPoint {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : StandardSimplex p

The simplex point at the upper feasible parameter.

Equations

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

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointSimplexPoint_apply {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (j : Fin (p + 1)) : ↑(lowerEndpointSimplexPoint hp V hregular w) j = lineCoordinate hp V w (lowerParameter hp V hregular w) j

@[simp]

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointSimplexPoint_apply {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (j : Fin (p + 1)) : ↑(upperEndpointSimplexPoint hp V hregular w) j = lineCoordinate hp V w (upperParameter hp V hregular w) j

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointSimplexPoint_omitted_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ↑(lowerEndpointSimplexPoint hp V hregular w) (lowerEndpointIndex hp V hregular w) = 0

The omitted coordinate of the lower endpoint point is zero.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointSimplexPoint_omitted_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : ↑(upperEndpointSimplexPoint hp V hregular w) (upperEndpointIndex hp V hregular w) = 0

The omitted coordinate of the upper endpoint point is zero.

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointFacetPoint {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : StandardSimplex (p - 1)

Restriction of the lower endpoint to its unique boundary facet.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointFacetPoint {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : StandardSimplex (p - 1)

Restriction of the upper endpoint to its unique boundary facet.

Equations

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

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointFacetPoint_isInterior {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : (lowerEndpointFacetPoint hp V hregular w).IsInterior

The lower endpoint gives a relative-interior point of its boundary facet.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointFacetPoint_isInterior {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : (upperEndpointFacetPoint hp V hregular w).IsInterior

The upper endpoint gives a relative-interior point of its boundary facet.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointFacetPoint_isInterior_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w))) : (lowerEndpointFacetPoint hp V hregular w).IsInterior

A positive lower endpoint gives a relative-interior point of its boundary facet under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointFacetPoint_isInterior_of_positiveMean {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (upperEndpointSimplexPoint hp V hregular w))) : (upperEndpointFacetPoint hp V hregular w).IsInterior

A positive upper endpoint gives a relative-interior point of its boundary facet under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_facetAffineValue_eq {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : V.facetAffineValue (lowerEndpointIndex hp V hregular w) (lowerEndpointFacetPoint hp V hregular w) = V.affineValue (lowerEndpointSimplexPoint hp V hregular w)

Facet interpolation at the lower endpoint restriction equals full interpolation at the lower endpoint simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_facetAffineValue_eq {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) : V.facetAffineValue (upperEndpointIndex hp V hregular w) (upperEndpointFacetPoint hp V hregular w) = V.affineValue (upperEndpointSimplexPoint hp V hregular w)

Facet interpolation at the upper endpoint restriction equals full interpolation at the upper endpoint simplex point.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointFacetPoint_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (q : Fin (p - 1)) : deviation hp (V.facetAffineValue (lowerEndpointIndex hp V hregular w) (lowerEndpointFacetPoint hp V hregular w)) q = 0

The lower endpoint facet point has zero deviation whenever the base line point does.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpointFacetPoint_deviation_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (q : Fin (p - 1)) : deviation hp (V.facetAffineValue (upperEndpointIndex hp V hregular w) (upperEndpointFacetPoint hp V hregular w)) q = 0

The upper endpoint facet point has zero deviation whenever the base line point does.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_mean_pos_iff_upperEndpoint_mean_pos {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w)) ↔ 0 < mean p (V.affineValue (upperEndpointSimplexPoint hp V hregular w))

The lower and upper endpoint means have the same sign.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpointFacet_mean_pos_iff_upperEndpointFacet_mean_pos {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (havoid : V.AvoidsOrigin) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) : 0 < mean p (V.facetAffineValue (lowerEndpointIndex hp V hregular w) (lowerEndpointFacetPoint hp V hregular w)) ↔ 0 < mean p (V.facetAffineValue (upperEndpointIndex hp V hregular w) (upperEndpointFacetPoint hp V hregular w))

Mean-sign constancy transferred to the two relative-interior facet representatives.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_facetHasPositiveRayIntersection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (lowerParameter hp V hregular w) ⋯))) : FacetHasPositiveRayIntersection hp V (lowerEndpointIndex hp V hregular w)

A positive mean at the lower endpoint supplies the required positive-ray facet witness.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_facetHasPositiveRayIntersection {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lineSimplexPoint hp V w (upperParameter hp V hregular w) ⋯))) : FacetHasPositiveRayIntersection hp V (upperEndpointIndex hp V hregular w)

A positive mean at the upper endpoint supplies the required positive-ray facet witness.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lowerEndpoint_facetHasPositiveRayIntersection_of_positiveCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w))) : FacetHasPositiveRayIntersection hp V (lowerEndpointIndex hp V hregular w)

A positive lower endpoint supplies the positive-ray facet witness under the weaker positive-ray-relative codimension-two condition.

theorem NRR.AffinePositiveRayBoundary.VertexMap.upperEndpoint_facetHasPositiveRayIntersection_of_positiveCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w : StandardSimplex p) (hw : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w) q = 0) (hmean : 0 < mean p (V.affineValue (upperEndpointSimplexPoint hp V hregular w))) : FacetHasPositiveRayIntersection hp V (upperEndpointIndex hp V hregular w)

A positive upper endpoint supplies the positive-ray facet witness under the weaker positive-ray-relative codimension-two condition.

theorem NRR.AffinePositiveRayBoundary.VertexMap.lineParameter_eq_lower_or_upper_of_coordinate_eq_zero {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (w : StandardSimplex p) (t : ℝ) (ht : LineFeasible hp V w t) (k : Fin (p + 1)) (hk : lineCoordinate hp V w t k = 0) : t = lowerParameter hp V hregular w ∨ t = upperParameter hp V hregular w

A feasible cofactor-line point with a vanishing coordinate occurs at one of the two finite interval endpoints. The sign of that coordinate's cofactor direction determines which endpoint is attained.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_endpoint_classification {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (k : Fin (p + 1)) (hfacet : FacetHasPositiveRayIntersection hp V k) : k = lowerEndpointIndex hp V hregular w₀ ∧ 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w₀)) ∨ k = upperEndpointIndex hp V hregular w₀ ∧ 0 < mean p (V.affineValue (upperEndpointSimplexPoint hp V hregular w₀))

Strong classification of an arbitrary positive-ray facet witness. Its full-simplex embedding is one of the two classified endpoint points, so both the omitted facet index and the positive mean are identified with the corresponding endpoint data.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_endpoint_classification_of_positiveCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (k : Fin (p + 1)) (hfacet : FacetHasPositiveRayIntersection hp V k) : k = lowerEndpointIndex hp V hregular w₀ ∧ 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w₀)) ∨ k = upperEndpointIndex hp V hregular w₀ ∧ 0 < mean p (V.affineValue (upperEndpointSimplexPoint hp V hregular w₀))

Strong classification of a positive-ray facet under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_imp_eq_lower_or_upper_of_positiveCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (k : Fin (p + 1)) : FacetHasPositiveRayIntersection hp V k → k = lowerEndpointIndex hp V hregular w₀ ∨ k = upperEndpointIndex hp V hregular w₀

Every positive-ray facet is one of the two interval endpoint facets under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_iff_eq_lower_or_upper_of_positiveCodimTwo {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsPositiveRayCodimTwo hp V) (havoid : V.AvoidsOrigin) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hlowerMean : 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w₀))) (k : Fin (p + 1)) : FacetHasPositiveRayIntersection hp V k ↔ k = lowerEndpointIndex hp V hregular w₀ ∨ k = upperEndpointIndex hp V hregular w₀

If the lower endpoint has positive mean, the positive-ray facets are exactly the lower and upper endpoints under positive-ray-relative codimension-two avoidance.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_imp_eq_lower_or_upper {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (k : Fin (p + 1)) : FacetHasPositiveRayIntersection hp V k → k = lowerEndpointIndex hp V hregular w₀ ∨ k = upperEndpointIndex hp V hregular w₀

Every positive-ray facet is one of the two interval endpoint facets.

theorem NRR.AffinePositiveRayBoundary.VertexMap.facetHasPositiveRayIntersection_iff_eq_lower_or_upper {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hregular : FacetRegular hp V) (hcodim : AvoidsCodimTwoDeviationZero hp V) (havoid : V.AvoidsOrigin) (w₀ : StandardSimplex p) (hw₀ : ∀ (q : Fin (p - 1)), deviation hp (V.affineValue w₀) q = 0) (hlowerMean : 0 < mean p (V.affineValue (lowerEndpointSimplexPoint hp V hregular w₀))) (k : Fin (p + 1)) : FacetHasPositiveRayIntersection hp V k ↔ k = lowerEndpointIndex hp V hregular w₀ ∨ k = upperEndpointIndex hp V hregular w₀

If the lower endpoint has positive mean, the positive-ray facets are exactly the lower and upper endpoint facets.

inductive NRR.AffinePositiveRayBoundary.VertexMap.RayBoundaryCertificate {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) : Type

Finite description of the positive-ray boundary of one generic affine prism simplex. Either the positive ray misses every facet, or it meets exactly two facets with opposite cofactor orientations.

• empty {p : ℕ} {hp : Nat.Prime p} {V : VertexMap p} (no_positive_facet : ∀ (k : Fin (p + 1)), ¬FacetHasPositiveRayIntersection hp V k) : RayBoundaryCertificate hp V
• pair {p : ℕ} {hp : Nat.Prime p} {V : VertexMap p} (lower upper : Fin (p + 1)) (lower_ne_upper : lower ≠ upper) (lower_positive : 0 < cofactorDirection hp V lower) (upper_negative : cofactorDirection hp V upper < 0) (positive_facets : ∀ (k : Fin (p + 1)), FacetHasPositiveRayIntersection hp V k ↔ k = lower ∨ k = upper) : RayBoundaryCertificate hp V

theorem NRR.AffinePositiveRayBoundary.VertexMap.faceSign_mul_determinantIndex_eq_directionIndex {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (k : Fin (p + 1)) : (-1) ^ ↑k * FoxNeuwirthOrderComplex.AffineVertexMap.determinantIndex (facetDeterminant hp V k) = FoxNeuwirthOrderComplex.AffineVertexMap.determinantIndex (cofactorDirection hp V k)

The alternating determinant sign is the sign of the cofactor direction.

def NRR.AffinePositiveRayBoundary.VertexMap.RayBoundaryTheorem : Prop

The exact local line-geometry statement needed for the prism argument. It says that facet regularity and origin avoidance produce the two signed boundary points of the positive-ray preimage. The construction is finite-dimensional: write the deviation-zero affine line using signed maximal minors, intersect it with the barycentric simplex, and use origin avoidance to keep the mean sign constant.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.rayBoundaryCertificateOfPositiveRayGeneralPosition {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hgp : PositiveRayGeneralPosition hp V) : RayBoundaryCertificate hp V

Construct the finite positive-ray boundary certificate from the weaker positive-ray-relative general-position hypotheses.

Equations

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

noncomputable def NRR.AffinePositiveRayBoundary.VertexMap.rayBoundaryCertificate {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hgp : GeneralPosition hp V) : RayBoundaryCertificate hp V

Construct the finite positive-ray boundary certificate from the local general-position hypotheses. If the deviation-zero line misses the simplex, or if its constant nonzero mean is negative, no facet meets the open positive ray. Otherwise the lower and upper feasible endpoints are exactly the two positive-ray facets and have opposite cofactor signs.

Equations

• NRR.AffinePositiveRayBoundary.VertexMap.rayBoundaryCertificate hp V hgp = NRR.AffinePositiveRayBoundary.VertexMap.rayBoundaryCertificateOfPositiveRayGeneralPosition hp V ⋯

theorem NRR.AffinePositiveRayBoundary.VertexMap.rayBoundaryTheorem : RayBoundaryTheorem

The local affine positive-ray boundary theorem.

theorem NRR.AffinePositiveRayBoundary.VertexMap.alternating_facetIndex_sum_eq_zero_of_certificate {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (C : RayBoundaryCertificate hp V) : ∑ k : Fin (p + 1), facetIndex hp V k = 0

Local affine Stokes theorem from the explicit boundary certificate.

theorem NRR.AffinePositiveRayBoundary.VertexMap.alternating_facetIndex_sum_eq_zero_of_positiveRayGeneralPosition {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hgp : PositiveRayGeneralPosition hp V) : ∑ k : Fin (p + 1), facetIndex hp V k = 0

Unconditional local affine Stokes under positive-ray-relative general position.

theorem NRR.AffinePositiveRayBoundary.VertexMap.alternating_facetIndex_sum_eq_zero {p : ℕ} (Hline : RayBoundaryTheorem) (hp : Nat.Prime p) (V : VertexMap p) (hgp : GeneralPosition hp V) : ∑ k : Fin (p + 1), facetIndex hp V k = 0

Local affine Stokes, reduced to the finite line-geometry theorem.

theorem NRR.AffinePositiveRayBoundary.VertexMap.alternating_facetIndex_sum_eq_zero_of_generalPosition {p : ℕ} (hp : Nat.Prime p) (V : VertexMap p) (hgp : GeneralPosition hp V) : ∑ k : Fin (p + 1), facetIndex hp V k = 0

Unconditional local affine Stokes theorem under the general-position hypotheses.