Exact affine covers for closed genus-five rows

This module joins two existing public trust boundaries. A CoordinateCell is an ordinary closed explicit-potential certificate whose coordinates are the twelve slot lengths. AffineCover selects one such cell, and the closed-face census turns its local scripts into BNExists on the canonical forest contraction. The final adapter recovers the diagnostic AR pencil.

Generated row modules contain data only: certificates, cones, and one checked cover tree. All graph and divisor semantics are proved here once.

theorem AtanasovRanganathan.GenusFiveClosedCover.degSpec_ext {n p : ℕ} {left right : Utilities.Certificate.DegenerateSpec.DegSpec n p} (hCore : left.core = right.core) (hLength : left.length = right.length) (hRep : left.rep = right.rep) : left = right

Extensionality for degenerate specifications; all omitted fields are proofs of propositions.

def AtanasovRanganathan.GenusFiveClosedCover.coordinateForm {p : ℕ} (edge : Fin p) : Utilities.Certificate.ExplicitPotential.AffineForm p

The affine coordinate reading the length of slot edge.

Equations

• AtanasovRanganathan.GenusFiveClosedCover.coordinateForm edge = { fixedValue := 0, coefficient := fun (coordinate : Fin p) => if coordinate = edge then 1 else 0 }

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.coordinateForm_eval {p : ℕ} (edge : Fin p) (point : Fin p → ℤ) : Utilities.Certificate.AffineCover.AffineForm.eval (coordinateForm edge) point = point edge

structure AtanasovRanganathan.GenusFiveClosedCover.CoordinateCell {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) : Type

Passive data for one cone of a closed row cover.

• divisor : Fin n → ℤ

  The integer chip multiplicities of the divisor used throughout this cone.

• witness : Fin n → Utilities.Certificate.ExplicitPotential.AnchorWitness p n p

  An explicit-potential witness for each anchor vertex of the core.

• cone : List (Utilities.Certificate.ExplicitPotential.AffineForm p)

  The affine constraints specifying the cone where this cell certificate applies.

def AtanasovRanganathan.GenusFiveClosedCover.CoordinateCell.certificate {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cell : CoordinateCell core) : Utilities.Certificate.ExplicitPotential.CertificateData p n p

Interpret a cell as the standard explicit-potential certificate.

Equations

• cell.certificate = { core := core, segment := AtanasovRanganathan.GenusFiveClosedCover.coordinateForm, divisor := cell.divisor, witness := cell.witness, cone := cell.cone }

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.CoordinateCell.certificate_cone {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cell : CoordinateCell core) : cell.certificate.cone = cell.cone

def AtanasovRanganathan.GenusFiveClosedCover.lengthPoint {p : ℕ} (length : Fin p → ℕ) : Fin p → ℤ

The length point used by a coordinate cell.

Equations

• AtanasovRanganathan.GenusFiveClosedCover.lengthPoint length edge = ↑(length edge)

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.coordinateCell_segmentNat {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cell : CoordinateCell core) (length : Fin p → ℕ) (edge : Fin p) : cell.certificate.segmentNat (lengthPoint length) edge = length edge

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.coordinateCell_zeroSlots {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cell : CoordinateCell core) (length : Fin p → ℕ) : cell.certificate.zeroSlots (lengthPoint length) = Configurations.zeroSlots length

theorem AtanasovRanganathan.GenusFiveClosedCover.CoordinateCell.bnExists_faceSpec {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (core_nonempty : 0 < n) (hCoreConnected : core.Connected) (cell : CoordinateCell core) (hValid : cell.certificate.ValidClosed 4) (length : Fin p → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Configurations.zeroSlots length)) (notLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Configurations.zeroSlots length)) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold cell.cone (lengthPoint length)) : Utilities.BNExists (Configurations.faceSpec core core_nonempty length forest notLoopy).graph 1 4

One accepted coordinate cell proves the semantic row statement on the canonical closed face.

def AtanasovRanganathan.GenusFiveClosedCover.cones {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cells : List (CoordinateCell core)) : List (List (Utilities.Certificate.ExplicitPotential.AffineForm p))

A list of passive cells advertises exactly their certificate cones.

Equations

• AtanasovRanganathan.GenusFiveClosedCover.cones cells = List.map AtanasovRanganathan.GenusFiveClosedCover.CoordinateCell.cone cells

A compact split tree for certificate cells

inductive AtanasovRanganathan.GenusFiveClosedCover.CellTree (p : ℕ) : Type

Proof-producing decision tree used by the fixed-row emitter. A leaf names one cell and carries, for every inequality in its cone, a Farkas contradiction from the active chamber together with the violation of that inequality.

• cell {p : ℕ} (index : ℕ) (receipts : List Utilities.Certificate.AffineCover.FarkasData) : CellTree p
• absurd {p : ℕ} (receipt : Utilities.Certificate.AffineCover.FarkasData) : CellTree p
• split {p : ℕ} (form : Utilities.Certificate.ExplicitPotential.AffineForm p) (nonnegative negative : CellTree p) : CellTree p

def AtanasovRanganathan.GenusFiveClosedCover.CellTree.coneAt {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cells : List (CoordinateCell core)) (index : ℕ) : List (Utilities.Certificate.ExplicitPotential.AffineForm p)

The affine cone attached to a cell index, defaulting to the empty constraint list for an invalid index.

Equations

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

def AtanasovRanganathan.GenusFiveClosedCover.CellTree.Valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) : CellTree p → Prop

Validity of the cell indices, Farkas receipts, and sign branches in a tree under the active affine constraints.

Equations

• One or more equations did not get rendered due to their size.
• AtanasovRanganathan.GenusFiveClosedCover.CellTree.Valid cells active (AtanasovRanganathan.GenusFiveClosedCover.CellTree.absurd receipt) = receipt.Valid active

def AtanasovRanganathan.GenusFiveClosedCover.CellTree.check {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) : CellTree p → Bool

The Boolean checker for cell coverage, contradiction receipts, and both branches of each affine split.

Equations

• One or more equations did not get rendered due to their size.
• AtanasovRanganathan.GenusFiveClosedCover.CellTree.check cells active (AtanasovRanganathan.GenusFiveClosedCover.CellTree.absurd receipt) = receipt.check active

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.CellTree.check_eq_true_iff {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (tree : CellTree p) (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) : check cells active tree = true ↔ Valid cells active tree

theorem AtanasovRanganathan.GenusFiveClosedCover.CellTree.coveredCell_of_valid {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (tree : CellTree p) (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (hValid : Valid cells active tree) (point : Fin p → ℤ) (hActive : Utilities.Certificate.ExplicitPotential.FormsHold active point) : ∃ cell ∈ cells, Utilities.Certificate.ExplicitPotential.FormsHold cell.cone point

The generated row proofs can have many repeated split forms and Farkas receipts. CompactCellTree stores indices into shared tables, keeping the checked source proportional to the genuinely distinct arithmetic data.

inductive AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree : Type

A cell decision tree whose forms and receipts are indices into shared tables.

• cell (index : ℕ) (receipts : List ℕ) : CompactCellTree
• absurd (receipt : ℕ) : CompactCellTree
• split (form : ℕ) (nonnegative negative : CompactCellTree) : CompactCellTree

def AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.decode {p : ℕ} (forms : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (receipts : List Utilities.Certificate.AffineCover.FarkasData) : CompactCellTree → CellTree p

Expand the shared form and receipt indices into a full cell tree, using zero forms and empty receipts for invalid indices.

Equations

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

def AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.check {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (tree : CompactCellTree) (forms : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (receipts : List Utilities.Certificate.AffineCover.FarkasData) (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) : Bool

Check a compact tree by decoding its shared tables and checking the resulting cell tree.

Equations

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

@[simp]

theorem AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree.check_split {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (index : ℕ) (nonnegative negative : CompactCellTree) (forms : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (receipts : List Utilities.Certificate.AffineCover.FarkasData) (cells : List (CoordinateCell core)) (active : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) : (split index nonnegative negative).check forms receipts cells active = (nonnegative.check forms receipts cells (active ++ [forms.getD index 0]) && negative.check forms receipts cells (active ++ [Utilities.Certificate.AffineCover.AffineForm.violation (forms.getD index 0)]))

theorem AtanasovRanganathan.GenusFiveClosedCover.closedConstruction_of_cellTree {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (core_nonempty : 0 < n) (hCoreConnected : core.Connected) (cells : List (CoordinateCell core)) (base : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (tree : CellTree p) (hBase : ∀ (length : Fin p → ℕ), Utilities.Certificate.ExplicitPotential.FormsHold base (lengthPoint length)) (hCells : ∀ cell ∈ cells, cell.certificate.ValidClosed 4) (hCheck : CellTree.check cells base tree = true) : Configurations.ClosedSubdivisionDharConstruction core core_nonempty

Checked split-tree form of closedConstruction_of_cover.

theorem AtanasovRanganathan.GenusFiveClosedCover.closedConstruction_of_compactCellTree {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (core_nonempty : 0 < n) (hCoreConnected : core.Connected) (cells : List (CoordinateCell core)) (base forms : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (receipts : List Utilities.Certificate.AffineCover.FarkasData) (tree : CompactCellTree) (hBase : ∀ (length : Fin p → ℕ), Utilities.Certificate.ExplicitPotential.FormsHold base (lengthPoint length)) (hCells : ∀ cell ∈ cells, cell.certificate.ValidClosed 4) (hCheck : tree.check forms receipts cells base = true) : Configurations.ClosedSubdivisionDharConstruction core core_nonempty

Table-compressed checked split-tree form of closedConstruction_of_cellTree.

theorem AtanasovRanganathan.GenusFiveClosedCover.chamberPencil_of_compactCellTree {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (core_nonempty : 0 < n) (hCoreConnected : core.Connected) (cells : List (CoordinateCell core)) (base forms : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (receipts : List Utilities.Certificate.AffineCover.FarkasData) (tree : CompactCellTree) (hCells : ∀ cell ∈ cells, cell.certificate.ValidClosed 4) (hCheck : tree.check forms receipts cells base = true) (length : Fin p → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest core (Configurations.zeroSlots length)) (notLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy core (Configurations.zeroSlots length)) (hHold : Utilities.Certificate.ExplicitPotential.FormsHold base (lengthPoint length)) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec core core_nonempty length forest notLoopy).graph)

Chamber form of closedConstruction_of_compactCellTree.

The checked data only has to cover the sub-cone cut out by base, and the conclusion is the pencil at a single length vector lying in that sub-cone. This is exactly the shape of the chamber argument of ClosedOrbit.closedConstruction_of_chamber, so a row whose exact cover is too large to replay on the whole orthant may be proved on a fundamental domain for the core's symmetry group and transported to the rest.

Nothing is weakened: base is still the active row list at the root of the tree, so every Farkas receipt is replayed against exactly the hypotheses the caller supplies pointwise through hHold.

theorem AtanasovRanganathan.GenusFiveClosedCover.closedConstruction_of_cover {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} (core_nonempty : 0 < n) (hCoreConnected : core.Connected) (cells : List (CoordinateCell core)) (base : List (Utilities.Certificate.ExplicitPotential.AffineForm p)) (hBase : ∀ (length : Fin p → ℕ), Utilities.Certificate.ExplicitPotential.FormsHold base (lengthPoint length)) (hCells : ∀ cell ∈ cells, cell.certificate.ValidClosed 4) (hCover : Utilities.Certificate.AffineCover.Covers base (cones cells)) : Configurations.ClosedSubdivisionDharConstruction core core_nonempty

A checked affine cover whose every cell is valid gives the full closed AR construction.