Affine-described positions on the CLOSED length orthant

The DegSpec counterpart of Certificate/AffinePosition.lean's decodePosition and decodeVertex. Nothing there is modified: the strictly positive decoder keeps working, and the passive Code type, its two cone rows (BoundsCertified), rawOffset, coordinate and every purely arithmetic fact about them are reused verbatim — none of them mention Spec.

Two things change, and both are forced.

• Valid becomes ValidClosed. rawOffset_le_segmentNat reads the slot length off segmentNat_cast_eq, which needs segment_positive_of_valid. The closed-orthant replacement is segmentNat_cast_eq_of_validClosed, which needs only non-negativity. Nothing else in the bound argument changes.

• The two-case split becomes a trichotomy. On a Spec a decoded position is 0 or interior whenever it is strictly below the slot length, and length_pos usually supplies that. On the closed orthant coordinate = length is reachable — and at a collapsed slot it is the only possibility, where it coincides with coordinate = 0. decodeDegenerateVertex_trichotomy is the exhaustive statement; the positive-world two-case consumers have no case for the middle disjunct.

Note that decodeVertex_eq_head_of_coordinate_eq_length is already boundary-safe as a statement; what is not boundary-safe is concluding "interior" from 0 < coordinate.

The bound argument, on the closed orthant

theorem MarkedGraphs.Certificate.AffinePosition.Code.rawOffset_le_segmentNat_of_validClosed {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : code.rawOffset point ≤ certificate.segmentNat point code.edge

Closed-orthant replacement for rawOffset_le_segmentNat. Only the length decoding changes: segmentNat_cast_eq_of_validClosed needs non-negativity, not positivity.

theorem MarkedGraphs.Certificate.AffinePosition.Code.coordinate_le_segmentNat_of_validClosed {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : coordinate certificate code point ≤ certificate.segmentNat point code.edge

Closed-orthant replacement for coordinate_le_segmentNat.

Decoding into the contracted subdivision

def MarkedGraphs.Certificate.AffinePosition.Code.decodeDegeneratePosition {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).PathPosition code.edge

Typed path position on the contracted subdivision, decoded from a cone-certified affine position.

Equations

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

def MarkedGraphs.Certificate.AffinePosition.Code.decodeDegenerateVertex {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).Vertex

The actual vertex of the contracted subdivision named by an affine position code.

Equations

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

@[simp]

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegeneratePosition_val {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : ↑(decodeDegeneratePosition certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone) = coordinate certificate code point

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegeneratePosition_val_of_fromHead_false {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hDirection : code.fromHead = false) : ↑(decodeDegeneratePosition certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone) = code.rawOffset point

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegeneratePosition_val_of_fromHead_true {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hDirection : code.fromHead = true) : ↑(decodeDegeneratePosition certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone) = certificate.segmentNat point code.edge - code.rawOffset point

The trichotomy

decodeVertex_eq_tail_of_coordinate_eq_zero and decodeVertex_eq_head_of_coordinate_eq_length port unchanged; the third case is the one the positive world does not have as a separate statement, because there 0 < coordinate already implies interiority when coordinate < length.

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegenerateVertex_eq_tail_of_coordinate_eq_zero {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hZero : coordinate certificate code point = 0) : decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).coreVertex (certificate.core.tail code.edge)

Coordinate zero decodes to the tail class.

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegenerateVertex_eq_head_of_coordinate_eq_length {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hLength : coordinate certificate code point = certificate.segmentNat point code.edge) : decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).coreVertex (certificate.core.head code.edge)

Coordinate equal to the slot length decodes to the head class. This holds at a collapsed slot too, where it is the same vertex as the tail class: DegSpec.pathVertex_length uses rep_zero, not length_pos.

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegenerateVertex_eq_interiorVertex {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hZero : coordinate certificate code point ≠ 0) (hLast : coordinate certificate code point ≠ certificate.segmentNat point code.edge) : decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).interiorVertex code.edge ⟨coordinate certificate code point - 1, ⋯⟩

A strictly interior coordinate decodes to an interior vertex.

theorem MarkedGraphs.Certificate.AffinePosition.Code.decodeDegenerateVertex_trichotomy {m n p : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (code : Code m p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (rep : Fin n → Fin n) (rep_idem : ∀ (v : Fin n), rep (rep v) = rep v) (rep_zero : ∀ (edge : Fin p), certificate.segmentNat point edge = 0 → rep (certificate.core.tail edge) = rep (certificate.core.head edge)) (rep_loopless : ∀ (edge : Fin p), 0 < certificate.segmentNat point edge → rep (certificate.core.tail edge) ≠ rep (certificate.core.head edge)) (forest : (Finset.image rep Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n) {degree : ℤ} (hValid : certificate.ValidClosed degree) (hBounds : BoundsCertified certificate code) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).coreVertex (certificate.core.tail code.edge) ∨ decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).coreVertex (certificate.core.head code.edge) ∨ ∃ (o : Fin (certificate.segmentNat point code.edge - 1)), decodeDegenerateVertex certificate code point core_nonempty rep rep_idem rep_zero rep_loopless forest hValid hBounds hCone = (certificate.degenerateSpec point core_nonempty rep rep_idem rep_zero rep_loopless forest).interiorVertex code.edge o

The trichotomy. A decoded position lands on the tail class, on the head class, or on an interior vertex. At a collapsed slot only the first two are available and they coincide; the positive-world two-case split (coordinate = 0 versus coordinate > 0 ⟹ interior) has no case for the head class.