From e450b248838123adb4d67a2c98299d19a448390a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:35:59 +0300 Subject: [PATCH 1/7] TEMP accidental --- .../STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md diff --git a/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md b/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md new file mode 100644 index 00000000..b3a42524 --- /dev/null +++ b/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md @@ -0,0 +1 @@ +placeholder \ No newline at end of file From 6115ee1eb4370d613c8a809ee5a351c9758fac6b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:36:18 +0300 Subject: [PATCH 2/7] Remove accidental terminology-audit placeholder --- .../STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md | 1 - 1 file changed, 1 deletion(-) delete mode 100644 625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md diff --git a/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md b/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md deleted file mode 100644 index b3a42524..00000000 --- a/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md +++ /dev/null @@ -1 +0,0 @@ -placeholder \ No newline at end of file From 010b3bdfc7d0573a2f090c190887ae7e73da4944 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:43:37 +0300 Subject: [PATCH 3/7] Add standard graph-theory definitions audit --- ...ITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md | 427 ++++++++++++++++++ 1 file changed, 427 insertions(+) create mode 100644 625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md diff --git a/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md b/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md new file mode 100644 index 00000000..902b256a --- /dev/null +++ b/625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md @@ -0,0 +1,427 @@ +# Erdős 625: standard definitions and terminology audit + +**Audit date:** 27 July 2026 +**Scope:** graph theory, random graphs, probabilistic combinatorics, configuration-model counting, and binary cycle spaces +**Manuscript audited:** `625/arxiv/main.tex` +**Parent proof branch:** PR #53 + +## 1. Verdict + +The manuscript uses the standard mathematical definitions of the chromatic +number, cochromatic number, \(G(n,1/2)\), bipartite matchings, even subgraphs, +and the binary cycle space. The proof does not rely on a nonstandard version +of the cochromatic number. + +The required corrections are principally terminological and expositional: + +1. state the standard definition using **independent sets and cliques**, while + noting the equivalent induced-empty/induced-complete formulation; +2. call the signed object a **signed cocoloring witness**, not a new graph + invariant; +3. define the falling-factorial convention explicitly, including the case + \(r>x\); +4. distinguish the stub-level bipartite configuration model from the simple + support graph derived from its cell counts; +5. define an even subgraph as an edge set of even degree at every vertex and + identify \(eta(H)=|E|-|V|+c(H)\) explicitly as the dimension of the binary + cycle space; +6. label `profile`, `demand`, `high cell`, `skeleton`, `endpoint table`, and + `attachment` as manuscript-specific bookkeeping terms. + +These changes do not alter any theorem. They prevent readers from mistaking +auxiliary proof objects for standard graph invariants and make the hypotheses +of the Section VIII product decomposition transparent. + +## 2. Authoritative usage + +The standard cochromatic definition was introduced by Lesniak and Straight: +the cochromatic number is the minimum number of parts in a partition of the +vertex set such that each part induces an empty or complete graph. Modern work +usually phrases the same definition as the minimum number of colors in a +vertex coloring for which every color class is an independent set or a clique. +The manuscript's notation \(\zeta(G)\) and its partition definition agree with +this usage. + +Relevant references already present in `625/arxiv/references.bib` are: + +- `lesniak-straight-1977`, the origin reference; +- `erdos-gimbel-straight-1990` and `erdos-gimbel-1993`, early cochromatic + theory and the problem source; +- `heckel-2024-question`, `heckel-2025-difference`, and `steiner-2024`, which + use the modern independent-set/clique formulation and the notation + \(\zeta(G)\); +- `scheinerman-1992` and `bollobas-thomason-1995`, for generalized chromatic + numbers associated with hereditary graph properties; +- `janson-luczak-rucinski-2000`, for standard random-graph notation and + high-probability terminology. + +The cochromatic number is also the generalized \(\mathcal P\)-chromatic number +for the hereditary class + +\[ + \mathcal P_{\mathrm{co}} + :=\{K_m,\overline{K_m}:m\ge 0\}. +\] + +Thus + +\[ + \zeta(G)=\chi_{\mathcal P_{\mathrm{co}}}(G). +\] + +This observation is background only; the proof does not invoke a theorem about +generalized chromatic numbers. + +## 3. Standard graph-theoretic definitions + +### 3.1 Graphs, induced subgraphs, independent sets, and cliques + +All graphs in the manuscript are finite, simple, and undirected. For +\(S\subseteq V(G)\), \(G[S]\) is the induced subgraph on \(S\). + +- \(S\) is an **independent set** (also called a stable set) when \(G[S]\) is + edgeless. +- \(S\) is a **clique** when \(G[S]\) is complete. + +The manuscript should consistently use `independent set` and `clique` as the +primary terms. “Induces an empty graph” and “induces a complete graph” are +correct equivalent formulations. + +### 3.2 Partitions and colorings + +A vertex partition means a family of nonempty, pairwise disjoint subsets whose +union is \(V(G)\). Empty color classes are not counted. Ordered and labelled +partitions used later in the proof are auxiliary presentations of such +partitions. + +The chromatic number is + +\[ + \chi(G)=\min\{k:V(G) ext{ is partitioned into }k ext{ independent sets}\}. +\] + +A **cocoloring** is a vertex partition in which each part is an independent set +or a clique. Its parts are cocolor classes. The cochromatic number is + +\[ + \zeta(G)=\min\{k:G ext{ has a cocoloring with }k ext{ classes}\}. +\] + +This is a partition parameter, not an overlapping cover parameter. The paper +should avoid `clique cover` or `cochromatic cover` unless overlap is explicitly +intended. + +Two immediate standard consequences are + +\[ + \zeta(G)=\zeta(\overline G),\qquad + \zeta(G)\le \min\{\chi(G),\chi(\overline G)\}. +\] + +They are not needed for the proof but provide useful consistency checks. + +### 3.3 Random graph and high probability + +\(G(n,p)\) denotes the simple labelled random graph on vertex set +\([n]=\{1,\ldots,n\}\) in which the \(inom n2\) edges are present independently +with probability \(p\). The manuscript fixes \(p=1/2\). + +An event \(E_n\) holds **with high probability** (whp) when + +\[ + \Pr(E_n)\longrightarrow 1 + \qquad(n o\infty). +\] + +The notations \(G(n,1/2)\) and \(G_{n,1/2}\) both occur in the literature. The +manuscript may retain \(G(n,1/2)\), but should use it consistently. + +### 3.4 Falling factorial + +The manuscript uses + +\[ + (x)_r=x(x-1)\cdots(x-r+1),\qquad (x)_0=1. +\] + +For nonnegative integers, the convention must be stated explicitly: + +\[ + (x)_r=0\quad ext{when }r>x. +\] + +This is the convention implemented by Lean's `Nat.descFactorial`. It makes all +finite counting identities total, including infeasible demand tables, and +avoids hidden feasibility hypotheses. + +## 4. Standard probabilistic-combinatorial objects + +### 4.1 Profiles + +A coloring profile is an auxiliary integer vector recording the number of +classes of each allowed size. This usage is common in random graph coloring, +but the exact indexing by deficits from \(\alpha\) is manuscript-specific. + +The paper should distinguish: + +- the abstract profile vector; +- an unordered partition having that profile; +- an ordered or labelled slot presentation used in the second moment. + +Labelling slots multiplies the witness count by a deterministic factorial and +does not change the normalized second moment. + +### 4.2 Overlap matrix + +For ordered partitions \((V_a)_a\) and \((W_b)_b\), the overlap matrix is the +contingency table + +\[ + r_{ab}=|V_a\cap W_b|. +\] + +Its row sums and column sums are the two class-size lists. The law + +\[ + p(r)= rac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{a,b}r_{ab}!} +\] + +is the standard exact law of the overlap contingency table for two independent +uniform ordered partitions with those margins. + +### 4.3 Bipartite configuration model + +The bipartite configuration model used here is the following finite object: + +1. row vertex \(a\) receives \(s_a\) labelled stubs; +2. column vertex \(b\) receives \(t_b\) labelled stubs; +3. the two stub sets have equal total cardinality; +4. choose a uniform perfect matching between the row and column stubs. + +The cell count \(r_{ab}\) is the number of matched stub pairs joining row type +\(a\) to column type \(b\). + +This is a stub-level matching model. It may induce multiple matched pairs +between the same row and column types. It should not be described as a simple +graph. The simple graph \(H(r)\) introduced later is a separate support graph +constructed from the cell counts. + +### 4.4 Matchings and partial matchings + +A matching is an edge set in which no two edges share an endpoint. A partial +matching need not cover all vertices or stubs; a perfect matching covers every +vertex or stub. + +The Section VIII physical skeleton is a partial matching of row and column +stubs. Its positive **type support** is a matching of block types only after +the high-cell threshold and degree caps have been used. These are different +levels: + +- physical matching: edges between individual stubs; +- block-support matching: selected pairs of row and column classes; +- configuration-model perfect matching: all ambient stubs are paired. + +The manuscript and Lean formalization correctly separate these three notions. + +## 5. Binary cycle-space terminology + +### 5.1 Support graph + +For an overlap table \(r\), \(H(r)\) is the simple bipartite graph whose row and +column vertices are the partition slots incident with a cell satisfying +\(r_{ab}\ge2\), and whose edges are those cells. Isolated slot vertices are +omitted. + +Let \(c(H)\) be the number of connected components of this simple graph, with +\(c( arnothing)=0\). The omission of isolated vertices does not change the +quantity \(|E|-|V|+c\), but stating the convention removes ambiguity. + +### 5.2 Even subgraphs + +An even subgraph of \(H\) is an edge set \(F\subseteq E(H)\) such that every +vertex has even degree in the spanning subgraph \((V(H),F)\). It need not be +connected. In the formalization, an even subgraph is represented directly by +its edge set. + +The even edge sets form the binary cycle space under symmetric difference. +Its dimension is + +\[ + eta(H)=|E(H)|-|V(H)|+c(H), +\] + +also called the cycle rank, circuit rank, cyclomatic number, or first Betti +number of \(H\). Therefore + +\[ + |\mathcal C(H)|=2^{eta(H)}. +\] + +The manuscript's equation (6.7) is exactly this standard identity. + +The phrase “independent cycle choices” should be replaced by “elements of the +binary cycle space” or “binary cycle-space degrees of freedom”: an arbitrary +cycle-space element need not be a single simple cycle. + +## 6. The signed witness is auxiliary, not a new invariant + +The term `signed cocoloring` is not a standard graph invariant. The safest +term is **signed cocoloring witness**: + +- start with a vertex partition; +- mark each class by `I` or `K`; +- an `I`-marked class must be independent; +- a `K`-marked class must be a clique. + +For the four-size profile used in the proof, every class has size at least two +for sufficiently large \(n\). Hence a class cannot simultaneously be +independent and a clique, and forgetting the marks identifies realized signed +witnesses with ordinary cocolorings of that fixed partition. + +The factor \(2^k\) is therefore a witness-counting factor, not the definition of +a new cochromatic parameter. The manuscript already states this idea, but the +word `witness` should be incorporated into the formal definition and retained +throughout Section 5. + +## 7. Manuscript-specific terminology + +The following terms are useful but are not standard graph invariants. Each +must be defined locally before use. + +| Term | Exact role | +|---|---| +| deficit coordinate | class size expressed relative to the phase reference \(\alpha\) | +| four-size profile | profile supported on the four selected deficit coordinates | +| demand table | prescribed number of physical stub pairs in each type cell | +| positive demand support | type cells with positive demand | +| high cell | a cell whose multiplicity lies strictly above the selected half-cap | +| endpoint multiplicity | the full-containment reference multiplicity \(\min\{s,t\}\) | +| deficit \(h\) | endpoint multiplicity minus actual multiplicity | +| physical high skeleton | partial matching of actual stubs realizing the high demand table | +| block skeleton/support | matching of row-class and column-class types carrying positive high demand | +| endpoint table | the \(4 imes4\) table counting selected block pairs by endpoint types | +| local reward | the signed-overlap factor attached to one cell multiplicity | +| residual attachment | the remaining local and cycle-space factor after the high skeleton is fixed | + +The use of `skeleton` is legitimate as bespoke terminology, but it must never +be conflated with the graph-theoretic \(k\)-core, a spanning forest, or the +configuration-model multigraph itself. + +## 8. Definition-dependent proof checks + +### 8.1 The \(2^k\) signed first-moment factor + +The factor is valid because: + +1. every chosen class has at least two vertices for all sufficiently large + \(n\); +2. for \(G(n,1/2)\), an \(s\)-set is independent with probability + \(2^{-inom s2}\), and is a clique with the same probability; +3. for \(s\ge2\), the two events are disjoint; +4. the edge constraints inside distinct classes concern disjoint edge sets. + +Thus the marked witness probability for a fixed partition is exactly +\(2^k2^{-B}\), where \(B\) is the total number of prescribed internal edge +bits. + +### 8.2 Threshold \(r_{ab}\ge2\) in the sign support graph + +A cell containing zero or one common vertex contains no internal edge bit +prescribed by both partitions. It imposes no equality between the two class +marks. A cell containing at least two vertices contains at least one shared +internal edge and forces the row and column marks to agree. Hence the support +graph threshold \(r_{ab}\ge2\) is definitionally correct. + +### 8.3 Cycle-space factor + +Compatible marks are constant on each connected component of \(H(r)\), and the +local reward splits one factor from each support edge. The remaining exponent +is \(|E|-|V|+c\), the standard binary cycle-space dimension. Equation (6.4) +does not use a nonstandard notion of cycle. + +### 8.4 Matching-supported local product + +The product of independent one-cell partial matching fibres in PR #53 is valid +only when the positive type support is a matching. If two positive cells share +a row type or column type, their local stub selections compete for the same +ambient stubs and do not factor independently. The standard matching +hypothesis is therefore load-bearing, not cosmetic. + +### 8.5 Maximum versus maximal + +Whenever optimization language is used, `maximum` means largest cardinality +and `maximal` means inclusion-maximal. The manuscript's independence number +uses maximum independent sets. The proof should not substitute `maximal` in +this context. + +## 9. Lean alignment + +The formalization agrees with the standard definitions: + +- `IsBipartiteMatching` states uniqueness of the column neighbor in each row + and uniqueness of the row neighbor in each column; +- `IsBipartiteEven` states even degree at every row and column vertex; +- `UnlabelledTypedSkeleton` is a finite partial matching of typed row and column + stubs; +- `UnlabelledTypedSkeleton.typeTable` counts physical edges by their two types; +- `positiveDemandSupport` is the finite support of nonzero demand cells; +- `Nat.descFactorial` implements the total falling-factorial convention; +- `cycleRank` and the even-edge-set cardinality theorem implement the binary + cycle-space identity. + +The names `UnlabelledTypedSkeleton`, `canonicalDemand`, and `attachment` are +project-specific definitions. Their correctness must be judged by their +explicit fields and theorems, not by importing an external meaning for those +words. + +## 10. Recommended Version 2 wording + +The companion file + +```text +625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex +``` + +contains copy-ready text for the introduction, notation section, signed-witness +definition, configuration-model convention, and cycle-space convention. + +The minimum required manuscript edits are: + +1. cite `lesniak-straight-1977` at the first cochromatic definition; +2. use `independent set or clique` as the primary wording; +3. define a signed cocoloring **witness**; +4. add the total falling-factorial convention; +5. distinguish the stub perfect matching from the simple support graph; +6. define \(c(H)\), even subgraphs, and \(eta(H)\) explicitly; +7. add one sentence declaring the Section VIII vocabulary manuscript-specific. + +## 11. Acceptance checklist + +Before the final TeX is submitted, verify all of the following. + +- [ ] `partition` is explicitly nonempty and disjoint; +- [ ] `cocoloring` is defined by independent-set/clique classes; +- [ ] \(\zeta(G)\) is identified as the cochromatic number introduced by + Lesniak--Straight; +- [ ] `signed cocoloring witness` is not presented as a new invariant; +- [ ] the class-size-\(\ge2\) condition is stated where the \(2^k\) factor is used; +- [ ] \((x)_r\) includes \((x)_0=1\) and the \(r>x\) zero convention; +- [ ] the configuration model is a uniform perfect matching of two stub sets; +- [ ] the support graph \(H(r)\) is explicitly simple; +- [ ] \(c(H)\) and the empty-graph convention are explicit; +- [ ] an even subgraph is defined by even degrees, not by connectedness; +- [ ] \(eta(H)\) is identified with the binary cycle-space dimension; +- [ ] `matching` is used only when no two selected cells share a row or column; +- [ ] all bespoke Section VIII terms are locally defined; +- [ ] no use of `cover` silently replaces the required vertex partition; +- [ ] the mathematical definitions in the TeX and Lean statements agree. + +## 12. Final assessment + +No proof step was found to depend on a nonstandard definition of chromatic or +cochromatic number. The main risk was terminological: the manuscript moves +between ordinary cocolorings, explicitly marked signed witnesses, a stub-level +configuration matching, a simple support graph, and several bespoke skeleton +objects. Once these levels are named separately, the proof's combinatorial +contracts are substantially easier to audit. From f03b24bc269b99d9436fdd39f1eb222a7a8d3caa Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:43:58 +0300 Subject: [PATCH 4/7] Add standard definitions insert for Version 2 --- 625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex | 84 ++++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex diff --git a/625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex b/625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex new file mode 100644 index 00000000..a6fda5b4 --- /dev/null +++ b/625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex @@ -0,0 +1,84 @@ +% Reader-facing terminology insert for the future Version 2 manuscript. +% This file is intentionally not included by main.tex on this branch. + +\subsection*{Conventions and terminology} + +All graphs are finite, simple, and undirected. For a graph \(G\) and +\(S\subseteq V(G)\), write \(G[S]\) for the subgraph induced by \(S\). A set +\(S\) is \emph{independent} if \(G[S]\) is edgeless and is a \emph{clique} if +\(G[S]\) is complete. By a vertex partition we mean a family of nonempty, +pairwise disjoint sets whose union is \(V(G)\). + +A \emph{cocoloring} of \(G\) is a vertex partition in which every class is an +independent set or a clique. The \emph{cochromatic number} \(\zeta(G)\) is the +minimum number of classes in a cocoloring. This is the standard invariant +introduced by Lesniak and Straight \citep{lesniak-straight-1977}; the equivalent +formulation says that every class induces an empty or complete graph. In the +language of generalized chromatic numbers, +\[ + \zeta(G)=\chi_{\mathcal P_{\mathrm{co}}}(G), + \qquad + \mathcal P_{\mathrm{co}}=\{K_m,\overline{K_m}:m\ge0\}, +\] +where \(\mathcal P_{\mathrm{co}}\) is hereditary +\citep{scheinerman-1992,bollobas-thomason-1995}. + +We write \(G(n,p)\) for the simple labelled random graph on +\([n]=\{1,\ldots,n\}\) in which the \(\binom n2\) edges occur independently +with probability \(p\). An event holds \emph{with high probability} if its +probability tends to one as \(n\to\infty\). Throughout the paper \(p=1/2\). + +For nonnegative integers \(x,r\), the falling factorial is +\[ + (x)_r=x(x-1)\cdots(x-r+1), + \qquad (x)_0=1, +\] +with the total convention \((x)_r=0\) when \(r>x\). This convention makes all +finite counting identities valid without a separate feasibility clause. + +\paragraph{Signed witnesses.} +A \emph{signed cocoloring witness} is a vertex partition together with a mark +\(I\) or \(K\) on every class. An \(I\)-marked class is required to be +independent and a \(K\)-marked class is required to be a clique. The marks are +auxiliary counting data, not a new graph invariant. In the four-size profile +used below every class has size at least two for all sufficiently large \(n\), +so a realized class cannot satisfy both marks. Forgetting the marks therefore +recovers an ordinary cocoloring witness without multiplicity. + +\paragraph{Overlap and configuration model.} +For ordered partitions \((V_a)_a\) and \((W_b)_b\), their overlap matrix is the +contingency table +\[ + r_{ab}=|V_a\cap W_b|. +\] +Equivalently, give row slot \(a\) exactly \(s_a\) labelled stubs and column slot +\(b\) exactly \(t_b\) labelled stubs, and choose a uniform perfect matching +between the two stub sets. The number of matched pairs in cell \((a,b)\) is +\(r_{ab}\). This bipartite configuration model is a stub-level matching and +may have several matched pairs between the same two slot types; it is not the +simple support graph defined next. + +\paragraph{Support graph and binary cycle space.} +Let \(H(r)\) be the simple bipartite graph whose edges are the cells +\((a,b)\) satisfying \(r_{ab}\ge2\), with isolated slot vertices omitted. Let +\(c(H)\) denote the number of connected components, with \(c(\varnothing)=0\), +and put +\[ + \beta(H)=|E(H)|-|V(H)|+c(H). +\] +An \emph{even subgraph} is an edge set \(F\subseteq E(H)\) for which every +vertex has even degree in \((V(H),F)\). The even edge sets form the binary cycle +space under symmetric difference, and \(\beta(H)\) is its dimension. Hence +\[ + \#\{F\subseteq E(H):\deg_F(v)\text{ is even for every }v\} + =2^{\beta(H)}. +\] + +\paragraph{Manuscript-specific bookkeeping.} +The terms \emph{deficit coordinate}, \emph{demand table}, \emph{high cell}, +\emph{physical high skeleton}, \emph{block support}, \emph{endpoint table}, +\emph{local reward}, and \emph{residual attachment} are auxiliary terms defined +in the sections where they are used. They do not denote additional standard +graph invariants. In particular, a physical skeleton is a partial matching of +individual row and column stubs, whereas its block support is a matching of row +and column class types. From 62e2aa72ad1b6a19415a4b39b32744de14ed256d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:44:43 +0300 Subject: [PATCH 5/7] Add exact regression for standard graph-theory definitions --- .../standard_definition_regression.py | 311 ++++++++++++++++++ 1 file changed, 311 insertions(+) create mode 100644 625/experiments/standard_definition_regression.py diff --git a/625/experiments/standard_definition_regression.py b/625/experiments/standard_definition_regression.py new file mode 100644 index 00000000..84a8664d --- /dev/null +++ b/625/experiments/standard_definition_regression.py @@ -0,0 +1,311 @@ +#!/usr/bin/env python3 +"""Exact finite checks for the standard definitions used in Erdős 625. + +This verifies small instances of cocoloring, complement invariance, binary cycle +spaces, the overlap-table law of a uniform bipartite stub matching, and the +matching-supported cell-factorization used in Section VIII. It is not evidence +for the main asymptotic theorem. +""" + +from __future__ import annotations + +from collections import Counter +from fractions import Fraction +from itertools import permutations, product +from math import factorial + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def pairs(n: int) -> tuple[tuple[int, int], ...]: + return tuple((i, j) for i in range(n) for j in range(i + 1, n)) + + +def graph_from_code(n: int, code: int) -> frozenset[tuple[int, int]]: + return frozenset(e for bit, e in enumerate(pairs(n)) if code & (1 << bit)) + + +def complement(n: int, edges: frozenset[tuple[int, int]]) -> frozenset[tuple[int, int]]: + return frozenset(set(pairs(n)) - set(edges)) + + +def vertices(mask: int, n: int) -> tuple[int, ...]: + return tuple(v for v in range(n) if mask & (1 << v)) + + +def independent(mask: int, n: int, edges: frozenset[tuple[int, int]]) -> bool: + vs = vertices(mask, n) + return all((i, j) not in edges for i in vs for j in vs if i < j) + + +def clique(mask: int, n: int, edges: frozenset[tuple[int, int]]) -> bool: + vs = vertices(mask, n) + return all((i, j) in edges for i in vs for j in vs if i < j) + + +def minimum_partition_number(n: int, valid: list[bool]) -> int: + dp = [n + 1] * (1 << n) + dp[0] = 0 + for mask in range(1, 1 << n): + first = mask & -mask + sub = mask + while sub: + if sub & first and valid[sub]: + dp[mask] = min(dp[mask], 1 + dp[mask ^ sub]) + sub = (sub - 1) & mask + return dp[-1] + + +def chromatic(n: int, edges: frozenset[tuple[int, int]]) -> int: + valid = [False] + [independent(mask, n, edges) for mask in range(1, 1 << n)] + return minimum_partition_number(n, valid) + + +def cochromatic(n: int, edges: frozenset[tuple[int, int]]) -> int: + valid = [False] + [ + independent(mask, n, edges) or clique(mask, n, edges) + for mask in range(1, 1 << n) + ] + return minimum_partition_number(n, valid) + + +def generalized_pco(n: int, edges: frozenset[tuple[int, int]]) -> int: + """P-chromatic number for P={all complete and all edgeless graphs}.""" + valid = [False] * (1 << n) + for mask in range(1, 1 << n): + valid[mask] = independent(mask, n, edges) or clique(mask, n, edges) + return minimum_partition_number(n, valid) + + +def check_cocoloring(max_n: int = 5) -> int: + count = 0 + for n in range(1, max_n + 1): + for code in range(1 << len(pairs(n))): + edges = graph_from_code(n, code) + comp = complement(n, edges) + zeta = cochromatic(n, edges) + require(zeta == cochromatic(n, comp), f"complement invariance failed: n={n}, code={code}") + require(zeta <= chromatic(n, edges), f"zeta<=chi failed: n={n}, code={code}") + require(zeta <= chromatic(n, comp), f"zeta<=chi(complement) failed: n={n}, code={code}") + require(zeta == generalized_pco(n, edges), f"P_co interpretation failed: n={n}, code={code}") + for mask in range(1, 1 << n): + if mask.bit_count() >= 2: + require( + not (independent(mask, n, edges) and clique(mask, n, edges)), + f"nonunique I/K mark: n={n}, code={code}, mask={mask}", + ) + count += 1 + return count + + +def bipartite_universe(a: int, b: int) -> tuple[tuple[int, int], ...]: + return tuple((i, j) for i in range(a) for j in range(b)) + + +def component_count(a: int, b: int, edges: frozenset[tuple[int, int]], include_isolates: bool) -> int: + left = set(range(a)) if include_isolates else {i for i, _ in edges} + right = set(range(b)) if include_isolates else {j for _, j in edges} + nodes = {(0, i) for i in left} | {(1, j) for j in right} + if not nodes: + return 0 + adjacency = {node: set() for node in nodes} + for i, j in edges: + adjacency[(0, i)].add((1, j)) + adjacency[(1, j)].add((0, i)) + seen: set[tuple[int, int]] = set() + components = 0 + for start in nodes: + if start in seen: + continue + components += 1 + stack = [start] + seen.add(start) + while stack: + node = stack.pop() + for nxt in adjacency[node]: + if nxt not in seen: + seen.add(nxt) + stack.append(nxt) + return components + + +def even_subset(subset: frozenset[tuple[int, int]], a: int, b: int) -> bool: + left = [0] * a + right = [0] * b + for i, j in subset: + left[i] += 1 + right[j] += 1 + return all(value % 2 == 0 for value in left + right) + + +def check_cycle_spaces(max_a: int = 3, max_b: int = 3) -> int: + count = 0 + for a in range(1, max_a + 1): + for b in range(1, max_b + 1): + universe = bipartite_universe(a, b) + for code in range(1 << len(universe)): + edges = frozenset(e for bit, e in enumerate(universe) if code & (1 << bit)) + edge_list = tuple(edges) + number_even = 0 + for subcode in range(1 << len(edge_list)): + subset = frozenset(e for bit, e in enumerate(edge_list) if subcode & (1 << bit)) + number_even += int(even_subset(subset, a, b)) + incident_vertices = len({i for i, _ in edges}) + len({j for _, j in edges}) + beta = len(edges) - incident_vertices + component_count(a, b, edges, False) + beta_spanning = len(edges) - (a + b) + component_count(a, b, edges, True) + require(beta == beta_spanning, "isolated vertices changed cycle rank") + require(number_even == 2**beta, f"cycle-space count failed: {a}x{b}, code={code}") + count += 1 + return count + + +def overlap_table( + row_types: tuple[int, ...], + col_types: tuple[int, ...], + permutation: tuple[int, ...], + a: int, + b: int, +) -> tuple[tuple[int, ...], ...]: + table = [[0] * b for _ in range(a)] + for row_stub, col_stub in enumerate(permutation): + table[row_types[row_stub]][col_types[col_stub]] += 1 + return tuple(tuple(row) for row in table) + + +def overlap_formula( + row_margins: tuple[int, ...], + col_margins: tuple[int, ...], + table: tuple[tuple[int, ...], ...], +) -> int: + numerator = 1 + for value in row_margins + col_margins: + numerator *= factorial(value) + denominator = 1 + for row in table: + for value in row: + denominator *= factorial(value) + require(numerator % denominator == 0, "nonintegral overlap count") + return numerator // denominator + + +def check_overlap_law() -> int: + cases = ( + ((1, 1), (1, 1)), + ((2, 1), (1, 2)), + ((2, 2), (1, 3)), + ((3, 1, 1), (2, 2, 1)), + ((2, 2, 1), (1, 2, 2)), + ) + table_count = 0 + for row_margins, col_margins in cases: + n = sum(row_margins) + require(n == sum(col_margins), "unequal stub totals") + row_types = tuple(i for i, d in enumerate(row_margins) for _ in range(d)) + col_types = tuple(j for j, d in enumerate(col_margins) for _ in range(d)) + counts: Counter[tuple[tuple[int, ...], ...]] = Counter() + for permutation in permutations(range(n)): + counts[overlap_table(row_types, col_types, permutation, len(row_margins), len(col_margins))] += 1 + require(sum(counts.values()) == factorial(n), "perfect matching count failed") + total_probability = Fraction(0, 1) + for table, observed in counts.items(): + expected = overlap_formula(row_margins, col_margins, table) + require(observed == expected, f"overlap law failed: {row_margins}, {col_margins}, {table}") + total_probability += Fraction(expected, factorial(n)) + table_count += 1 + require(total_probability == 1, "overlap probabilities do not sum to one") + return table_count + + +def falling(x: int, r: int) -> int: + if r > x: + return 0 + value = 1 + for offset in range(r): + value *= x - offset + return value + + +def support_is_matching(demand: tuple[tuple[int, ...], ...]) -> bool: + row_hits = [0] * len(demand) + col_hits = [0] * len(demand[0]) + for i, row in enumerate(demand): + for j, value in enumerate(row): + if value: + row_hits[i] += 1 + col_hits[j] += 1 + return all(hit <= 1 for hit in row_hits + col_hits) + + +def global_count( + row_degree: tuple[int, ...], + col_degree: tuple[int, ...], + demand: tuple[tuple[int, ...], ...], +) -> int: + numerator = 1 + for i, degree in enumerate(row_degree): + numerator *= falling(degree, sum(demand[i])) + for j, degree in enumerate(col_degree): + numerator *= falling(degree, sum(demand[i][j] for i in range(len(demand)))) + denominator = 1 + for row in demand: + for value in row: + denominator *= factorial(value) + return numerator // denominator + + +def local_product( + row_degree: tuple[int, ...], + col_degree: tuple[int, ...], + demand: tuple[tuple[int, ...], ...], +) -> int: + value = 1 + for i, row in enumerate(demand): + for j, cell in enumerate(row): + if cell: + value *= falling(row_degree[i], cell) * falling(col_degree[j], cell) // factorial(cell) + return value + + +def check_matching_factorization() -> int: + checked = 0 + degree_cases = (((2, 3), (3, 2)), ((3, 3), (2, 4)), ((2, 3, 2), (3, 2, 2))) + for row_degree, col_degree in degree_cases: + size = len(row_degree) + for entries in product(range(3), repeat=size * size): + demand = tuple(tuple(entries[i * size + j] for j in range(size)) for i in range(size)) + if any(sum(demand[i]) > row_degree[i] for i in range(size)): + continue + if any(sum(demand[i][j] for i in range(size)) > col_degree[j] for j in range(size)): + continue + if support_is_matching(demand): + require(global_count(row_degree, col_degree, demand) == local_product(row_degree, col_degree, demand), "matching cell product failed") + checked += 1 + explicit_nonmatching = ((1, 1), (0, 0)) + require(not support_is_matching(explicit_nonmatching), "counterexample is a matching") + require(global_count((3, 3), (3, 3), explicit_nonmatching) != local_product((3, 3), (3, 3), explicit_nonmatching), "nonmatching support did not expose coupling") + return checked + + +def main() -> None: + graphs = check_cocoloring() + support_graphs = check_cycle_spaces() + overlap_tables = check_overlap_law() + matching_demands = check_matching_factorization() + print("ERDOS 625 STANDARD-DEFINITION REGRESSION: PASS") + print(f" simple graphs checked: {graphs}") + print(f" bipartite support graphs checked: {support_graphs}") + print(f" overlap tables checked: {overlap_tables}") + print(f" matching-supported demand tables checked: {matching_demands}") + print(" verified: zeta(G)=zeta(complement G)") + print(" verified: zeta is the P_co-chromatic number") + print(" verified: |cycle space|=2^(|E|-|V|+c)") + print(" verified: exact uniform-stub overlap law") + print(" verified: local-cell factorization requires matching support") + print(" scope: finite definition checks only") + + +if __name__ == "__main__": + main() From 10f88cb5cc9cde9f49a4433bbf34951e90df34eb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:45:13 +0300 Subject: [PATCH 6/7] Add standard definitions consistency checker --- 625/experiments/check_standard_definitions.py | 170 ++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 625/experiments/check_standard_definitions.py diff --git a/625/experiments/check_standard_definitions.py b/625/experiments/check_standard_definitions.py new file mode 100644 index 00000000..fae9d8bc --- /dev/null +++ b/625/experiments/check_standard_definitions.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Check the Erdős 625 standard-definition audit and terminology insert. + +This validates source coverage, bibliography keys, and agreement with the +relevant Lean structures. It is not a proof of the asymptotic theorem. +""" + +from __future__ import annotations + +import re +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +AUDIT = ROOT / "625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md" +INSERT = ROOT / "625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex" +MAIN = ROOT / "625/arxiv/main.tex" +BIB = ROOT / "625/arxiv/references.bib" +MATCHING = ROOT / "625/formalization/Erdos625/Section9CyclePolymerBound.lean" +SKELETON = ROOT / "625/formalization/Erdos625/Section8UnlabelledTypedSkeleton.lean" +CONFIGURATION = ROOT / "625/formalization/Erdos625/ConfigurationModelProbability.lean" + +REQUIRED_BIB_KEYS = { + "lesniak-straight-1977", + "erdos-gimbel-1993", + "heckel-2024-question", + "heckel-2025-difference", + "steiner-2024", + "scheinerman-1992", + "bollobas-thomason-1995", + "janson-luczak-rucinski-2000", +} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def read(path: Path) -> str: + require(path.is_file(), f"missing required file: {path}") + return path.read_text(encoding="utf-8") + + +def extract_bib_keys(text: str) -> set[str]: + return set(re.findall(r"@[A-Za-z]+\{([^,]+),", text)) + + +def check_insert(text: str) -> None: + markers = ( + "All graphs are finite, simple, and undirected", + "A \\emph{cocoloring}", + "cochromatic number", + "signed cocoloring witness", + "not a new graph invariant", + "(x)_0=1", + "when \(r>x\)", + "uniform perfect matching", + "stub-level matching", + "simple bipartite graph", + "c(\\varnothing)=0", + "even subgraph", + "binary cycle space", + "partial matching", + "Manuscript-specific bookkeeping", + ) + missing = [marker for marker in markers if marker not in text] + require(not missing, f"definition insert missing markers: {missing}") + require(text.count("{") == text.count("}"), "unbalanced braces in TeX insert") + require("\\tag{" not in text, "manual equation tags are forbidden in TeX insert") + require("clique cover" not in text.lower(), "ambiguous cover terminology in TeX insert") + require("empty or complete graph" in text, "historical equivalent definition absent") + + +def check_audit(text: str) -> None: + markers = ( + "standard definitions and terminology audit", + "independent sets and cliques", + "generalized \\(\\mathcal P\\)-chromatic number", + "partition parameter, not an overlapping cover parameter", + "Falling factorial", + "Bipartite configuration model", + "Binary cycle-space terminology", + "signed witness is auxiliary, not a new invariant", + "Manuscript-specific terminology", + "Definition-dependent proof checks", + "Lean alignment", + "Acceptance checklist", + "No proof step was found to depend on a nonstandard definition", + ) + missing = [marker for marker in markers if marker not in text] + require(not missing, f"definition audit missing markers: {missing}") + require("maximum versus maximal" in text.lower(), "maximum/maximal distinction absent") + require("clique cover" in text.lower(), "cover warning absent") + require("2^k" in text, "signed-witness factor check absent") + require("r_{ab}\\ge2" in text, "support-graph threshold check absent") + + +def check_canonical_source(text: str) -> None: + require( + "The cochromatic number \\(\\zeta(G)\\) is the least number of parts" in text, + "canonical cochromatic definition changed; refresh audit", + ) + require( + "A \\emph{signed cocoloring} is a partition" in text, + "canonical signed-witness wording changed; refresh audit", + ) + require( + "Let \\(H(r)\\) be the simple bipartite graph" in text, + "canonical support graph changed; refresh audit", + ) + require( + "the even\nsubgraphs form the binary cycle space" in text, + "canonical cycle-space statement changed; refresh audit", + ) + + +def check_lean(matching: str, skeleton: str, configuration: str) -> None: + for marker in ( + "def IsBipartiteEven", + "∀ a, Even", + "∀ b, Even", + "def IsBipartiteMatching", + "no two cells share a row or column", + ): + require(marker in matching, f"formal matching/even definition missing: {marker}") + for marker in ( + "structure UnlabelledTypedSkeleton", + "edges : Finset", + "leftUnique", + "rightUnique", + "def UnlabelledTypedSkeleton.typeTable", + ): + require(marker in skeleton, f"formal skeleton definition missing: {marker}") + for marker in ( + "def totalDemand", + "def demandFactorialProduct", + "def rowDescendingProduct", + "def columnDescendingProduct", + ): + require(marker in configuration, f"configuration counting definition missing: {marker}") + + +def main() -> None: + audit = read(AUDIT) + insert = read(INSERT) + main_tex = read(MAIN) + bibliography = read(BIB) + matching = read(MATCHING) + skeleton = read(SKELETON) + configuration = read(CONFIGURATION) + + missing_keys = sorted(REQUIRED_BIB_KEYS - extract_bib_keys(bibliography)) + require(not missing_keys, f"bibliography keys missing: {missing_keys}") + check_insert(insert) + check_audit(audit) + check_canonical_source(main_tex) + check_lean(matching, skeleton, configuration) + + print("ERDOS 625 STANDARD-DEFINITION SOURCE CHECK: PASS") + print(f" bibliography keys checked: {len(REQUIRED_BIB_KEYS)}") + print(" standard invariants and auxiliary witness terminology separated") + print(" configuration matching and simple support graph separated") + print(" even-subgraph and binary cycle-space conventions aligned") + print(" Lean structures agree with the stated mathematical definitions") + print(" scope: source consistency only") + + +if __name__ == "__main__": + main() From 4f26f5f8b99dca379742229baf21bafa8e875169 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Mon, 27 Jul 2026 13:45:27 +0300 Subject: [PATCH 7/7] Add standard definitions audit workflow --- .../erdos625-standard-definitions.yml | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 .github/workflows/erdos625-standard-definitions.yml diff --git a/.github/workflows/erdos625-standard-definitions.yml b/.github/workflows/erdos625-standard-definitions.yml new file mode 100644 index 00000000..5eb4a661 --- /dev/null +++ b/.github/workflows/erdos625-standard-definitions.yml @@ -0,0 +1,55 @@ +name: Erdős 625 standard definitions and terminology + +on: + pull_request: + paths: + - "625/audits/STANDARD_DEFINITIONS_AND_TERMINOLOGY_AUDIT_2026-07-27.md" + - "625/arxiv/STANDARD_DEFINITIONS_INSERT_V2.tex" + - "625/arxiv/main.tex" + - "625/arxiv/references.bib" + - "625/experiments/check_standard_definitions.py" + - "625/experiments/standard_definition_regression.py" + - "625/formalization/Erdos625/Section9CyclePolymerBound.lean" + - "625/formalization/Erdos625/Section8UnlabelledTypedSkeleton.lean" + - "625/formalization/Erdos625/ConfigurationModelProbability.lean" + - ".github/workflows/erdos625-standard-definitions.yml" + workflow_dispatch: + +concurrency: + group: erdos625-standard-definitions-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + terminology-source-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Compile source checker + run: python -m py_compile 625/experiments/check_standard_definitions.py + - name: Check definitions, citations, and Lean alignment + run: python 625/experiments/check_standard_definitions.py + - name: Repeat source checker under optimized Python + run: python -O 625/experiments/check_standard_definitions.py + + exact-definition-regression: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Compile exact regression + run: python -m py_compile 625/experiments/standard_definition_regression.py + - name: Run exact finite definition regression + shell: bash + run: | + python 625/experiments/standard_definition_regression.py \ + | tee /tmp/erdos625-standard-definition-regression.log + - name: Repeat regression under optimized Python + run: python -O 625/experiments/standard_definition_regression.py + - uses: actions/upload-artifact@v4 + if: always() + with: + name: erdos625-standard-definition-regression + path: /tmp/erdos625-standard-definition-regression.log + if-no-files-found: error