Finite loop-aware pseudocore certificates

This module defines finite loop-aware pseudocores and a Boolean checker for their structural properties. The validity API is parameterized by cyclomatic genus; it does not contain a census or assert a completeness theorem.

A loop-aware pseudocore stores semantic loops separately and stores nonloop multiplicities in a full matrix. The checker requires that matrix to be symmetric with zero diagonal, so the redundant lower triangle cannot disagree with the upper triangle used by edgeCount. Validity then checks connected nonloop support, stable valence at least three, and the requested genus edge-count identity.

SplitMetadata is an optional second boundary matching the loopless split cores used by explicit-potential certificates. It gives every semantic loop one marker vertex and checks the resulting ExplicitPotential.Core directly: marker counts, looplessness, core connectivity, and every unordered edge multiplicity are all replayed by finite Boolean folds.

structure Utilities.Certificate.GenusFourPseudocore.Pseudocore (n : ℕ) : Type

A labelled loop-aware multigraph on Fin n. multiplicity i j is meant to be an unordered nonloop multiplicity; validity checks symmetry and a zero diagonal explicitly.

• loops : Fin n → ℕ

  The number of semantic loop occurrences based at each pseudocore vertex.

• multiplicity : Fin n → Fin n → ℕ

  The proposed multiplicity of nonloop edges between each pair of pseudocore vertices.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.loopCount {n : ℕ} (core : Pseudocore n) : ℕ

Total number of semantic loop occurrences.

Equations

• core.loopCount = ∑ vertex : Fin n, core.loops vertex

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.nonloopEdgeCount {n : ℕ} (core : Pseudocore n) : ℕ

Number of nonloop edge occurrences, counted in the strict upper triangle.

Equations

• core.nonloopEdgeCount = ∑ first : Fin n, ∑ second : Fin n, if first < second then core.multiplicity first second else 0

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.edgeCount {n : ℕ} (core : Pseudocore n) : ℕ

Total number of topological edge occurrences.

Equations

• core.edgeCount = core.loopCount + core.nonloopEdgeCount

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.valence {n : ℕ} (core : Pseudocore n) (vertex : Fin n) : ℕ

Loop-aware valence: a loop contributes two and a nonloop occurrence one.

Equations

• core.valence vertex = 2 * core.loops vertex + ∑ neighbor : Fin n, core.multiplicity vertex neighbor

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.MatrixWellFormed {n : ℕ} (core : Pseudocore n) : Prop

The redundant multiplicity matrix really represents unordered nonloops.

Equations

• core.MatrixWellFormed = ((∀ (vertex : Fin n), core.multiplicity vertex vertex = 0) ∧ ∀ (first second : Fin n), core.multiplicity first second = core.multiplicity second first)

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.Connected {n : ℕ} (core : Pseudocore n) : Prop

Connectedness of the nonloop support, in the same cut form used by graphConnected. Semantic loops do not cross cuts.

Equations

• core.Connected = ∀ (S : Finset (Fin n)), (∃ (inside : Fin n) (outside : Fin n), inside ∈ S ∧ outside ∉ S) → ∃ inside ∈ S, ∃ outside ∉ S, 0 < core.multiplicity inside outside

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.Stable {n : ℕ} (core : Pseudocore n) : Prop

Every topological vertex has valence at least three.

Equations

• core.Stable = ∀ (vertex : Fin n), 3 ≤ core.valence vertex

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.ValidAt {n : ℕ} (core : Pseudocore n) (g : ℕ) : Prop

Mathematical validity of a labelled pseudocore at cyclomatic genus g.

The edge equation is written without truncated natural subtraction, so it is the exact Euler-characteristic identity at every genus.

Equations

• core.ValidAt g = (core.MatrixWellFormed ∧ core.Connected ∧ core.Stable ∧ core.edgeCount + 1 = n + g)

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.Valid {n : ℕ} (core : Pseudocore n) : Prop

Backwards-compatible genus-four specialization of ValidAt.

Equations

• core.Valid = core.ValidAt 4

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.matrixCheck {n : ℕ} (core : Pseudocore n) : Bool

Executable exact matrix check.

Equations

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

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.connectedCheck {n : ℕ} (core : Pseudocore n) : Bool

Executable exact cut-connectedness check over all finite vertex subsets.

Equations

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

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.stableCheck {n : ℕ} (core : Pseudocore n) : Bool

Executable exact stability check.

Equations

• core.stableCheck = Utilities.Certificate.AffineCover.allFin fun (vertex : Fin n) => decide (3 ≤ core.valence vertex)

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.checkAt {n : ℕ} (core : Pseudocore n) (g : ℕ) : Bool

Complete executable checker at a requested cyclomatic genus.

Equations

• core.checkAt g = (core.matrixCheck && core.connectedCheck && core.stableCheck && decide (core.edgeCount + 1 = n + g))

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.check {n : ℕ} (core : Pseudocore n) : Bool

Backwards-compatible genus-four specialization of checkAt.

Equations

• core.check = core.checkAt 4

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.matrixCheck_eq_true_iff {n : ℕ} (core : Pseudocore n) : core.matrixCheck = true ↔ core.MatrixWellFormed

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.connectedCheck_eq_true_iff {n : ℕ} (core : Pseudocore n) : core.connectedCheck = true ↔ core.Connected

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.stableCheck_eq_true_iff {n : ℕ} (core : Pseudocore n) : core.stableCheck = true ↔ core.Stable

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.checkAt_eq_true_iff {n : ℕ} (core : Pseudocore n) (g : ℕ) : core.checkAt g = true ↔ core.ValidAt g

The finite Boolean checker at genus g implements ValidAt g.

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.valid_iff_validAt_four {n : ℕ} (core : Pseudocore n) : core.Valid ↔ core.ValidAt 4

The legacy validity predicate is exactly the genus-four specialization.

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.check_eq_true_iff {n : ℕ} (core : Pseudocore n) : core.check = true ↔ core.Valid

The legacy checker is exactly the genus-four specialization.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.topologicalGenus {n : ℕ} (core : Pseudocore n) : ℤ

The cyclomatic genus of the loop-aware topological multigraph.

Equations

• core.topologicalGenus = ↑core.edgeCount - ↑n + 1

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.topologicalGenus_eq {n : ℕ} (core : Pseudocore n) {g : ℕ} (hValid : core.ValidAt g) : core.topologicalGenus = ↑g

The checked edge-count identity is exactly the requested genus.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.topologicalGenus_eq_four {n : ℕ} (core : Pseudocore n) (hValid : core.Valid) : core.topologicalGenus = 4

The legacy genus-four form of topologicalGenus_eq.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.vertexCount_pos_of_valid {n : ℕ} (core : Pseudocore n) (hValid : core.Valid) : 0 < n

A valid genus-four pseudocore has at least one vertex.

Loopless split-core metadata

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.splitEdgeCount {n : ℕ} (core : Pseudocore n) : ℕ

Number of edge slots after replacing each semantic loop by two parallel edges from its base vertex to a fresh marker.

Equations

• core.splitEdgeCount = core.nonloopEdgeCount + 2 * core.loopCount

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.splitEdgeCount_eq_edgeCount_add_loopCount {n : ℕ} (core : Pseudocore n) : core.splitEdgeCount = core.edgeCount + core.loopCount

Splitting a semantic loop adds one marker vertex and one net edge.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.splitTopologicalGenus {n : ℕ} (core : Pseudocore n) : ℤ

Cyclomatic genus of the loopless split incidence data.

Equations

• core.splitTopologicalGenus = ↑core.splitEdgeCount - ↑(n + core.loopCount) + 1

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.splitTopologicalGenus_eq {n : ℕ} (core : Pseudocore n) {g : ℕ} (hValid : core.ValidAt g) : core.splitTopologicalGenus = ↑g

Loop splitting preserves the requested cyclomatic genus.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.splitTopologicalGenus_eq_four {n : ℕ} (core : Pseudocore n) (hValid : core.Valid) : core.splitTopologicalGenus = 4

The legacy genus-four form of splitTopologicalGenus_eq.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.baseVertex {n : ℕ} (core : Pseudocore n) (vertex : Fin n) : Fin (n + core.loopCount)

Original base vertices occupy the left summand of the split vertex type.

Equations

• core.baseVertex vertex = Fin.castAdd core.loopCount vertex

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.markerVertex {n : ℕ} (core : Pseudocore n) (marker : Fin core.loopCount) : Fin (n + core.loopCount)

Loop markers occupy the right summand of the split vertex type.

Equations

• core.markerVertex marker = Fin.natAdd n marker

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.explicitCoreMultiplicity {vertexCount edgeCount : ℕ} (splitCore : ExplicitPotential.Core vertexCount edgeCount) (first second : Fin vertexCount) : ℕ

Unordered edge multiplicity of an ordered-slot explicit-potential core.

Equations

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

structure Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata {n : ℕ} (core : Pseudocore n) : Type

Passive metadata for the canonical loopless split of a loop-aware core. The actual marker order and edge-slot order are arbitrary and are checked from the displayed functions.

• markerBase : Fin core.loopCount → Fin n

  The original base vertex to which each split-loop marker is attached.

• splitCore : ExplicitPotential.Core (n + core.loopCount) core.splitEdgeCount

  The proposed explicit core after adjoining one marker per loop and splitting each loop into two slots.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.markerMultiplicity {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (vertex : Fin n) : ℕ

Number of displayed markers attached to a base vertex.

Equations

• data.markerMultiplicity vertex = {marker : Fin core.loopCount | data.markerBase marker = vertex}.card

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.expectedMultiplicity {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (first second : Fin (n + core.loopCount)) : ℕ

Expected split multiplicity between two displayed split vertices.

Equations

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

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.ValidAt {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (g : ℕ) : Prop

Exact mathematical relation between loop-aware data and its displayed loopless ordered-slot split core at genus g.

Equations

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

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.Valid {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) : Prop

Backwards-compatible genus-four specialization of SplitMetadata.ValidAt.

Equations

• data.Valid = data.ValidAt 4

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.checkAt {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (g : ℕ) : Bool

Exact finite checker for split-core metadata at genus g.

Equations

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

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.check {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) : Bool

Backwards-compatible genus-four specialization of SplitMetadata.checkAt.

Equations

• data.check = data.checkAt 4

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.checkAt_eq_true_iff {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (g : ℕ) : data.checkAt g = true ↔ data.ValidAt g

The split metadata checker at genus g implements ValidAt g.

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.valid_iff_validAt_four {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) : data.Valid ↔ data.ValidAt 4

The legacy split validity predicate is its genus-four specialization.

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.check_eq_true_iff {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) : data.check = true ↔ data.Valid

The legacy split checker is its genus-four specialization.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.splitTopologicalGenus_eq {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) {g : ℕ} (hValid : data.ValidAt g) : core.splitTopologicalGenus = ↑g

A valid split certificate carries the requested genus through loop splitting.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.splitCore_loopless_of_valid {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (hValid : data.Valid) (edge : Fin core.splitEdgeCount) : data.splitCore.tail edge ≠ data.splitCore.head edge

Accepted split metadata is loopless as ordered edge-slot data.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.SplitMetadata.splitCore_connected_of_valid {n : ℕ} {core : Pseudocore n} (data : core.SplitMetadata) (hValid : data.Valid) : data.splitCore.Connected

Accepted split metadata carries the core connectedness required by the explicit-potential bundle checker.

Closed regressions