Audit and standardize graph-theoretic definitions in Erdős 625

[SamPetkov]

Purpose

This PR makes the mathematical vocabulary of Erdős 625 conform explicitly to standard graph-theory and random-graph usage. It is stacked on PR #53 and does not alter the proof theorem chain.

The main conclusion is that the manuscript uses the standard cochromatic invariant, but it must distinguish standard notions from auxiliary bookkeeping more sharply.

Standard definitions confirmed

The audit confirms the usual definitions of:

• finite simple undirected graph;
• independent set and clique;
• chromatic number;
• cocoloring and cochromatic number (\zeta(G));
• (G(n,p)) and “with high probability”;
• falling factorial;
• overlap contingency table;
• uniform bipartite stub matching/configuration model;
• matching and partial matching;
• even subgraph;
• binary cycle space and cycle rank (|E|-|V|+c).

The cochromatic number is also identified with the generalized (\mathcal P)-chromatic number for

P_co = {complete graphs and edgeless graphs}.

The relevant foundational and modern references are already in 625/arxiv/references.bib, including Lesniak–Straight, Scheinerman, Bollobás–Thomason, Heckel, and Steiner.

Terminology corrections

The proposed Version 2 wording:

1. uses “independent set or clique” as the primary cochromatic definition;
2. defines a signed cocoloring witness, explicitly not a new invariant;
3. states that partitions have nonempty, disjoint classes;
4. defines (x)_0=1 and (x)_r=0 for r>x;
5. distinguishes the stub-level configuration perfect matching from the simple support graph H(r);
6. defines c(H) and the empty-graph convention;
7. defines an even subgraph by even degree at every vertex;
8. identifies beta(H) as the binary cycle-space dimension;
9. labels demand, high cell, skeleton, endpoint table, and attachment as manuscript-specific bookkeeping terms.

The distinction between maximum and maximal is also recorded, and the audit warns against replacing the required vertex partition by an overlapping “cover.”

Definition-dependent proof checks

The audit verifies explicitly that:

• the 2^k signed factor uses classes of size at least two, so the independent/clique mark is unique on every realized class;
• the threshold r_ab >= 2 is exactly where a shared internal edge forces sign compatibility;
• equation (6.7) is the standard binary cycle-space cardinality identity;
• the local-cell product in PR Identify attained high-skeleton weights with exact partial-cell fibres #53 requires standard matching support, because nonmatching cells compete for the same row or column stubs;
• the Lean definitions IsBipartiteMatching, IsBipartiteEven, UnlabelledTypedSkeleton, typeTable, and Nat.descFactorial agree with the stated mathematics.

Files

625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md
625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex
625/experiments/check_standard_definitions.py
625/experiments/standard_definition_regression.py
.github/workflows/erdos625-standard-definitions.yml

The TeX insert is intentionally not included by main.tex; it is copy-ready for the final Version 2 rewrite after the theorem-status and line-number audits are synchronized.

Exact finite regression

The standard-library Python regression passed under ordinary and optimized Python. It checked:

simple graphs:                      1099
bipartite support graphs:            682
overlap contingency tables:           25
matching-supported demand tables:    173

The regression verifies:

• zeta(G)=zeta(complement G);
• zeta(G) <= min(chi(G), chi(complement G));
• equality with the generalized P_co-chromatic number;
• uniqueness of the independent/clique mark on classes of size at least two;
• |cycle space| = 2^(|E|-|V|+c) for small bipartite support graphs;
• invariance of the cycle rank under adding or omitting isolated vertices;
• the exact overlap-table law arising from a uniform perfect matching of labelled stubs;
• equality of global and cellwise partial-matching counts on matching-supported demands;
• failure of that cellwise factorization on an explicit nonmatching demand.

These are definition regressions, not evidence for the asymptotic theorem.

Validation

The dedicated workflow is green on

4f26f5f8b99dca379742229baf21bafa8e875169

with workflow run

30259312043.

Both jobs passed:

• source terminology, bibliography-key, TeX, and Lean-definition alignment checks under ordinary and optimized Python;
• the exact finite regression under ordinary and optimized Python, with its output uploaded as an artifact.

Scope boundary

This PR does not close the remaining global Section VIII summation, Proposition 9.2, or Erdos625Statement. It prevents a separate class of errors: proving statements about bespoke proof objects while inadvertently changing the standard graph invariant or configuration-model convention.