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..7eb39457 --- /dev/null +++ b/.github/workflows/erdos625-section8-decorated-reference-quotient.yml @@ -0,0 +1,89 @@ +name: Erdős 625 Section 8 decorated endpoint reference + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean" + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean" + - "625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean" + - "625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean" + - "625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md" + - "625/audits/LITERATURE_UPDATE_2026-07-25.md" + - "625/sources/ERDOS625_REFERENCES.bib" + - "625/arxiv/references.bib" + - ".github/workflows/erdos625-section8-decorated-reference-quotient.yml" + workflow_dispatch: + +concurrency: + group: erdos625-section8-decorated-reference-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + focused-lean-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Reject placeholders and project axioms in the new modules + shell: bash + run: | + if grep -nE \ + '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean \ + 625/formalization/Erdos625/Section8EndpointDecoratedPhysicalInjective.lean; then + exit 1 + fi + - name: Parse added bibliography entries + run: | + python - <<'PY' + from pathlib import Path + + required = { + "lesniak-straight-1977", + "erdos-gimbel-straight-1990", + "erdos-gimbel-kratsch-1991", + "scheinerman-1992", + "bollobas-thomason-1995", + "gimbel-kundgen-molloy-2022", + } + for path in ( + Path("625/sources/ERDOS625_REFERENCES.bib"), + Path("625/arxiv/references.bib"), + ): + text = path.read_text(encoding="utf-8") + missing = sorted(key for key in required if "{" + key + "," not in text) + if missing: + raise SystemExit(f"{path}: missing bibliography keys {missing}") + if text.count("{") != text.count("}"): + raise SystemExit(f"{path}: unbalanced braces") + print(f"{path}: bibliography key and brace checks passed") + PY + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 + with: + lake-package-directory: 625/formalization + auto-config: false + build: false + use-mathlib-cache: true + use-github-cache: false + nanoda: false + - name: Build the decorated endpoint physical injection warning-fatally + working-directory: 625/formalization + shell: bash + run: | + set +e + lake build Erdos625.Section8EndpointDecoratedPhysicalInjective --wfail \ + > /tmp/section8-decorated-reference-quotient.log 2>&1 + status=$? + tail -n 600 /tmp/section8-decorated-reference-quotient.log + exit $status + - name: Upload focused compiler log + if: always() + uses: actions/upload-artifact@v4 + with: + name: erdos625-section8-decorated-reference-quotient-log + path: /tmp/section8-decorated-reference-quotient.log + if-no-files-found: ignore 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} +} 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..b51544ac --- /dev/null +++ b/625/audits/LITERATURE_UPDATE_2026-07-25.md @@ -0,0 +1,206 @@ +# Erdős 625 literature update + +**Search date:** 25 July 2026 +**Scope:** cochromatic number of `G(n,1/2)`, generalized hereditary +partition parameters, and the alternative two-independent-graph coupling +suggested in the Erdős Problems discussion + +## 1. Current public status + +The Erdős Problems database continues to mark Problem 625 as open. Its current +summary records: + +- the nonconcentration-based lower obstruction of Heckel and, independently, + Steiner; +- Heckel's conjectured scale `n/(log n)^3`; +- Heckel's positive result for roughly 95 percent of integer values of `n`. + +The targeted search did not find an indexed paper, through the search date, +claiming a full-sequence high-probability lower bound of order +`n/(log n)^3`. This is a search result, not a claim about unpublished work or +material absent from the searched indexes. + +Primary/current sources: + +- Thomas Bloom, *Erdős Problem #625*, + . +- 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. Foundational cochromatic literature absent from the present background + +The present introduction begins with the 1993 problem paper, but the invariant +and the surrounding comparison questions predate it. A more complete historical +paragraph should include at least: + +1. L. Lesniak and H. J. Straight, *The cochromatic number of a graph*, Ars + Combin. 3 (1977), 39--46. This is the standard origin reference for the + parameter. +2. P. Erdős, J. Gimbel, and H. J. Straight, *Chromatic number versus + cochromatic number in graphs with bounded clique number*, European J. + Combin. 11 (1990), 235--240, DOI 10.1016/S0195-6698(13)80123-0. +3. P. Erdős, J. Gimbel, and D. Kratsch, *Some extremal results in + cochromatic and dichromatic theory*, J. Graph Theory 15 (1991), 579--585, + DOI 10.1002/jgt.3190150604. +4. P. Erdős and J. Gimbel, *Some problems and results in cochromatic theory*, + Ann. Discrete Math. 55 (1993), 261--264, which contains the problem used in + the manuscript. + +Steiner's 2025 paper gives a compact modern map of these three early papers and +of which associated conjectures and questions have since been settled. + +## 4. Generalized-chromatic random-graph framework missing from the draft + +Edward R. Scheinerman's + +> *Generalized Chromatic Numbers of Random Graphs*, SIAM J. Discrete Math. 5 +> (1992), 74--80, DOI 10.1137/0405006 + +studies `P`-chromatic numbers for hereditary graph classes. For an infinite +hereditary class `P` and fixed `0 *Generalized chromatic numbers of random graphs*, Random Structures & +> Algorithms 6 (1995), 353--356, DOI 10.1002/rsa.3240060222. + +Their theorem associates an explicit coloring-number parameter `r(P)` with a +nontrivial hereditary property and gives the corresponding exact first-order +constant for its generalized chromatic number in a dense random graph. + +The cochromatic number is the `P`-chromatic number for the hereditary class +consisting of complete and empty graphs. These two papers therefore provide the +proper first-order framework for the present fine comparison. They do not +address the phase-sensitive difference `chi-zeta`, but they explain why both +parameters have the same `n/log n` order before the manuscript resolves their +third-order separation. + +Before inserting the Bollobás--Thomason formula into the paper, the manuscript +should state explicitly how their coloring-number parameter specializes to the +complete-or-empty hereditary class, rather than leaving the reader to infer it. + +Sources: + +- ; +- . + +## 5. Adjacent cocoloring literature + +John Gimbel, André Kündgen, and Michael Molloy's + +> *Fractional Cocoloring of Graphs*, Graphs Combin. 38 (2022), article 64, +> DOI 10.1007/s00373-022-02463-5 + +introduces and studies the fractional cochromatic number. Among other results, +it compares fractional chromatic and cochromatic numbers under clique +restrictions and determines the maximal order of the fractional parameter up +to constants. + +This does not enter the random-graph second moment, but it is relevant if the +paper includes a broader related-work paragraph or if a later paper studies a +fractional or linear-programming relaxation of the signed witness. + +## 6. Informal two-independent-graph reduction + +The discussion thread for Problem 625 contains an informal reduction reported +by Zach Hunter and observed with Micha Christoph, Annika Heckel, and Raphael +Steiner. Sample independent graphs + +```text +G1, G2 ~ G(n,1/2), +``` + +and let `X` be the minimum number of parts in a partition in which every part +is independent in at least one of `G1` or `G2`. The comment states that a +McDiarmid-coupling argument couples this variable so that + +```text +X >= zeta(G) +``` + +for a single `G ~ G(n,1/2)`. + +Source: +. + +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. + +## 7. Restriction-product theorem and novelty caution + +The cumulative proof stack extracts the finite statement + +```text +if deletion of I is injective on a finite set family C, then +sum_{A in C} product_{e in A \ I} q_e + <= product_{e notin I} (1+q_e). +``` + +For a graph cycle space, deletion of a forest is injective; for a binary +matroid cycle space, deletion of an independent set is injective. These are +immediate coding/cycle-space consequences of the generic finite theorem. + +The targeted search did not identify a paper presenting this exact weighted +subset-product inequality under the same name. That absence is not evidence +of novelty: the statement is elementary and is likely implicit in standard +cycle-space, coding-theory, or matroid arguments. The present Erdős 625 paper +should use it as a proof lemma without a novelty claim. A separate follow-up +would require a dedicated literature review and applications beyond this one +second-moment problem. + +## 8. Recommended manuscript changes after proof closure + +1. Update Steiner's reference to the 2025 SIAM journal publication. +2. Add Lesniak--Straight (1977), Erdős--Gimbel--Straight (1990), and + Erdős--Gimbel--Kratsch (1991) to the historical paragraph. +3. Add Scheinerman (1992) and Bollobás--Thomason (1995) to the first-order + random-graph background; the latter is the sharper general antecedent. +4. Keep the Erdős Problems page as a current-status pointer, not as the primary + source for the original problem. +5. Mention fractional cocoloring only as adjacent work unless the manuscript + develops a concrete fractional corollary. +6. Mention the two-independent-graph model only in a concluding-remarks or + future-work paragraph, clearly labelled as an informal external suggestion, + unless a complete proof and attribution are obtained. +7. Make no novelty claim for the generic restriction-product lemma without a + separate coding/matroid literature audit. 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 diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean new file mode 100644 index 00000000..7a1f234d --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean @@ -0,0 +1,172 @@ +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. 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 +parameterization; the equivalence with `FourEndpointPhysicalFibre` is a +separate finite theorem. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +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 + (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 + 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. -/ +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] + 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 +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_mul_stubFactorialProduct +#print axioms fourEndpointLocalProduct_eq_stubQuotient_mul_reward +#print axioms fourEndpointDecoratedReferenceQuotientWeight_eq_fourEndpointW +#print axioms sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW + +end + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean new file mode 100644 index 00000000..515aa89c --- /dev/null +++ b/625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean @@ -0,0 +1,138 @@ +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 + 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 + 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. -/ +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, 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. -/ +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 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 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 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] 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..aec9bb74 --- /dev/null +++ b/625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md @@ -0,0 +1,135 @@ +# Section VIII decorated endpoint reference audit + +## Purpose + +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 the table; +2. selection and bijective matching of the physical stubs inside every chosen + full endpoint cell; +3. multiplication by the common signed local reward and the ambient + falling-factorial normalization. + +The final result is the exact manuscript weight `fourEndpointW`. It is a finite +normalization theorem, not an asymptotic estimate. + +## 1. Combined cardinality quotient + +For a full endpoint table `L`, the repository already proved separately + +```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. +``` + +`Section8EndpointDecoratedReferenceQuotient.lean` 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 combined denominator is proved +positive, then cast to `ENNReal` and divided only with explicit nonzero and +finite side conditions. + +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`. + +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 + +`Section8EndpointDecoratedReferenceWeight.lean` defines the common contribution +of one fully decorated endpoint block pairing: + +```text +full signed reward product / (n)_{J(L)}. +``` + +It proves that summing this constant atom over the whole decorated endpoint +family is exactly the combined quotient coefficient times that atom: + +```text +sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight. +``` + +## 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. +``` + +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. + +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. + +## 4. Relation to the Section VIII closure problem + +This closes the **decorated full-endpoint reference normalization**. It is the +reference measure against which the all-high deficit ratios are charged. + +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. 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} +}