From cf2e4848fd55c5e115d2d4f8c7a342fc856e4651 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:53:58 +0300 Subject: [PATCH 01/21] Add the combined decorated endpoint reference quotient --- ...on8EndpointDecoratedReferenceQuotient.lean | 124 ++++++++++++++++++ 1 file changed, 124 insertions(+) create mode 100644 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean new file mode 100644 index 00000000..fe995a3d --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean @@ -0,0 +1,124 @@ +import Erdos625.Section8EndpointDecoratedBlockPairings +import Mathlib.Tactic + +/-! +# Section VIII: combined decorated endpoint reference quotient + +A full endpoint table contains two independent finite fibres: + +* the block-level pairing fibre, with its single table-cell factorial quotient; +* the physical full-stub matching fibre inside every selected block pair. + +This module combines their two existing cross-multiplied cardinality identities +before any division. It then casts the result to `ENNReal` and packages the +weighted constant-fibre sum used by the endpoint reference calculation. + +No equivalence with the separately defined physical endpoint fibre, no deficit +sum, no endpoint transportation inequality, and no asymptotic estimate is +asserted here. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- The two finite factorial denominators in the decorated endpoint +parameterization: one for grouping identical block-pair types and one for the +stub bijections inside the selected cells. -/ +def fourEndpointDecoratedDenominator + (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : Nat := + fourEndpointCellFactorialProduct L * + fourEndpointCellStubFactorialProduct alpha hAlpha L + +/-- The corresponding numerator: row-block selections, column-block +selections, and the two endpoint-stub selections in every selected cell. -/ +def fourEndpointDecoratedNumerator + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : Nat := + (fourEndpointRowSelectionProduct alpha hAlpha k L * + fourEndpointColumnSelectionProduct alpha hAlpha k L) * + fourEndpointCellStubSelectionProduct alpha hAlpha L + +/-- Combining the exact block-pairing and per-cell stub-matching identities +introduces no additional multiplicity or factorial. -/ +theorem card_fourEndpointDecoratedBlockPairing_mul_denominator + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : + Fintype.card (FourEndpointDecoratedBlockPairing alpha hAlpha k L) * + fourEndpointDecoratedDenominator alpha hAlpha L = + fourEndpointDecoratedNumerator alpha hAlpha k L := by + have hDecor := + card_fourEndpointDecoratedBlockPairing_mul_cellStubFactorials + alpha hAlpha k L + have hPair := card_fourEndpointBlockPairing_mul_cellFactorials + alpha hAlpha k L + unfold fourEndpointDecoratedDenominator fourEndpointDecoratedNumerator + calc + Fintype.card (FourEndpointDecoratedBlockPairing alpha hAlpha k L) * + (fourEndpointCellFactorialProduct L * + fourEndpointCellStubFactorialProduct alpha hAlpha L) = + (Fintype.card (FourEndpointDecoratedBlockPairing alpha hAlpha k L) * + fourEndpointCellStubFactorialProduct alpha hAlpha L) * + fourEndpointCellFactorialProduct L := by + ac_rfl + _ = (Fintype.card (FourEndpointBlockPairing alpha hAlpha k L) * + fourEndpointCellStubSelectionProduct alpha hAlpha L) * + fourEndpointCellFactorialProduct L := by + rw [hDecor] + _ = (Fintype.card (FourEndpointBlockPairing alpha hAlpha k L) * + fourEndpointCellFactorialProduct L) * + fourEndpointCellStubSelectionProduct alpha hAlpha L := by + ac_rfl + _ = (fourEndpointRowSelectionProduct alpha hAlpha k L * + fourEndpointColumnSelectionProduct alpha hAlpha k L) * + fourEndpointCellStubSelectionProduct alpha hAlpha L := by + rw [hPair] + +/-- The combined factorial denominator is a positive natural number. -/ +theorem fourEndpointDecoratedDenominator_ne_zero + (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : + fourEndpointDecoratedDenominator alpha hAlpha L ≠ 0 := by + simp [fourEndpointDecoratedDenominator, + fourEndpointCellFactorialProduct, + fourEndpointCellStubFactorialProduct] + +/-- Division form of the exact decorated endpoint cardinality in `ENNReal`. +All factors are finite and the denominator is nonzero. -/ +theorem ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : + (Fintype.card (FourEndpointDecoratedBlockPairing alpha hAlpha k L) : ENNReal) = + (fourEndpointDecoratedNumerator alpha hAlpha k L : ENNReal) / + (fourEndpointDecoratedDenominator alpha hAlpha L : ENNReal) := by + apply (ENNReal.eq_div_iff + (Nat.cast_ne_zero.mpr + (fourEndpointDecoratedDenominator_ne_zero alpha hAlpha L)) + (ENNReal.natCast_ne_top _)).2 + simpa only [Nat.cast_mul] using congrArg (fun x : Nat => (x : ENNReal)) + (card_fourEndpointDecoratedBlockPairing_mul_denominator + alpha hAlpha k L) + +/-- A weight constant on the full decorated endpoint fibre sums with exactly +that quotient coefficient. -/ +theorem sum_fourEndpointDecoratedBlockPairing_const_eq_quotient_mul + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) + (weight : ENNReal) : + (∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L, weight) = + ((fourEndpointDecoratedNumerator alpha hAlpha k L : ENNReal) / + (fourEndpointDecoratedDenominator alpha hAlpha L : ENNReal)) * weight := by + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] + rw [ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient] + +#print axioms card_fourEndpointDecoratedBlockPairing_mul_denominator +#print axioms fourEndpointDecoratedDenominator_ne_zero +#print axioms ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient +#print axioms sum_fourEndpointDecoratedBlockPairing_const_eq_quotient_mul + +end + +end Erdos625 From ac61f6cc9533ef94a458b83e7e656ce12a126fc0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:54:12 +0300 Subject: [PATCH 02/21] Add focused CI for the decorated endpoint reference quotient --- ...-section8-decorated-reference-quotient.yml | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 .github/workflows/erdos625-section8-decorated-reference-quotient.yml diff --git a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml new file mode 100644 index 00000000..e1b0a9e4 --- /dev/null +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -0,0 +1,56 @@ +name: Erdős 625 Section 8 decorated reference quotient + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean" + - "625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md" + - "625/audits/LITERATURE_UPDATE_2026-07-25.md" + - ".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 module + shell: bash + run: | + if grep -nE \ + '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean; then + exit 1 + fi + - 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 reference quotient warning-fatally + working-directory: 625/formalization + shell: bash + run: | + set +e + lake build Erdos625.Section8EndpointDecoratedReferenceQuotient --wfail \ + > /tmp/section8-decorated-reference-quotient.log 2>&1 + status=$? + tail -n 500 /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 From 0e7058b52d76da2865513f04836b3ece6b500bae Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:54:34 +0300 Subject: [PATCH 03/21] Document the decorated endpoint reference quotient boundary --- ...ION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md diff --git a/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md b/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md new file mode 100644 index 00000000..f883a743 --- /dev/null +++ b/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md @@ -0,0 +1,97 @@ +# Section VIII decorated endpoint reference quotient audit + +## Purpose + +This module combines two finite enumerations that were previously available +only as separate cross-multiplied identities: + +1. selection and pairing of row and column blocks according to one full + endpoint table; +2. selection and bijective matching of the physical stubs inside every chosen + full endpoint cell. + +The result is an exact coefficient for the full decorated endpoint reference +family. It is a normalization theorem, not an asymptotic estimate. + +## Existing inputs + +For a full endpoint table `L`, the repository already proves + +```text +card(block pairings) * cell-table factorials + = row block selections * column block selections, +``` + +and + +```text +card(decorated block pairings) * cell-stub factorials + = card(block pairings) * cell-stub selections. +``` + +The new module multiplies these identities in the correct order and obtains + +```text +card(decorated block pairings) + * (cell-table factorials * cell-stub factorials) += +(row block selections * column block selections) + * cell-stub selections. +``` + +No cancellation is performed in `Nat`. The denominator is then proved +nonzero and the exact quotient is cast to `ENNReal`. + +## Public declarations + +`Erdos625/Section8EndpointDecoratedReferenceQuotient.lean` proves: + +1. `card_fourEndpointDecoratedBlockPairing_mul_denominator`; +2. `fourEndpointDecoratedDenominator_ne_zero`; +3. `ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient`; +4. `sum_fourEndpointDecoratedBlockPairing_const_eq_quotient_mul`. + +The final theorem says that any weight constant across the decorated endpoint +fibre sums with precisely the combined quotient coefficient. Thus there is no +second table factorial, no hidden ordering of identical block pairs, and no +missing local-stub factorial. + +## Relation to the Section VIII closure problem + +This closes the finite cardinality part of the full-endpoint reference seam. +It supplies the coefficient that must be multiplied by the common local reward +and ambient falling-factorial normalization to recover the endpoint reference +weight `fourEndpointW`. + +The remaining endpoint task is to connect this decorated parameterization to +the separately defined `FourEndpointPhysicalFibre`. The repository already +contains the map + +```text +fourEndpointDecoratedBlockPairingToPhysicalFibre +``` + +and proves that its output is endpoint-only, block-matching, and has the +prescribed full table. A complete equivalence still requires the reverse map +and both round-trip identities, or an equivalent weighted-surjectivity and +injectivity proof. + +After the endpoint reference fibre is closed, the nonendpoint task remains the +aggregate deficit reindexing: every attained canonical high physical skeleton +must be summed as a full endpoint block pairing with one allowed multiplicity +deficit and one partial stub-matching fibre in each selected cell. The exact +one-cell ratio and product majorant are already present elsewhere in the +cumulative stack. + +## Trust boundary + +The focused workflow: + +- rejects `sorry`, `admit`, `sorryAx`, project-defined axioms/constants, and + `unsafe` declarations in the new module; +- builds the exact dependency closure under the pinned Lean 4.31 project with + warnings fatal; +- uploads the compiler log. + +The theorem is finite and exact. It does not establish Lemma 8.3, +Proposition 9.2, or `Erdos625Statement` by itself. From d92b356ffe15d68c46426ed2144b437762400a0b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:55:41 +0300 Subject: [PATCH 04/21] =?UTF-8?q?Add=20the=20July=202026=20Erd=C5=91s=2062?= =?UTF-8?q?5=20literature=20update?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 625/audits/LITERATURE_UPDATE_2026-07-25.md | 147 +++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 625/audits/LITERATURE_UPDATE_2026-07-25.md diff --git a/625/audits/LITERATURE_UPDATE_2026-07-25.md b/625/audits/LITERATURE_UPDATE_2026-07-25.md new file mode 100644 index 00000000..c8e1888d --- /dev/null +++ b/625/audits/LITERATURE_UPDATE_2026-07-25.md @@ -0,0 +1,147 @@ +# 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*, + . +- Annika Heckel, *On a question of Erdős and Gimbel on the cochromatic + number*, Electron. J. Combin. 31 (2024), P4.72; + . +- Annika Heckel, *The difference between the chromatic and the cochromatic + number of a random graph*, . +- 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. Older generalized-chromatic framework missing from the current 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. + +## 4. 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: +. + +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*, . 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. + +## 5. 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. + +## 6. Recommended manuscript changes after proof closure + +1. Update Steiner's reference to the 2025 SIAM journal publication. +2. Add Scheinerman's 1992 generalized-chromatic-number paper to the historical + first-order discussion. +3. Keep the Erdős Problems page as a current-status pointer, not as the primary + source for the original problem. +4. 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. +5. Make no novelty claim for the generic restriction-product lemma without a + separate coding/matroid literature audit. From 047cd2c161f3534053108ac6e366a42bfd7b8e0a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:59:29 +0300 Subject: [PATCH 05/21] Attach the full-cell reward and ambient normalization --- ...tion8EndpointDecoratedReferenceWeight.lean | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean new file mode 100644 index 00000000..4d6fd22e --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean @@ -0,0 +1,66 @@ +import Erdos625.Section8EndpointDecoratedReferenceQuotient +import Mathlib.Tactic + +/-! +# Section VIII: decorated full-endpoint reference weight + +The combined quotient counts all block pairings and all full-cell stub +matchings for one endpoint table. Every object in that finite family has the +same local signed reward and the same ambient falling-factorial normalization. +This module attaches those two factors and records the exact weighted sum. + +The final identification with `fourEndpointW` is deliberately separated from +this theorem: it requires only an algebraic regrouping of the local product, +but no physical-fibre or asymptotic argument. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Product of the signed local rewards of all full endpoint cells in a table. -/ +def fourEndpointFullRewardProduct + (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : ENNReal := + ∏ i : Fin 4, ∏ j : Fin 4, + (localSignRewardNat (fourEndpointOverlapSize alpha hAlpha i j) : ENNReal) ^ + L.toFun i j + +/-- Common contribution of one fully decorated endpoint block pairing after +its literal block and stub choices have been made. -/ +def fourEndpointDecoratedReferenceAtomWeight + (n alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : ENNReal := + fourEndpointFullRewardProduct alpha hAlpha L / + ((n.descFactorial (fourEndpointJ alpha hAlpha L) : Nat) : ENNReal) + +/-- Expanded full-endpoint reference weight obtained by multiplying the exact +decorated cardinality quotient by the common reward/ambient factor. -/ +def fourEndpointDecoratedReferenceQuotientWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : ENNReal := + ((fourEndpointDecoratedNumerator alpha hAlpha k L : Nat) : ENNReal) / + ((fourEndpointDecoratedDenominator alpha hAlpha L : Nat) : ENNReal) * + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L + +/-- The literal finite sum over all block and full-stub decorations is exactly +the expanded endpoint reference weight. -/ +theorem sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : + (∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L) = + fourEndpointDecoratedReferenceQuotientWeight + n alpha hAlpha k L := by + simpa only [fourEndpointDecoratedReferenceQuotientWeight] using + (sum_fourEndpointDecoratedBlockPairing_const_eq_quotient_mul + alpha hAlpha k L + (fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L)) + +#print axioms sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight + +end + +end Erdos625 From b23773df0194d4ad8b322433d711b2b5938af2df Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 21:59:53 +0300 Subject: [PATCH 06/21] Extend focused CI through the decorated reference weight --- .../erdos625-section8-decorated-reference-quotient.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml index e1b0a9e4..6cbda331 100644 --- a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean" + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean" - "625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md" - "625/audits/LITERATURE_UPDATE_2026-07-25.md" - ".github/workflows/erdos625-section8-decorated-reference-quotient.yml" @@ -21,12 +22,13 @@ jobs: runs-on: ubuntu-24.04 steps: - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 - - name: Reject placeholders and project axioms in the new module + - 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; then + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -37,12 +39,12 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the decorated endpoint reference quotient warning-fatally + - name: Build the decorated endpoint reference weight warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8EndpointDecoratedReferenceQuotient --wfail \ + lake build Erdos625.Section8EndpointDecoratedReferenceWeight --wfail \ > /tmp/section8-decorated-reference-quotient.log 2>&1 status=$? tail -n 500 /tmp/section8-decorated-reference-quotient.log From d7b2e542815db068e93e08364afda1a5ee72a57c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:01:50 +0300 Subject: [PATCH 07/21] Identify the decorated endpoint reference sum with W(L) --- ...pointDecoratedReferenceIdentification.lean | 76 +++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean new file mode 100644 index 00000000..42e235b7 --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean @@ -0,0 +1,76 @@ +import Erdos625.Section8EndpointDecoratedReferenceWeight +import Mathlib.Tactic + +/-! +# Section VIII: identify the decorated endpoint reference with `W(L)` + +The preceding modules count the block-pairing and full-stub fibres and attach +the common local reward. This file performs the remaining finite algebraic +regrouping: the manuscript local product is exactly the quotient of the full +stub-selection product by the local stub-factorial product, multiplied by the +signed reward product. + +Consequently the literal sum over decorated endpoint block pairings is exactly +`fourEndpointW`. This is still a statement about the decorated +parameterization; the equivalence with `FourEndpointPhysicalFibre` is a +separate finite theorem. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- The aggregate manuscript local factor is exactly the full-cell stub +selection quotient times the product of signed local rewards. -/ +theorem fourEndpointLocalProduct_eq_stubQuotient_mul_reward + (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : + fourEndpointLocalProduct alpha hAlpha L = + ((fourEndpointCellStubSelectionProduct alpha hAlpha L : Nat) : ENNReal) / + ((fourEndpointCellStubFactorialProduct alpha hAlpha L : Nat) : ENNReal) * + fourEndpointFullRewardProduct alpha hAlpha L := by + unfold fourEndpointLocalProduct fourEndpointLocalCellFactor + fourEndpointCellStubSelectionProduct + fourEndpointCellStubFactorialProduct + fourEndpointFullRewardProduct + push_cast + simp_rw [mul_pow, div_pow] + simp_rw [Finset.prod_mul_distrib, Finset.prod_div_distrib] + +/-- The expanded decorated quotient weight is definitionally the manuscript +endpoint reference weight after the local-product regrouping. -/ +theorem fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : + fourEndpointDecoratedReferenceQuotientWeight n alpha hAlpha k L = + fourEndpointW n alpha hAlpha k L := by + unfold fourEndpointDecoratedReferenceQuotientWeight + fourEndpointDecoratedNumerator fourEndpointDecoratedDenominator + fourEndpointDecoratedReferenceAtomWeight fourEndpointW + rw [fourEndpointLocalProduct_eq_stubQuotient_mul_reward] + push_cast + simp only [div_eq_mul_inv] + ring + +/-- Exact full-endpoint normalization: summing the common reference atom over +all selected block pairings and all full-cell stub matchings gives `W(L)` with +no extra multiplicity. -/ +theorem sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) (L : FourEndpointFullTable) : + (∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L) = + fourEndpointW n alpha hAlpha k L := by + rw [sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight, + fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW] + +#print axioms fourEndpointLocalProduct_eq_stubQuotient_mul_reward +#print axioms fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW +#print axioms sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW + +end + +end Erdos625 From 58ef2b74f3c48025195fe0d6ac14df06fa5e9249 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:02:13 +0300 Subject: [PATCH 08/21] Build the exact W(L) identification in focused CI --- .../erdos625-section8-decorated-reference-quotient.yml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml index 6cbda331..a1871494 100644 --- a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -5,6 +5,7 @@ on: paths: - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean" - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean" + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean" - "625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md" - "625/audits/LITERATURE_UPDATE_2026-07-25.md" - ".github/workflows/erdos625-section8-decorated-reference-quotient.yml" @@ -28,7 +29,8 @@ jobs: if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean \ - 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean; then + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -39,12 +41,12 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the decorated endpoint reference weight warning-fatally + - name: Build the decorated endpoint W(L) identification warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8EndpointDecoratedReferenceWeight --wfail \ + lake build Erdos625.Section8EndpointDecoratedReferenceIdentification --wfail \ > /tmp/section8-decorated-reference-quotient.log 2>&1 status=$? tail -n 500 /tmp/section8-decorated-reference-quotient.log From b6a55b765e78bc66b999d661ccd10e35ee58e347 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:07:23 +0300 Subject: [PATCH 09/21] Discharge the decorated quotient positivity and cast order --- .../Section8EndpointDecoratedReferenceQuotient.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean index fe995a3d..5eb6e741 100644 --- a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean @@ -82,9 +82,9 @@ theorem card_fourEndpointDecoratedBlockPairing_mul_denominator theorem fourEndpointDecoratedDenominator_ne_zero (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : fourEndpointDecoratedDenominator alpha hAlpha L ≠ 0 := by - simp [fourEndpointDecoratedDenominator, - fourEndpointCellFactorialProduct, - fourEndpointCellStubFactorialProduct] + apply Nat.ne_of_gt + unfold fourEndpointDecoratedDenominator + positivity /-- Division form of the exact decorated endpoint cardinality in `ENNReal`. All factors are finite and the denominator is nonzero. -/ @@ -98,9 +98,10 @@ theorem ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient (Nat.cast_ne_zero.mpr (fourEndpointDecoratedDenominator_ne_zero alpha hAlpha L)) (ENNReal.natCast_ne_top _)).2 - simpa only [Nat.cast_mul] using congrArg (fun x : Nat => (x : ENNReal)) - (card_fourEndpointDecoratedBlockPairing_mul_denominator - alpha hAlpha k L) + simpa only [Nat.cast_mul, mul_comm] using + congrArg (fun x : Nat => (x : ENNReal)) + (card_fourEndpointDecoratedBlockPairing_mul_denominator + alpha hAlpha k L) /-- A weight constant on the full decorated endpoint fibre sums with exactly that quotient coefficient. -/ From cfeea0bb52de872bdb382a0b700082ec9fb22bdb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:14:30 +0300 Subject: [PATCH 10/21] Prove decorated factorial positivity cellwise --- ...tion8EndpointDecoratedReferenceQuotient.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean index 5eb6e741..515aa89c 100644 --- a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean @@ -82,9 +82,22 @@ theorem card_fourEndpointDecoratedBlockPairing_mul_denominator theorem fourEndpointDecoratedDenominator_ne_zero (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : fourEndpointDecoratedDenominator alpha hAlpha L ≠ 0 := by - apply Nat.ne_of_gt + have hTable : 0 < fourEndpointCellFactorialProduct L := by + unfold fourEndpointCellFactorialProduct + apply Finset.prod_pos + intro i hi + apply Finset.prod_pos + intro j hj + exact Nat.factorial_pos _ + have hStub : 0 < fourEndpointCellStubFactorialProduct alpha hAlpha L := by + unfold fourEndpointCellStubFactorialProduct + apply Finset.prod_pos + intro i hi + apply Finset.prod_pos + intro j hj + exact pow_pos (Nat.factorial_pos _) _ unfold fourEndpointDecoratedDenominator - positivity + exact mul_ne_zero hTable.ne' hStub.ne' /-- Division form of the exact decorated endpoint cardinality in `ENNReal`. All factors are finite and the denominator is nonzero. -/ From cada6627ef8eb84467e6d4949f7112ad057046e9 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:18:10 +0300 Subject: [PATCH 11/21] =?UTF-8?q?Expand=20the=20Erd=C5=91s=20625=20histori?= =?UTF-8?q?cal=20and=20generalized-coloring=20literature=20audit?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 625/audits/LITERATURE_UPDATE_2026-07-25.md | 89 ++++++++++++++++++---- 1 file changed, 74 insertions(+), 15 deletions(-) diff --git a/625/audits/LITERATURE_UPDATE_2026-07-25.md b/625/audits/LITERATURE_UPDATE_2026-07-25.md index c8e1888d..b51544ac 100644 --- a/625/audits/LITERATURE_UPDATE_2026-07-25.md +++ b/625/audits/LITERATURE_UPDATE_2026-07-25.md @@ -43,7 +43,29 @@ 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. Older generalized-chromatic framework missing from the current draft +## 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 @@ -54,16 +76,49 @@ studies `P`-chromatic numbers for hereditary graph classes. For an infinite hereditary class `P` and fixed `0 *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. Scheinerman therefore supplies useful -historical first-order context, although it does not address the fine -chromatic--cochromatic difference or the `n/(log n)^3` scale. It should be -considered for the background paragraph and bibliography. +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. -Source: -. +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: + +- ; +- . + +## 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. -## 4. Informal two-independent-graph reduction +## 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 @@ -111,7 +166,7 @@ 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. -## 5. Restriction-product theorem and novelty caution +## 7. Restriction-product theorem and novelty caution The cumulative proof stack extracts the finite statement @@ -133,15 +188,19 @@ 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. -## 6. Recommended manuscript changes after proof closure +## 8. Recommended manuscript changes after proof closure 1. Update Steiner's reference to the 2025 SIAM journal publication. -2. Add Scheinerman's 1992 generalized-chromatic-number paper to the historical - first-order discussion. -3. Keep the Erdős Problems page as a current-status pointer, not as the primary +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. -4. Mention the two-independent-graph model only in a concluding-remarks or +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. -5. Make no novelty claim for the generic restriction-product lemma without a +7. Make no novelty claim for the generic restriction-product lemma without a separate coding/matroid literature audit. From a7bd8ee8d2c85ccb8fce32e5722ca023e15bd766 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:19:19 +0300 Subject: [PATCH 12/21] Add missing foundational and generalized cochromatic references --- 625/sources/ERDOS625_REFERENCES.bib | 69 +++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/625/sources/ERDOS625_REFERENCES.bib b/625/sources/ERDOS625_REFERENCES.bib index f116bf7a..8d12de2a 100644 --- a/625/sources/ERDOS625_REFERENCES.bib +++ b/625/sources/ERDOS625_REFERENCES.bib @@ -123,3 +123,72 @@ @misc{scott-2008-2017 url = {https://arxiv.org/abs/0806.0178}, note = {Version 2; first submitted in 2008} } + +@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ő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ő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ás, Bé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} +} From 771ab485e017e030bb43b0a18e121e2e4c9027d8 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:20:29 +0300 Subject: [PATCH 13/21] Add missing cochromatic and generalized-coloring bibliography entries --- 625/arxiv/references.bib | 71 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 70 insertions(+), 1 deletion(-) diff --git a/625/arxiv/references.bib b/625/arxiv/references.bib index 3c378e86..24f73f51 100644 --- a/625/arxiv/references.bib +++ b/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} +} From 7faa8ce1c6b8f18a01b0200636072f361bde0f7c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:21:19 +0300 Subject: [PATCH 14/21] Validate the literature bibliography on the exact PR head --- ...-section8-decorated-reference-quotient.yml | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml index a1871494..a49bfb0b 100644 --- a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -8,6 +8,8 @@ on: - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.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: @@ -33,6 +35,31 @@ jobs: 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.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 From 8c8af1addc5cfb055752307700c6ea88152c300a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:29:44 +0300 Subject: [PATCH 15/21] Close the endpoint W(L) algebra with explicit ENNReal inversion --- .../Section8EndpointDecoratedReferenceIdentification.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean index 42e235b7..e71ba01b 100644 --- a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean @@ -37,8 +37,9 @@ theorem fourEndpointLocalProduct_eq_stubQuotient_mul_reward fourEndpointCellStubFactorialProduct fourEndpointFullRewardProduct push_cast - simp_rw [mul_pow, div_pow] - simp_rw [Finset.prod_mul_distrib, Finset.prod_div_distrib] + simp only [mul_pow, div_pow, Finset.prod_mul_distrib, + Finset.prod_div_distrib] + ring /-- The expanded decorated quotient weight is definitionally the manuscript endpoint reference weight after the local-product regrouping. -/ @@ -53,6 +54,9 @@ theorem fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW rw [fourEndpointLocalProduct_eq_stubQuotient_mul_reward] push_cast simp only [div_eq_mul_inv] + rw [ENNReal.mul_inv + (Or.inr (ENNReal.natCast_ne_top _)) + (Or.inl (ENNReal.natCast_ne_top _))] ring /-- Exact full-endpoint normalization: summing the common reference atom over From f5e72950800131f847d48953be2a8a4b134e47b4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:37:42 +0300 Subject: [PATCH 16/21] Prove the endpoint local quotient by finite cross multiplication --- ...pointDecoratedReferenceIdentification.lean | 114 ++++++++++++++++-- 1 file changed, 103 insertions(+), 11 deletions(-) diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean index e71ba01b..7a1f234d 100644 --- a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean @@ -6,9 +6,9 @@ import Mathlib.Tactic The preceding modules count the block-pairing and full-stub fibres and attach the common local reward. This file performs the remaining finite algebraic -regrouping: the manuscript local product is exactly the quotient of the full -stub-selection product by the local stub-factorial product, multiplied by the -signed reward product. +regrouping. Because `ENNReal` does not support unrestricted cancellation at +zero or infinity, the local product is first compared in cross-multiplied form; +only positive finite factorial factors are then cancelled. Consequently the literal sum over decorated endpoint block pairings is exactly `fourEndpointW`. This is still a statement about the decorated @@ -24,6 +24,88 @@ noncomputable section set_option autoImplicit false +/-- Cross-multiplied local-product identity. Each local factorial is positive +and finite, so its literal full-cell quotient cancels after multiplication by +the same factorial. -/ +theorem fourEndpointLocalProduct_mul_stubFactorialProduct + (alpha : Nat) (hAlpha : 5 < alpha) (L : FourEndpointFullTable) : + fourEndpointLocalProduct alpha hAlpha L * + ((fourEndpointCellStubFactorialProduct alpha hAlpha L : Nat) : ENNReal) = + ((fourEndpointCellStubSelectionProduct alpha hAlpha L : Nat) : ENNReal) * + fourEndpointFullRewardProduct alpha hAlpha L := by + classical + unfold fourEndpointLocalProduct fourEndpointLocalCellFactor + fourEndpointCellStubSelectionProduct + fourEndpointCellStubFactorialProduct + fourEndpointFullRewardProduct + push_cast + let A : Fin 4 → Fin 4 → ENNReal := fun i j => + ((fourEndpointSize alpha hAlpha i).descFactorial + (fourEndpointOverlapSize alpha hAlpha i j) : Nat) + let B : Fin 4 → Fin 4 → ENNReal := fun i j => + ((fourEndpointSize alpha hAlpha j).descFactorial + (fourEndpointOverlapSize alpha hAlpha i j) : Nat) + let F : Fin 4 → Fin 4 → ENNReal := fun i j => + ((fourEndpointOverlapSize alpha hAlpha i j).factorial : Nat) + let R : Fin 4 → Fin 4 → ENNReal := fun i j => + (localSignRewardNat (fourEndpointOverlapSize alpha hAlpha i j) : Nat) + let E : Fin 4 → Fin 4 → Nat := fun i j => L.toFun i j + change + (∏ i : Fin 4, ∏ j : Fin 4, + (((A i j * B i j / F i j) * R i j) ^ E i j)) * + (∏ i : Fin 4, ∏ j : Fin 4, (F i j) ^ E i j) = + (∏ i : Fin 4, ∏ j : Fin 4, (A i j * B i j) ^ E i j) * + (∏ i : Fin 4, ∏ j : Fin 4, (R i j) ^ E i j) + calc + (∏ i : Fin 4, ∏ j : Fin 4, + (((A i j * B i j / F i j) * R i j) ^ E i j)) * + (∏ i : Fin 4, ∏ j : Fin 4, (F i j) ^ E i j) = + ∏ i : Fin 4, + ((∏ j : Fin 4, + (((A i j * B i j / F i j) * R i j) ^ E i j)) * + (∏ j : Fin 4, (F i j) ^ E i j)) := by + rw [← Finset.prod_mul_distrib] + _ = ∏ i : Fin 4, ∏ j : Fin 4, + (((A i j * B i j / F i j) * R i j) ^ E i j) * + (F i j) ^ E i j := by + apply Finset.prod_congr rfl + intro i hi + rw [← Finset.prod_mul_distrib] + _ = ∏ i : Fin 4, ∏ j : Fin 4, + (A i j * B i j) ^ E i j * (R i j) ^ E i j := by + apply Finset.prod_congr rfl + intro i hi + apply Finset.prod_congr rfl + intro j hj + have hF0 : F i j ≠ 0 := by + dsimp [F] + exact_mod_cast (Nat.factorial_pos + (fourEndpointOverlapSize alpha hAlpha i j)).ne' + have hFtop : F i j ≠ ⊤ := by + dsimp [F] + exact ENNReal.natCast_ne_top _ + have hbase : + ((A i j * B i j / F i j) * R i j) * F i j = + (A i j * B i j) * R i j := by + calc + ((A i j * B i j / F i j) * R i j) * F i j = + (A i j * B i j / F i j * F i j) * R i j := by + ac_rfl + _ = (A i j * B i j) * R i j := by + rw [ENNReal.div_mul_cancel hF0 hFtop] + simpa only [mul_pow] using + congrArg (fun z : ENNReal => z ^ E i j) hbase + _ = ∏ i : Fin 4, + ((∏ j : Fin 4, (A i j * B i j) ^ E i j) * + (∏ j : Fin 4, (R i j) ^ E i j)) := by + apply Finset.prod_congr rfl + intro i hi + rw [Finset.prod_mul_distrib] + _ = (∏ i : Fin 4, ∏ j : Fin 4, + (A i j * B i j) ^ E i j) * + (∏ i : Fin 4, ∏ j : Fin 4, (R i j) ^ E i j) := by + rw [Finset.prod_mul_distrib] + /-- The aggregate manuscript local factor is exactly the full-cell stub selection quotient times the product of signed local rewards. -/ theorem fourEndpointLocalProduct_eq_stubQuotient_mul_reward @@ -32,14 +114,23 @@ theorem fourEndpointLocalProduct_eq_stubQuotient_mul_reward ((fourEndpointCellStubSelectionProduct alpha hAlpha L : Nat) : ENNReal) / ((fourEndpointCellStubFactorialProduct alpha hAlpha L : Nat) : ENNReal) * fourEndpointFullRewardProduct alpha hAlpha L := by - unfold fourEndpointLocalProduct fourEndpointLocalCellFactor - fourEndpointCellStubSelectionProduct - fourEndpointCellStubFactorialProduct - fourEndpointFullRewardProduct - push_cast - simp only [mul_pow, div_pow, Finset.prod_mul_distrib, - Finset.prod_div_distrib] - ring + have hStubPos : 0 < fourEndpointCellStubFactorialProduct alpha hAlpha L := by + unfold fourEndpointCellStubFactorialProduct + apply Finset.prod_pos + intro i hi + apply Finset.prod_pos + intro j hj + exact pow_pos (Nat.factorial_pos _) _ + have hStub0 : + ((fourEndpointCellStubFactorialProduct alpha hAlpha L : Nat) : ENNReal) ≠ 0 := by + exact_mod_cast hStubPos.ne' + have hStubTop : + ((fourEndpointCellStubFactorialProduct alpha hAlpha L : Nat) : ENNReal) ≠ ⊤ := + ENNReal.natCast_ne_top _ + rw [← ENNReal.mul_div_right_comm] + apply (ENNReal.eq_div_iff hStub0 hStubTop).2 + simpa only [mul_comm] using + fourEndpointLocalProduct_mul_stubFactorialProduct alpha hAlpha L /-- The expanded decorated quotient weight is definitionally the manuscript endpoint reference weight after the local-product regrouping. -/ @@ -71,6 +162,7 @@ theorem sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW rw [sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight, fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW] +#print axioms fourEndpointLocalProduct_mul_stubFactorialProduct #print axioms fourEndpointLocalProduct_eq_stubQuotient_mul_reward #print axioms fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW #print axioms sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW From 2309328e7429abdb6f5def2174770dbbd9ae132d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:42:24 +0300 Subject: [PATCH 17/21] Synchronize the green Section 9 frontier from the audit base --- .../Erdos625/Section9QOnlySecondMomentFrontier.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean b/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean index 8e31cf6e..803c9494 100644 --- a/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean +++ b/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean @@ -56,7 +56,7 @@ theorem exists_normalizedSignedProfileSecondMoment_qOnly_error_of_bareSkeleton b U k row0 hPhase hcap let epsilon := fun n => epsilonSkeleton n + epsilonAttachment n refine ⟨epsilon, ?_, ?_, ?_⟩ - · simpa only [epsilon] using hSkeletonTendsto.add hAttachmentTendsto + · simpa [epsilon] using hSkeletonTendsto.add hAttachmentTendsto · filter_upwards [hSkeletonNonneg, hAttachmentNonneg] with n hs ha exact add_nonneg hs ha · filter_upwards [hUmin, hSkeleton, hAttachment] with n hUn hs ha @@ -71,7 +71,7 @@ theorem exists_normalizedSignedProfileSecondMoment_qOnly_error_of_bareSkeleton (Real.exp (epsilonSkeleton n * amplificationBase n)) * ENNReal.ofReal (Real.exp (epsilonAttachment n * amplificationBase n)) := by - exact mul_le_mul_right hs _ + exact mul_le_mul_left hs _ _ = ENNReal.ofReal (Real.exp (epsilon n * amplificationBase n)) := by rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), ← Real.exp_add] From 39f75aaa31f27fe6d7f740fa325d5ff25e6358db Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:42:57 +0300 Subject: [PATCH 18/21] Record the exact green endpoint W(L) normalization --- ...ION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md | 134 +++++++++++------- 1 file changed, 86 insertions(+), 48 deletions(-) diff --git a/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md b/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md index f883a743..aec9bb74 100644 --- a/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md +++ b/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md @@ -1,21 +1,22 @@ -# Section VIII decorated endpoint reference quotient audit +# Section VIII decorated endpoint reference audit ## Purpose -This module combines two finite enumerations that were previously available -only as separate cross-multiplied identities: +This stack closes the exact full-endpoint normalization calculation for one +four-type endpoint table. It combines three finite layers: -1. selection and pairing of row and column blocks according to one full - endpoint table; +1. selection and pairing of row and column blocks according to the table; 2. selection and bijective matching of the physical stubs inside every chosen - full endpoint cell. + full endpoint cell; +3. multiplication by the common signed local reward and the ambient + falling-factorial normalization. -The result is an exact coefficient for the full decorated endpoint reference -family. It is a normalization theorem, not an asymptotic estimate. +The final result is the exact manuscript weight `fourEndpointW`. It is a finite +normalization theorem, not an asymptotic estimate. -## Existing inputs +## 1. Combined cardinality quotient -For a full endpoint table `L`, the repository already proves +For a full endpoint table `L`, the repository already proved separately ```text card(block pairings) * cell-table factorials @@ -29,7 +30,8 @@ card(decorated block pairings) * cell-stub factorials = card(block pairings) * cell-stub selections. ``` -The new module multiplies these identities in the correct order and obtains +`Section8EndpointDecoratedReferenceQuotient.lean` multiplies these identities +in the correct order and obtains ```text card(decorated block pairings) @@ -39,59 +41,95 @@ card(decorated block pairings) * cell-stub selections. ``` -No cancellation is performed in `Nat`. The denominator is then proved -nonzero and the exact quotient is cast to `ENNReal`. +No cancellation is performed in `Nat`. The combined denominator is proved +positive, then cast to `ENNReal` and divided only with explicit nonzero and +finite side conditions. -## Public declarations - -`Erdos625/Section8EndpointDecoratedReferenceQuotient.lean` proves: +The public declarations are: 1. `card_fourEndpointDecoratedBlockPairing_mul_denominator`; 2. `fourEndpointDecoratedDenominator_ne_zero`; 3. `ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient`; 4. `sum_fourEndpointDecoratedBlockPairing_const_eq_quotient_mul`. -The final theorem says that any weight constant across the decorated endpoint -fibre sums with precisely the combined quotient coefficient. Thus there is no -second table factorial, no hidden ordering of identical block pairs, and no -missing local-stub factorial. +Thus there is exactly one factorial for identical block-pair types, exactly one +factorial for every local stub bijection, and no hidden ordering multiplicity. + +## 2. Common full-endpoint atom weight -## Relation to the Section VIII closure problem +`Section8EndpointDecoratedReferenceWeight.lean` defines the common contribution +of one fully decorated endpoint block pairing: -This closes the finite cardinality part of the full-endpoint reference seam. -It supplies the coefficient that must be multiplied by the common local reward -and ambient falling-factorial normalization to recover the endpoint reference -weight `fourEndpointW`. +```text +full signed reward product / (n)_{J(L)}. +``` -The remaining endpoint task is to connect this decorated parameterization to -the separately defined `FourEndpointPhysicalFibre`. The repository already -contains the map +It proves that summing this constant atom over the whole decorated endpoint +family is exactly the combined quotient coefficient times that atom: ```text -fourEndpointDecoratedBlockPairingToPhysicalFibre +sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight. ``` -and proves that its output is endpoint-only, block-matching, and has the -prescribed full table. A complete equivalence still requires the reverse map -and both round-trip identities, or an equivalent weighted-surjectivity and -injectivity proof. +## 3. Exact identification with `fourEndpointW` + +The local quotient cannot be simplified in `ENNReal` by an unrestricted +product-of-divisions rule, because such a rule is invalid at zero and infinity. +`Section8EndpointDecoratedReferenceIdentification.lean` therefore proves the +cross-multiplied identity first: + +```text +fourEndpointLocalProduct * cell-stub factorial product + = cell-stub selection product * full signed reward product. +``` + +Every cancelled factorial is a positive finite natural cast. This gives + +```text +fourEndpointLocalProduct + = cell-stub selection quotient * full signed reward product, +``` + +and hence the exact endpoint normalization theorem + +```text +sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW. +``` -After the endpoint reference fibre is closed, the nonendpoint task remains the -aggregate deficit reindexing: every attained canonical high physical skeleton -must be summed as a full endpoint block pairing with one allowed multiplicity -deficit and one partial stub-matching fibre in each selected cell. The exact -one-cell ratio and product majorant are already present elsewhere in the -cumulative stack. +In words: summing over every selected block pairing and every full-cell physical +stub matching with type table `L` gives exactly `fourEndpointW n alpha hAlpha +k L`. No symmetry factor is missing and none is duplicated. -## Trust boundary +The focused Lean 4.31 workflow builds this theorem and its complete dependency +closure under `--wfail`, after rejecting placeholders and project-defined +axioms/constants. The same workflow validates the added bibliography entries. -The focused workflow: +## 4. Relation to the Section VIII closure problem -- rejects `sorry`, `admit`, `sorryAx`, project-defined axioms/constants, and - `unsafe` declarations in the new module; -- builds the exact dependency closure under the pinned Lean 4.31 project with - warnings fatal; -- uploads the compiler log. +This closes the **decorated full-endpoint reference normalization**. It is the +reference measure against which the all-high deficit ratios are charged. -The theorem is finite and exact. It does not establish Lemma 8.3, -Proposition 9.2, or `Erdos625Statement` by itself. +The repository also contains + +```text +fourEndpointDecoratedBlockPairingToPhysicalFibre +``` + +and proves that its output is endpoint-only, block-matching, and has the +prescribed full table. A complete identification with the separately defined +`FourEndpointPhysicalFibre` still requires the reverse construction and the two +round trips, or an equivalent weighted injectivity/surjectivity theorem. + +The remaining nonendpoint task is the aggregate deficit reindexing: every +attained canonical high physical skeleton must be summed over its endpoint block +support, one allowed multiplicity deficit per selected cell, and the associated +partial stub-matching fibre. The exact one-cell ratio, its cross-multiplied +normalization, and the product majorant are already present in the cumulative +stack. + +## 5. Trust boundary + +These results do not by themselves establish Lemma 8.3, Proposition 9.2, or +`Erdos625Statement`. They remove one previously ambiguous normalization seam +from that route. The remaining theorem is now a physical-fibre/deficit +reindexing theorem, not an unresolved endpoint factorial calculation. From 707ebd6eaa781110d9d5de9ea85d055ca6769d1c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:50:03 +0300 Subject: [PATCH 19/21] Prove injectivity of the decorated endpoint physical map --- ...on8EndpointDecoratedPhysicalInjective.lean | 190 ++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean b/625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean new file mode 100644 index 00000000..1625aded --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean @@ -0,0 +1,190 @@ +import Erdos625.Section8EndpointDecoratedPhysicalFibre +import Mathlib.Tactic + +/-! +# Section VIII: injectivity of the decorated endpoint physical map + +The existing map from a block pairing with one literal full-cell stub matching +per selected cell to the physical endpoint fibre must not identify two +different decorated witnesses. This module proves that injectivity directly. + +The proof first recovers the block-level support from the physical full pairs. +After the block pairing is fixed, each local stub matching is recovered from +the physical edges in its selected block cell. +-/ + +namespace Erdos625 + +noncomputable section + +set_option autoImplicit false + +/-- Equality of two physical images of local edges forces equality of the local +stub edges, even when the surrounding decorations differ. -/ +theorem fourEndpointPhysicalEdgeOfLocalEdge_eq_imp + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (P : FourEndpointBlockPairing alpha hAlpha k L) + (dec₁ dec₂ : ∀ e : ↥P.1.edges, + FourEndpointSelectedCellStubMatching alpha hAlpha k L P e) + (e : ↥P.1.edges) + (p q : RowStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.1.1) × + ColumnStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.2.1)) + (hEq : fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P, dec₁⟩ e p = + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P, dec₂⟩ e q) : + p = q := by + apply Prod.ext + · apply Sigma.ext (x := p.1) (y := q.1) rfl + apply heq_of_eq + apply Fin.ext + simpa only [fourEndpointPhysicalEdgeOfLocalEdge] using + congrArg (fun z => z.1.2.val) hEq + · apply Sigma.ext (x := p.2) (y := q.2) rfl + apply heq_of_eq + apply Fin.ext + simpa only [fourEndpointPhysicalEdgeOfLocalEdge] using + congrArg (fun z => z.2.2.val) hEq + +/-- The physical endpoint skeleton determines the selected block-level edge +set of a decorated witness. -/ +theorem fourEndpointDecoratedPhysicalSkeleton_eq_imp_blockEdges_eq + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (D₁ D₂ : FourEndpointDecoratedBlockPairing alpha hAlpha k L) + (hEq : fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₁ = + fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₂) : + D₁.1.1.edges = D₂.1.1.edges := by + ext edge + constructor + · intro hedge + let e₁ : ↥D₁.1.1.edges := ⟨edge, hedge⟩ + have hfull₁ : + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₁.1.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₁.1.2) ∈ + fourEndpointFullPairs alpha hAlpha k + (fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₁) := + (fourEndpointDecoratedPhysicalSkeleton_fullPairs_iff + alpha hAlpha k L slotIndex D₁ _ _).2 ⟨e₁, rfl, rfl⟩ + have hfull₂ : + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₁.1.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₁.1.2) ∈ + fourEndpointFullPairs alpha hAlpha k + (fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₂) := by + simpa only [hEq] using hfull₁ + obtain ⟨e₂, hrow, hcol⟩ := + (fourEndpointDecoratedPhysicalSkeleton_fullPairs_iff + alpha hAlpha k L slotIndex D₂ _ _).1 hfull₂ + have hleft : e₁.1.1 = e₂.1.1 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex hrow + have hright : e₁.1.2 = e₂.1.2 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex hcol + have hedgeEq : edge = e₂.1 := Prod.ext hleft hright + simpa only [hedgeEq] using e₂.2 + · intro hedge + let e₂ : ↥D₂.1.1.edges := ⟨edge, hedge⟩ + have hfull₂ : + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₂.1.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₂.1.2) ∈ + fourEndpointFullPairs alpha hAlpha k + (fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₂) := + (fourEndpointDecoratedPhysicalSkeleton_fullPairs_iff + alpha hAlpha k L slotIndex D₂ _ _).2 ⟨e₂, rfl, rfl⟩ + have hfull₁ : + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₂.1.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e₂.1.2) ∈ + fourEndpointFullPairs alpha hAlpha k + (fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex D₁) := by + simpa only [hEq] using hfull₂ + obtain ⟨e₁, hrow, hcol⟩ := + (fourEndpointDecoratedPhysicalSkeleton_fullPairs_iff + alpha hAlpha k L slotIndex D₁ _ _).1 hfull₁ + have hleft : e₂.1.1 = e₁.1.1 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex hrow + have hright : e₂.1.2 = e₁.1.2 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex hcol + have hedgeEq : edge = e₁.1 := Prod.ext hleft hright + simpa only [hedgeEq] using e₁.2 + +/-- The map from decorated endpoint block pairings to the literal physical +endpoint fibre is injective. -/ +theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_injective + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) : + Function.Injective + (fourEndpointDecoratedBlockPairingToPhysicalFibre + alpha hAlpha k L slotIndex) := by + rintro ⟨P₁, dec₁⟩ ⟨P₂, dec₂⟩ hPhysical + have hSkeleton : + fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex + ⟨P₁, dec₁⟩ = + fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex + ⟨P₂, dec₂⟩ := by + exact congrArg (fun S : FourEndpointPhysicalFibre alpha hAlpha k L => S.1.1) + hPhysical + have hEdges : P₁.1.edges = P₂.1.edges := + fourEndpointDecoratedPhysicalSkeleton_eq_imp_blockEdges_eq + alpha hAlpha k L slotIndex ⟨P₁, dec₁⟩ ⟨P₂, dec₂⟩ hSkeleton + have hPskel : P₁.1 = P₂.1 := UnlabelledTypedSkeleton.ext hEdges + have hP : P₁ = P₂ := Subtype.ext hPskel + subst P₂ + have hdec : dec₁ = dec₂ := by + funext e + have hImage : + (dec₁ e).1.edges.image (fun p => + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₁⟩ e p) = + (dec₂ e).1.edges.image (fun p => + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₂⟩ e p) := by + rw [← fourEndpointDecoratedPhysicalSkeleton_cellEdges_selected + alpha hAlpha k L slotIndex ⟨P₁, dec₁⟩ e] + rw [← fourEndpointDecoratedPhysicalSkeleton_cellEdges_selected + alpha hAlpha k L slotIndex ⟨P₁, dec₂⟩ e] + rw [hSkeleton] + have hLocalEdges : (dec₁ e).1.edges = (dec₂ e).1.edges := by + ext p + constructor + · intro hp + have hpImage : + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₁⟩ e p ∈ + (dec₁ e).1.edges.image (fun q => + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₁⟩ e q) := + Finset.mem_image.mpr ⟨p, hp, rfl⟩ + rw [hImage] at hpImage + obtain ⟨q, hq, hqp⟩ := Finset.mem_image.mp hpImage + have hpq : p = q := + fourEndpointPhysicalEdgeOfLocalEdge_eq_imp + alpha hAlpha k L slotIndex P₁ dec₁ dec₂ e p q hqp.symm + simpa only [hpq] using hq + · intro hp + have hpImage : + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₂⟩ e p ∈ + (dec₂ e).1.edges.image (fun q => + fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex + ⟨P₁, dec₂⟩ e q) := + Finset.mem_image.mpr ⟨p, hp, rfl⟩ + rw [← hImage] at hpImage + obtain ⟨q, hq, hqp⟩ := Finset.mem_image.mp hpImage + have hpq : p = q := + fourEndpointPhysicalEdgeOfLocalEdge_eq_imp + alpha hAlpha k L slotIndex P₁ dec₂ dec₁ e p q hqp.symm + simpa only [hpq] using hq + exact Subtype.ext (UnlabelledTypedSkeleton.ext hLocalEdges) + subst dec₂ + rfl + +#print axioms fourEndpointPhysicalEdgeOfLocalEdge_eq_imp +#print axioms fourEndpointDecoratedPhysicalSkeleton_eq_imp_blockEdges_eq +#print axioms fourEndpointDecoratedBlockPairingToPhysicalFibre_injective + +end + +end Erdos625 From 65584591a15c0e875f9d47ca05345c1fb73e3c03 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 22:50:45 +0300 Subject: [PATCH 20/21] Extend focused CI through physical-map injectivity --- ...rdos625-section8-decorated-reference-quotient.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml index a49bfb0b..7eb39457 100644 --- a/.github/workflows/erdos625-section8-decorated-reference-quotient.yml +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -1,4 +1,4 @@ -name: Erdős 625 Section 8 decorated reference quotient +name: Erdős 625 Section 8 decorated endpoint reference on: pull_request: @@ -6,6 +6,7 @@ on: - "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" @@ -32,7 +33,8 @@ jobs: '(^|[[: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; then + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean; then exit 1 fi - name: Parse added bibliography entries @@ -68,15 +70,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the decorated endpoint W(L) identification warning-fatally + - name: Build the decorated endpoint physical injection warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8EndpointDecoratedReferenceIdentification --wfail \ + lake build Erdos625.Section8EndpointDecoratedPhysicalInjective --wfail \ > /tmp/section8-decorated-reference-quotient.log 2>&1 status=$? - tail -n 500 /tmp/section8-decorated-reference-quotient.log + tail -n 600 /tmp/section8-decorated-reference-quotient.log exit $status - name: Upload focused compiler log if: always() From b5c5eac61dc71140b53a9e7dccc74bb085d0559c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 23:00:21 +0300 Subject: [PATCH 21/21] Construct endpoint block and cell data from a physical fibre --- .../Section8EndpointPhysicalReverseData.lean | 464 ++++++++++++++++++ 1 file changed, 464 insertions(+) create mode 100644 625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean b/625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean new file mode 100644 index 00000000..a2e518e8 --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean @@ -0,0 +1,464 @@ +import Erdos625.Section8EndpointDecoratedPhysicalInjective +import Mathlib.Tactic + +/-! +# Section VIII: reconstruct decorated endpoint data from a physical fibre + +This module constructs the reverse data needed for the endpoint-fibre +equivalence. A physical endpoint fibre member determines: + +* a matching of the four-type block atoms, obtained by pulling back its full + block pairs through a fixed slot indexing; +* one literal full-cell stub matching for every selected block pair, obtained + by pulling back the physical cell edges. + +The round-trip theorem is deliberately placed in a subsequent module. +-/ + +namespace Erdos625 + +open scoped BigOperators + +noncomputable section + +set_option autoImplicit false + +/-- Abstract block atoms used by the four endpoint coordinates. -/ +abbrev FourEndpointBlockAtom (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) := + Σ i : Fin 4, Fin (fourEndpointMultiplicity alpha hAlpha k i) + +/-- A profile block cannot belong to two distinct endpoint-size slot families. -/ +theorem fourEndpointBlockSlots_type_unique + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (a : ProfileBlockIndex k) (i j : Fin 4) + (hi : a ∈ fourEndpointBlockSlots alpha hAlpha k i) + (hj : a ∈ fourEndpointBlockSlots alpha hAlpha k j) : + i = j := by + have hsi : profileBlockMargin k a = fourEndpointSize alpha hAlpha i := by + simpa only [fourEndpointBlockSlots, Finset.mem_filter, + Finset.mem_univ, true_and] using hi + have hsj : profileBlockMargin k a = fourEndpointSize alpha hAlpha j := by + simpa only [fourEndpointBlockSlots, Finset.mem_filter, + Finset.mem_univ, true_and] using hj + have hs : fourEndpointSize alpha hAlpha i = + fourEndpointSize alpha hAlpha j := hsi.symm.trans hsj + have hiCoord := (fourEndpoint_profile_indexing_facts alpha hAlpha k).1 i + have hjCoord := (fourEndpoint_profile_indexing_facts alpha hAlpha k).1 j + rw [hiCoord, hjCoord] at hs + apply Fin.ext + omega + +/-- Pull back the physical full block pairs through the fixed endpoint slot +indexing. -/ +noncomputable def fourEndpointPhysicalBlockEdges + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) : + Finset (FourEndpointBlockAtom alpha hAlpha k × + FourEndpointBlockAtom alpha hAlpha k) := by + classical + exact (Finset.univ.product Finset.univ).filter fun e => + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2) ∈ + fourEndpointFullPairs alpha hAlpha k S.1.1 + +/-- A pulled-back block edge carries the literal full multiplicity associated +with its two endpoint types. -/ +theorem fourEndpointPhysicalBlockEdge_typeTable + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : FourEndpointBlockAtom alpha hAlpha k × + FourEndpointBlockAtom alpha hAlpha k) + (he : e ∈ fourEndpointPhysicalBlockEdges + alpha hAlpha k L slotIndex S) : + S.1.1.typeTable + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1) + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2) = + fourEndpointOverlapSize alpha hAlpha e.1.1 e.2.1 := by + rw [fourEndpointPhysicalBlockEdges, Finset.mem_filter] at he + have hfull := he.2 + rw [fourEndpointFullPairs, Finset.mem_filter] at hfull + obtain ⟨_, i, j, hi, hj, htable⟩ := hfull + have hiOwn : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1 ∈ + fourEndpointBlockSlots alpha hAlpha k e.1.1 := + (slotIndex e.1.1 e.1.2).2 + have hjOwn : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2 ∈ + fourEndpointBlockSlots alpha hAlpha k e.2.1 := + (slotIndex e.2.1 e.2.2).2 + have hei : e.1.1 = i := + fourEndpointBlockSlots_type_unique alpha hAlpha k _ _ _ hiOwn hi + have hej : e.2.1 = j := + fourEndpointBlockSlots_type_unique alpha hAlpha k _ _ _ hjOwn hj + subst i + subst j + exact htable + +/-- The pulled-back physical full pairs form a block-level matching. -/ +noncomputable def fourEndpointPhysicalBlockSkeleton + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) : + UnlabelledTypedSkeleton + (fun i : Fin 4 => fourEndpointMultiplicity alpha hAlpha k i) + (fun j : Fin 4 => fourEndpointMultiplicity alpha hAlpha k j) where + edges := fourEndpointPhysicalBlockEdges alpha hAlpha k L slotIndex S + leftUnique := by + intro x hx y hy hleft + rw [fourEndpointPhysicalBlockEdges, Finset.mem_filter] at hx hy + have hleftActual : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1 = + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1 := + congrArg (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex) hleft + have hrightActual : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2 = + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2 := + S.1.2.2.1 _ _ _ hx.2 hy.2 hleftActual + have hright : x.2 = y.2 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex + hrightActual + exact Prod.ext hleft hright + rightUnique := by + intro x hx y hy hright + rw [fourEndpointPhysicalBlockEdges, Finset.mem_filter] at hx hy + have hrightActual : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2 = + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2 := + congrArg (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex) hright + have hleftActual : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1 = + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1 := + S.1.2.2.2 _ _ _ hx.2 hy.2 hrightActual + have hleft : x.1 = y.1 := + fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex + hleftActual + exact Prod.ext hleft hright + +/-- The block skeleton reconstructed from a physical fibre has exactly the +prescribed full endpoint table. -/ +theorem fourEndpointPhysicalBlockSkeleton_typeTable + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (i j : Fin 4) : + (fourEndpointPhysicalBlockSkeleton alpha hAlpha k L slotIndex S).typeTable + i j = L.toFun i j := by + classical + let source := + (fourEndpointPhysicalBlockEdges alpha hAlpha k L slotIndex S).filter + (fun e => e.1.1 = i ∧ e.2.1 = j) + let target := + ((fourEndpointBlockSlots alpha hAlpha k i).product + (fourEndpointBlockSlots alpha hAlpha k j)).filter + (fun ab => S.1.1.typeTable ab.1 ab.2 = + fourEndpointOverlapSize alpha hAlpha i j) + let F := fun e : FourEndpointBlockAtom alpha hAlpha k × + FourEndpointBlockAtom alpha hAlpha k => + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1, + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2) + have hfin : target = source.image F := by + ext ab + constructor + · intro hab + rw [Finset.mem_filter] at hab + obtain ⟨hprod, htable⟩ := hab + obtain ⟨ha, hb⟩ := Finset.mem_product.mp hprod + let ai := (slotIndex i).symm ⟨ab.1, ha⟩ + let bj := (slotIndex j).symm ⟨ab.2, hb⟩ + let edge : FourEndpointBlockAtom alpha hAlpha k × + FourEndpointBlockAtom alpha hAlpha k := + (⟨i, ai⟩, ⟨j, bj⟩) + have hrow : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.1 = + ab.1 := by + exact congrArg Subtype.val ((slotIndex i).apply_symm_apply ⟨ab.1, ha⟩) + have hcol : + fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.2 = + ab.2 := by + exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨ab.2, hb⟩) + have hedge : edge ∈ + fourEndpointPhysicalBlockEdges alpha hAlpha k L slotIndex S := by + rw [fourEndpointPhysicalBlockEdges, Finset.mem_filter] + constructor + · simp + · rw [fourEndpointFullPairs, Finset.mem_filter] + refine ⟨by simp, i, j, ?_, ?_, ?_⟩ + · simpa only [hrow] using ha + · simpa only [hcol] using hb + · simpa only [hrow, hcol] using htable + rw [Finset.mem_image] + refine ⟨edge, ?_, ?_⟩ + · rw [Finset.mem_filter] + exact ⟨hedge, rfl, rfl⟩ + · exact Prod.ext hrow hcol + · intro hab + rw [Finset.mem_image] at hab + obtain ⟨edge, hedge, rfl⟩ := hab + rw [Finset.mem_filter] at hedge + obtain ⟨hedgeFull, hei, hej⟩ := hedge + rw [Finset.mem_filter] + constructor + · apply Finset.mem_product.mpr + constructor + · simpa only [hei] using (slotIndex edge.1.1 edge.1.2).2 + · simpa only [hej] using (slotIndex edge.2.1 edge.2.2).2 + · simpa only [hei, hej] using + fourEndpointPhysicalBlockEdge_typeTable + alpha hAlpha k L slotIndex S edge hedgeFull + have hFinjective : Function.Injective F := by + intro e₁ e₂ he + exact Prod.ext + (fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex + (congrArg Prod.fst he)) + (fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex + (congrArg Prod.snd he)) + have hSourceTarget : source.card = target.card := by + rw [hfin, Finset.card_image_of_injective] + exact hFinjective + have hTable := congrArg FourEndpointFullTable.toFun S.2 + have hCell := congrFun (congrFun hTable i) j + have hTarget : target.card = L.toFun i j := by + simpa only [target, fourEndpointFullTableOfBlockTypeTable] using hCell + change source.card = L.toFun i j + exact hSourceTarget.trans hTarget + +/-- Reconstructed block pairing over the prescribed full table. -/ +noncomputable def fourEndpointPhysicalBlockPairing + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) : + FourEndpointBlockPairing alpha hAlpha k L := + ⟨fourEndpointPhysicalBlockSkeleton alpha hAlpha k L slotIndex S, by + funext i j + exact fourEndpointPhysicalBlockSkeleton_typeTable + alpha hAlpha k L slotIndex S i j⟩ + +/-- Public cell-cardinality identity for a physical typed matching. -/ +theorem physicalCellEdges_card_eq_typeTable + {I J : Type*} + [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] + {row : I → Nat} {col : J → Nat} + (S : UnlabelledTypedSkeleton row col) (i : I) (j : J) : + (S.cellEdges i j).card = S.typeTable i j := by + unfold UnlabelledTypedSkeleton.cellEdges UnlabelledTypedSkeleton.typeTable + refine Finset.card_bij + (fun p _ => ((⟨i, p.1⟩, ⟨j, p.2⟩) : RowStub row × ColumnStub col)) + ?_ ?_ ?_ + · intro p hp + rw [Finset.mem_filter] at hp ⊢ + exact ⟨hp.2, rfl, rfl⟩ + · intro p₁ hp₁ p₂ hp₂ hEq + exact Prod.ext + (eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.fst hEq)).2) + (eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.snd hEq)).2) + · intro e he + rw [Finset.mem_filter] at he + obtain ⟨hEdge, hI, hJ⟩ := he + obtain ⟨⟨i', r⟩, ⟨j', c⟩⟩ := e + simp only at hI hJ + subst i' + subst j' + exact ⟨(r, c), by simp [hEdge], rfl⟩ + +/-- Pull one physical cell edge back to the corresponding unit-typed local +stub edge. -/ +noncomputable def fourEndpointLocalEdgeOfPhysicalCellEdge + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) + (p : Fin (profileBlockMargin k + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)) × + Fin (profileBlockMargin k + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2))) : + RowStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.1.1) × + ColumnStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.2.1) := + let ha := profileBlockMargin_fourEndpointActualBlockOfAtom + alpha hAlpha k slotIndex e.1.1 + let hb := profileBlockMargin_fourEndpointActualBlockOfAtom + alpha hAlpha k slotIndex e.1.2 + (⟨(), Fin.cast ha p.1⟩, ⟨(), Fin.cast hb p.2⟩) + +/-- The pullback of physical cell edges is injective. -/ +theorem fourEndpointLocalEdgeOfPhysicalCellEdge_injective + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) : + Function.Injective + (fourEndpointLocalEdgeOfPhysicalCellEdge + alpha hAlpha k L slotIndex S e) := by + intro p q hpq + apply Prod.ext + · apply Fin.ext + simpa only [fourEndpointLocalEdgeOfPhysicalCellEdge] using + congrArg (fun z => z.1.2.val) hpq + · apply Fin.ext + simpa only [fourEndpointLocalEdgeOfPhysicalCellEdge] using + congrArg (fun z => z.2.2.val) hpq + +/-- Local physical cell edges, pulled back to unit-typed stub coordinates. -/ +noncomputable def fourEndpointPhysicalCellLocalEdges + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) : + Finset + (RowStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.1.1) × + ColumnStub (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.2.1)) := + (S.1.1.cellEdges + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1) + (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2)).image + (fourEndpointLocalEdgeOfPhysicalCellEdge + alpha hAlpha k L slotIndex S e) + +/-- Pulled-back physical cell matching. -/ +noncomputable def fourEndpointPhysicalCellLocalSkeleton + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) : + UnlabelledTypedSkeleton + (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.1.1) + (fun _ : Unit => fourEndpointSize alpha hAlpha e.1.2.1) where + edges := fourEndpointPhysicalCellLocalEdges + alpha hAlpha k L slotIndex S e + leftUnique := by + intro x hx y hy hleft + rw [fourEndpointPhysicalCellLocalEdges, Finset.mem_image] at hx hy + obtain ⟨p, hp, rfl⟩ := hx + obtain ⟨q, hq, rfl⟩ := hy + have hpFirst : p.1 = q.1 := by + apply Fin.ext + simpa only [fourEndpointLocalEdgeOfPhysicalCellEdge] using + congrArg (fun z => z.1.2.val) hleft + have hpEdge : + ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, p.1⟩, + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, p.2⟩) : + RowStub (profileBlockMargin k) × + ColumnStub (profileBlockMargin k)) ∈ S.1.1.edges := by + simpa [UnlabelledTypedSkeleton.cellEdges] using hp + have hqEdge : + ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, q.1⟩, + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, q.2⟩) : + RowStub (profileBlockMargin k) × + ColumnStub (profileBlockMargin k)) ∈ S.1.1.edges := by + simpa [UnlabelledTypedSkeleton.cellEdges] using hq + have hrow : + (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, p.1⟩ : + RowStub (profileBlockMargin k)) = + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, q.1⟩ := + Sigma.ext rfl (heq_of_eq hpFirst) + have hglobal := S.1.1.leftUnique _ hpEdge _ hqEdge hrow + have hpSecond : p.2 = q.2 := + eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.snd hglobal)).2 + subst q + rfl + rightUnique := by + intro x hx y hy hright + rw [fourEndpointPhysicalCellLocalEdges, Finset.mem_image] at hx hy + obtain ⟨p, hp, rfl⟩ := hx + obtain ⟨q, hq, rfl⟩ := hy + have hpSecond : p.2 = q.2 := by + apply Fin.ext + simpa only [fourEndpointLocalEdgeOfPhysicalCellEdge] using + congrArg (fun z => z.2.2.val) hright + have hpEdge : + ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, p.1⟩, + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, p.2⟩) : + RowStub (profileBlockMargin k) × + ColumnStub (profileBlockMargin k)) ∈ S.1.1.edges := by + simpa [UnlabelledTypedSkeleton.cellEdges] using hp + have hqEdge : + ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, q.1⟩, + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, q.2⟩) : + RowStub (profileBlockMargin k) × + ColumnStub (profileBlockMargin k)) ∈ S.1.1.edges := by + simpa [UnlabelledTypedSkeleton.cellEdges] using hq + have hcol : + (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, p.2⟩ : + ColumnStub (profileBlockMargin k)) = + ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, q.2⟩ := + Sigma.ext rfl (heq_of_eq hpSecond) + have hglobal := S.1.1.rightUnique _ hpEdge _ hqEdge hcol + have hpFirst : p.1 = q.1 := + eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.fst hglobal)).2 + subst q + rfl + +/-- The pulled-back local skeleton has the required full-cell multiplicity. -/ +theorem fourEndpointPhysicalCellLocalSkeleton_typeTable + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) : + (fourEndpointPhysicalCellLocalSkeleton + alpha hAlpha k L slotIndex S e).typeTable () () = + fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1 := by + unfold UnlabelledTypedSkeleton.typeTable + have hAll : + (fourEndpointPhysicalCellLocalEdges alpha hAlpha k L slotIndex S e).filter + (fun z => z.1.1 = () ∧ z.2.1 = ()) = + fourEndpointPhysicalCellLocalEdges alpha hAlpha k L slotIndex S e := by + ext z + simp + rw [hAll] + rw [fourEndpointPhysicalCellLocalEdges, Finset.card_image_of_injective] + · rw [physicalCellEdges_card_eq_typeTable] + exact fourEndpointPhysicalBlockEdge_typeTable + alpha hAlpha k L slotIndex S e.1 e.2 + · exact fourEndpointLocalEdgeOfPhysicalCellEdge_injective + alpha hAlpha k L slotIndex S e + +/-- One reconstructed literal full-cell matching. -/ +noncomputable def fourEndpointPhysicalCellStubMatching + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (S : FourEndpointPhysicalFibre alpha hAlpha k L) + (e : ↥(fourEndpointPhysicalBlockPairing + alpha hAlpha k L slotIndex S).1.edges) : + FourEndpointSelectedCellStubMatching alpha hAlpha k L + (fourEndpointPhysicalBlockPairing alpha hAlpha k L slotIndex S) e := + ⟨fourEndpointPhysicalCellLocalSkeleton alpha hAlpha k L slotIndex S e, + fourEndpointPhysicalCellLocalSkeleton_typeTable + alpha hAlpha k L slotIndex S e⟩ + +/-- Reverse decorated data reconstructed from one physical endpoint fibre +member. -/ +noncomputable def fourEndpointPhysicalFibreToDecoratedBlockPairing + (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) + (L : FourEndpointFullTable) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) : + FourEndpointPhysicalFibre alpha hAlpha k L → + FourEndpointDecoratedBlockPairing alpha hAlpha k L := fun S => + ⟨fourEndpointPhysicalBlockPairing alpha hAlpha k L slotIndex S, + fun e => fourEndpointPhysicalCellStubMatching + alpha hAlpha k L slotIndex S e⟩ + +#print axioms fourEndpointBlockSlots_type_unique +#print axioms fourEndpointPhysicalBlockSkeleton_typeTable +#print axioms physicalCellEdges_card_eq_typeTable +#print axioms fourEndpointPhysicalCellLocalSkeleton_typeTable + +end + +end Erdos625