Unordered pair multiplicities of an ordered core (light half)

Core.pairMultiplicity and the elementary symmetry, diagonal, row-sum, and positivity facts about it that the pseudocore marker layer consumes. Rehomed from CoreOccurrenceMatching.lean and CubicMatrixReplay.lean (which import this file) so that consumers of these three declarations do not pull in the occurrence-relabeling and replay machinery.

def Utilities.Certificate.ExplicitPotential.Core.pairMultiplicity {n p : ℕ} (core : Core n p) (i j : Fin n) : ℕ

The number of ordered edge slots of core whose two endpoints are exactly the unordered vertex pair {i, j}. Both orientations are counted, so the value is symmetric in i and j.

Equations

• core.pairMultiplicity i j = {edge : Fin p | core.tail edge = i ∧ core.head edge = j ∨ core.tail edge = j ∧ core.head edge = i}.card

theorem Utilities.Certificate.ExplicitPotential.Core.pairMultiplicity_comm {n p : ℕ} (core : Core n p) (i j : Fin n) : core.pairMultiplicity i j = core.pairMultiplicity j i

Unordered multiplicity does not see the order of its two arguments.

theorem Utilities.Certificate.ExplicitPotential.Core.pairMultiplicity_self_eq_zero {n p : ℕ} (core : Core n p) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (i : Fin n) : core.pairMultiplicity i i = 0

A loopless core has zero diagonal in its multiplicity table.

theorem Utilities.Certificate.CubicMatrixReplay.sum_pairMultiplicity_eq_incidenceDegree {n p : ℕ} (core : ExplicitPotential.Core n p) (hLoopless : ∀ (edge : Fin p), core.tail edge ≠ core.head edge) (i : Fin n) : ∑ j : Fin n, core.pairMultiplicity i j = core.incidenceDegree i

On a loopless core the multiplicity row sums are exactly the occurrence incidence degrees. Looplessness is what makes the two endpoint conditions mutually exclusive.

theorem Utilities.Certificate.CubicMatrixReplay.pairMultiplicity_endpoints_pos {n p : ℕ} (core : ExplicitPotential.Core n p) (edge : Fin p) : 0 < core.pairMultiplicity (core.tail edge) (core.head edge)

Each edge slot contributes to the multiplicity of its own endpoint pair.