def orientFace {ι : Type} [LinearOrder ι] (s : Finset ι) : List ι

orientFace s is the canonical orientation of a face s: its vertices listed in increasing order with respect to the ambient LinearOrder on ι.

Use this in the specification/proof layer (incidence and sign checks), not as a transport encoding for Sage JSON interop.

Equations

• orientFace s = s.sort fun (x1 x2 : ι) => x1 ≤ x2

def deletionMatches {ι : Type} [DecidableEq ι] (σ τ : List ι) : List ℕ

Equations

• deletionMatches σ τ = List.filter (fun (i : ℕ) => decide (σ.eraseIdx i = τ)) (List.range σ.length)

def deletionIndex {ι : Type} [DecidableEq ι] (σ τ : List ι) : Option ℕ

index i if τ = σ with exactly the i-th vertex deleted; none otherwise

Equations

• deletionIndex σ τ = match deletionMatches σ τ with | [i] => some i | x => none

def signOfIndex (i : ℕ) : ℤ

Equations

• signOfIndex i = if i % 2 = 0 then 1 else -1

def boundaryCoeff {ι : Type} [DecidableEq ι] (σ τ : List ι) : ℤ

Equations

• boundaryCoeff σ τ = match deletionIndex σ τ with | some i => signOfIndex i | none => 0

def isBoundaryEntry {ι : Type} [DecidableEq ι] (σ τ : List ι) (a : ℤ) : Prop

declarative entry predicate for external matrix verification

Equations

• isBoundaryEntry σ τ a = (a = boundaryCoeff σ τ)

def getEntry? (d : List (List ℤ)) (i j : ℕ) : Option ℤ

Safe list indexing.

Equations

• getEntry? d i j = do let row ← d[i]? row[j]?

def expectedEntry? {ι : Type} [DecidableEq ι] (dom cod : List (List ι)) (i j : ℕ) : Option ℤ

Expected boundary entry from bases at (i,j): row i = codomain simplex τ, column j = domain simplex σ.

Equations

• expectedEntry? dom cod i j = do let τ ← cod[i]? let σ ← dom[j]? pure (boundaryCoeff σ τ)