Kernel-check the exact Section 8 decorated endpoint reference weight

.github/workflows/erdos625-section8-decorated-reference-quotient.yml

@@ -0,0 +1,89 @@
+name: Erdős 625 Section 8 decorated endpoint reference
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean"
+      - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean"
+      - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean"
+      - "625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean"
+      - "625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md"
+      - "625/audits/LITERATURE_UPDATE_2026-07-25.md"
+      - "625/sources/ERDOS625_REFERENCES.bib"
+      - "625/arxiv/references.bib"
+      - ".github/workflows/erdos625-section8-decorated-reference-quotient.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-section8-decorated-reference-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the new modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean \
+            625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean \
+            625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean \
+            625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean; then
+              exit 1
+          fi
+      - name: Parse added bibliography entries
+        run: |
+          python - <<'PY'
+          from pathlib import Path
+
+          required = {
+              "lesniak-straight-1977",
+              "erdos-gimbel-straight-1990",
+              "erdos-gimbel-kratsch-1991",
+              "scheinerman-1992",
+              "bollobas-thomason-1995",
+              "gimbel-kundgen-molloy-2022",
+          }
+          for path in (
+              Path("625/sources/ERDOS625_REFERENCES.bib"),
+              Path("625/arxiv/references.bib"),
+          ):
+              text = path.read_text(encoding="utf-8")
+              missing = sorted(key for key in required if "{" + key + "," not in text)
+              if missing:
+                  raise SystemExit(f"{path}: missing bibliography keys {missing}")
+              if text.count("{") != text.count("}"):
+                  raise SystemExit(f"{path}: unbalanced braces")
+              print(f"{path}: bibliography key and brace checks passed")
+          PY
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the decorated endpoint physical injection warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8EndpointDecoratedPhysicalInjective --wfail \
+            > /tmp/section8-decorated-reference-quotient.log 2>&1
+          status=$?
+          tail -n 600 /tmp/section8-decorated-reference-quotient.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-section8-decorated-reference-quotient-log
+          path: /tmp/section8-decorated-reference-quotient.log
+          if-no-files-found: ignore

625/arxiv/references.bib

@@ -197,7 +197,7 @@ @misc{scott-2008-2017
 }
 
 @misc{achim-et-al-2025,
-  author        = {Achim, Tudor and Best, Alex and Der, Kevin and F{\'e}d{\'e}rico, Math{\"i}s and Gukov, Sergei and Halpern-Leistner, Daniel and Henningsgard, Kirsten and Kudryashov, Yury and Meiburg, Alexander and Michelsen, Martin and Patterson, Riley and Rodriguez, Eric and Scharff, Laura and Shanker, Vikram and Sicca, Vladimir and Sowrirajan, Hari and Swope, Aidan and Tamas, Matyas and Tenev, Vlad and Thomm, Jonathan and Williams, Harold and Wu, Lawrence},
+  author        = {Achim, Tudor and Best, Alex and Der, Kevin and F{\'{e}}d{\'{e}}rico, Math{\"{i}}s and Gukov, Sergei and Halpern-Leistner, Daniel and Henningsgard, Kirsten and Kudryashov, Yury and Meiburg, Alexander and Michelsen, Martin and Patterson, Riley and Rodriguez, Eric and Scharff, Laura and Shanker, Vikram and Sicca, Vladimir and Sowrirajan, Hari and Swope, Aidan and Tamas, Matyas and Tenev, Vlad and Thomm, Jonathan and Williams, Harold and Wu, Lawrence},
   title         = {{Aristotle}: {IMO}-level Automated Theorem Proving},
   year          = {2025},
   eprint        = {2510.01346},
@@ -207,3 +207,72 @@ @misc{achim-et-al-2025
   url           = {https://doi.org/10.48550/arXiv.2510.01346},
   note          = {arXiv:2510.01346; version 2, revised 10 October 2025; DOI 10.48550/arXiv.2510.01346}
 }
+
+@article{lesniak-straight-1977,
+  author  = {Lesniak, Linda and Straight, H. Joseph},
+  title   = {The Cochromatic Number of a Graph},
+  journal = {Ars Combinatoria},
+  volume  = {3},
+  pages   = {39--46},
+  year    = {1977}
+}
+
+@article{erdos-gimbel-straight-1990,
+  author  = {Erd{\H{o}}s, Paul and Gimbel, John and Straight, H. Joseph},
+  title   = {Chromatic Number Versus Cochromatic Number in Graphs with Bounded Clique Number},
+  journal = {European Journal of Combinatorics},
+  volume  = {11},
+  number  = {3},
+  pages   = {235--240},
+  year    = {1990},
+  doi     = {10.1016/S0195-6698(13)80123-0},
+  url     = {https://doi.org/10.1016/S0195-6698(13)80123-0}
+}
+
+@article{erdos-gimbel-kratsch-1991,
+  author  = {Erd{\H{o}}s, Paul and Gimbel, John and Kratsch, Dieter},
+  title   = {Some Extremal Results in Cochromatic and Dichromatic Theory},
+  journal = {Journal of Graph Theory},
+  volume  = {15},
+  number  = {6},
+  pages   = {579--585},
+  year    = {1991},
+  doi     = {10.1002/jgt.3190150604},
+  url     = {https://doi.org/10.1002/jgt.3190150604}
+}
+
+@article{scheinerman-1992,
+  author  = {Scheinerman, Edward R.},
+  title   = {Generalized Chromatic Numbers of Random Graphs},
+  journal = {SIAM Journal on Discrete Mathematics},
+  volume  = {5},
+  number  = {1},
+  pages   = {74--80},
+  year    = {1992},
+  doi     = {10.1137/0405006},
+  url     = {https://doi.org/10.1137/0405006}
+}
+
+@article{bollobas-thomason-1995,
+  author  = {Bollob{\'{a}}s, B{\'{e}}la and Thomason, Andrew},
+  title   = {Generalized Chromatic Numbers of Random Graphs},
+  journal = {Random Structures \& Algorithms},
+  volume  = {6},
+  number  = {2--3},
+  pages   = {353--356},
+  year    = {1995},
+  doi     = {10.1002/rsa.3240060222},
+  url     = {https://doi.org/10.1002/rsa.3240060222}
+}
+
+@article{gimbel-kundgen-molloy-2022,
+  author  = {Gimbel, John and K{\"{u}}ndgen, Andr{\'{e}} and Molloy, Michael},
+  title   = {Fractional Cocoloring of Graphs},
+  journal = {Graphs and Combinatorics},
+  volume  = {38},
+  number  = {3},
+  pages   = {64},
+  year    = {2022},
+  doi     = {10.1007/s00373-022-02463-5},
+  url     = {https://doi.org/10.1007/s00373-022-02463-5}
+}

625/audits/LITERATURE_UPDATE_2026-07-25.md

@@ -0,0 +1,206 @@
+# Erdős 625 literature update
+
+**Search date:** 25 July 2026  
+**Scope:** cochromatic number of `G(n,1/2)`, generalized hereditary
+partition parameters, and the alternative two-independent-graph coupling
+suggested in the Erdős Problems discussion
+
+## 1. Current public status
+
+The Erdős Problems database continues to mark Problem 625 as open. Its current
+summary records:
+
+- the nonconcentration-based lower obstruction of Heckel and, independently,
+  Steiner;
+- Heckel's conjectured scale `n/(log n)^3`;
+- Heckel's positive result for roughly 95 percent of integer values of `n`.
+
+The targeted search did not find an indexed paper, through the search date,
+claiming a full-sequence high-probability lower bound of order
+`n/(log n)^3`. This is a search result, not a claim about unpublished work or
+material absent from the searched indexes.
+
+Primary/current sources:
+
+- Thomas Bloom, *Erdős Problem #625*,
+  <https://www.erdosproblems.com/625>.
+- Annika Heckel, *On a question of Erdős and Gimbel on the cochromatic
+  number*, Electron. J. Combin. 31 (2024), P4.72;
+  <https://arxiv.org/abs/2408.13839>.
+- Annika Heckel, *The difference between the chromatic and the cochromatic
+  number of a random graph*, <https://arxiv.org/abs/2409.17614>.
+- Raphael Steiner, *On the Difference Between the Chromatic and Cochromatic
+  Number*, SIAM J. Discrete Math. 39 (2025), 2268--2274,
+  DOI 10.1137/24M1715180.
+
+## 2. Publication-status correction
+
+Steiner's 2024 preprint is now a journal article. SIAM records acceptance on
+22 September 2025 and online publication on 17 November 2025. The abstract
+states that it gives positive evidence for the Erdős--Gimbel prize question;
+it does not claim the full random-graph resolution pursued here.
+
+The bibliography and introduction should therefore cite the journal version,
+not only the arXiv preprint.
+
+## 3. Foundational cochromatic literature absent from the present background
+
+The present introduction begins with the 1993 problem paper, but the invariant
+and the surrounding comparison questions predate it. A more complete historical
+paragraph should include at least:
+
+1. L. Lesniak and H. J. Straight, *The cochromatic number of a graph*, Ars
+   Combin. 3 (1977), 39--46. This is the standard origin reference for the
+   parameter.
+2. P. Erdős, J. Gimbel, and H. J. Straight, *Chromatic number versus
+   cochromatic number in graphs with bounded clique number*, European J.
+   Combin. 11 (1990), 235--240, DOI 10.1016/S0195-6698(13)80123-0.
+3. P. Erdős, J. Gimbel, and D. Kratsch, *Some extremal results in
+   cochromatic and dichromatic theory*, J. Graph Theory 15 (1991), 579--585,
+   DOI 10.1002/jgt.3190150604.
+4. P. Erdős and J. Gimbel, *Some problems and results in cochromatic theory*,
+   Ann. Discrete Math. 55 (1993), 261--264, which contains the problem used in
+   the manuscript.
+
+Steiner's 2025 paper gives a compact modern map of these three early papers and
+of which associated conjectures and questions have since been settled.
+
+## 4. Generalized-chromatic random-graph framework missing from the draft
+
+Edward R. Scheinerman's
+
+> *Generalized Chromatic Numbers of Random Graphs*, SIAM J. Discrete Math. 5
+> (1992), 74--80, DOI 10.1137/0405006
+
+studies `P`-chromatic numbers for hereditary graph classes. For an infinite
+hereditary class `P` and fixed `0<p<1`, it proves the first-order scale
+`Theta(n/log n)`.
+
+Béla Bollobás and Andrew Thomason subsequently proved the sharper general
+result
+
+> *Generalized chromatic numbers of random graphs*, Random Structures &
+> Algorithms 6 (1995), 353--356, DOI 10.1002/rsa.3240060222.
+
+Their theorem associates an explicit coloring-number parameter `r(P)` with a
+nontrivial hereditary property and gives the corresponding exact first-order
+constant for its generalized chromatic number in a dense random graph.
+
+The cochromatic number is the `P`-chromatic number for the hereditary class
+consisting of complete and empty graphs. These two papers therefore provide the
+proper first-order framework for the present fine comparison. They do not
+address the phase-sensitive difference `chi-zeta`, but they explain why both
+parameters have the same `n/log n` order before the manuscript resolves their
+third-order separation.
+
+Before inserting the Bollobás--Thomason formula into the paper, the manuscript
+should state explicitly how their coloring-number parameter specializes to the
+complete-or-empty hereditary class, rather than leaving the reader to infer it.
+
+Sources:
+
+- <https://epubs.siam.org/doi/10.1137/0405006>;
+- <https://doi.org/10.1002/rsa.3240060222>.
+
+## 5. Adjacent cocoloring literature
+
+John Gimbel, André Kündgen, and Michael Molloy's
+
+> *Fractional Cocoloring of Graphs*, Graphs Combin. 38 (2022), article 64,
+> DOI 10.1007/s00373-022-02463-5
+
+introduces and studies the fractional cochromatic number. Among other results,
+it compares fractional chromatic and cochromatic numbers under clique
+restrictions and determines the maximal order of the fractional parameter up
+to constants.
+
+This does not enter the random-graph second moment, but it is relevant if the
+paper includes a broader related-work paragraph or if a later paper studies a
+fractional or linear-programming relaxation of the signed witness.
+
+## 6. Informal two-independent-graph reduction
+
+The discussion thread for Problem 625 contains an informal reduction reported
+by Zach Hunter and observed with Micha Christoph, Annika Heckel, and Raphael
+Steiner. Sample independent graphs
+
+```text
+G1, G2 ~ G(n,1/2),
+```
+
+and let `X` be the minimum number of parts in a partition in which every part
+is independent in at least one of `G1` or `G2`. The comment states that a
+McDiarmid-coupling argument couples this variable so that
+
+```text
+X >= zeta(G)
+```
+
+for a single `G ~ G(n,1/2)`.
+
+Source:
+<https://www.erdosproblems.com/forum/thread/625>.
+
+This is a discussion comment, not a published theorem with a citable proof in
+the searched literature. It should not be used as an input to the present
+paper without obtaining or supplying the full coupling argument.
+
+### Why it may be useful later
+
+The two-layer model removes explicit clique declarations: a class is assigned
+to layer 1 or layer 2 and must be independent in that layer. Its first moment
+retains the same `2^k` assignment gain that drives the signed four-size
+profile. It may therefore provide:
+
+1. an alternative conceptual interpretation of the signed witness;
+2. a cleaner coupling-based route to comparison with `zeta(G)`;
+3. a separate model in which concentration of `X` and comparison with
+   `chi(G)` can be studied directly.
+
+Recent random-graph papers use McDiarmid's coupling in other transversal or
+multilayer settings; for example Micha Christoph, Anders Martinsson, and
+Aleksa Milojević, *Universality for transversal Hamilton cycles in random
+graphs*, <https://arxiv.org/abs/2505.05385>. This confirms that the technique is
+active, but it does not establish the cochromatic reduction.
+
+For the current manuscript, this direction is a follow-up project rather than
+a replacement for the nearly completed Section VIII--IX proof.
+
+## 7. Restriction-product theorem and novelty caution
+
+The cumulative proof stack extracts the finite statement
+
+```text
+if deletion of I is injective on a finite set family C, then
+sum_{A in C} product_{e in A \ I} q_e
+  <= product_{e notin I} (1+q_e).
+```
+
+For a graph cycle space, deletion of a forest is injective; for a binary
+matroid cycle space, deletion of an independent set is injective. These are
+immediate coding/cycle-space consequences of the generic finite theorem.
+
+The targeted search did not identify a paper presenting this exact weighted
+subset-product inequality under the same name. That absence is not evidence
+of novelty: the statement is elementary and is likely implicit in standard
+cycle-space, coding-theory, or matroid arguments. The present Erdős 625 paper
+should use it as a proof lemma without a novelty claim. A separate follow-up
+would require a dedicated literature review and applications beyond this one
+second-moment problem.
+
+## 8. Recommended manuscript changes after proof closure
+
+1. Update Steiner's reference to the 2025 SIAM journal publication.
+2. Add Lesniak--Straight (1977), Erdős--Gimbel--Straight (1990), and
+   Erdős--Gimbel--Kratsch (1991) to the historical paragraph.
+3. Add Scheinerman (1992) and Bollobás--Thomason (1995) to the first-order
+   random-graph background; the latter is the sharper general antecedent.
+4. Keep the Erdős Problems page as a current-status pointer, not as the primary
+   source for the original problem.
+5. Mention fractional cocoloring only as adjacent work unless the manuscript
+   develops a concrete fractional corollary.
+6. Mention the two-independent-graph model only in a concluding-remarks or
+   future-work paragraph, clearly labelled as an informal external suggestion,
+   unless a complete proof and attribution are obtained.
+7. Make no novelty claim for the generic restriction-product lemma without a
+   separate coding/matroid literature audit.