From c201d2c3c5a0c483a3e134b228c4f58caff173f8 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 18:55:54 +0300
Subject: [PATCH 01/26] Add focused CI for the Section 8 physical-fibre closure

---
 ...dos625-section8-physical-fibre-closure.yml | 80 +++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 .github/workflows/erdos625-section8-physical-fibre-closure.yml

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
new file mode 100644
index 00000000..afe9e49e
--- /dev/null
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -0,0 +1,80 @@
+name: Erdős 625 Section 8 physical-fibre closure
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean"
+      - "625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean"
+      - "625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean"
+      - "625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean"
+      - "625/formalization/Erdos625/Section8BareSkeletonClosure.lean"
+      - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
+      - "625/formalization/SECTION8_PHYSICAL_FIBRE_CLOSURE_AUDIT.md"
+      - ".github/workflows/erdos625-section8-physical-fibre-closure.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-section8-physical-fibre-${{ 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 closure modules
+        shell: bash
+        run: |
+          files=(
+            625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean
+          )
+          for optional in \
+            625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean \
+            625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean \
+            625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean \
+            625/formalization/Erdos625/Section8BareSkeletonClosure.lean; do
+            if [[ -f "$optional" ]]; then files+=("$optional"); fi
+          done
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            "${files[@]}"; 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 current physical-fibre closure frontier warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          target=Erdos625.Section8EndpointPhysicalReverseData
+          if [[ -f Erdos625/Section8BareSkeletonClosure.lean ]]; then
+            target=Erdos625.Section8BareSkeletonClosure
+          elif [[ -f Erdos625/Section8AttainedAllDeficitReindexing.lean ]]; then
+            target=Erdos625.Section8AttainedAllDeficitReindexing
+          elif [[ -f Erdos625/Section8PartialCellPhysicalFibre.lean ]]; then
+            target=Erdos625.Section8PartialCellPhysicalFibre
+          elif [[ -f Erdos625/Section8EndpointPhysicalEquiv.lean ]]; then
+            target=Erdos625.Section8EndpointPhysicalEquiv
+          fi
+          set +e
+          lake build "$target" --wfail \
+            > /tmp/section8-physical-fibre-closure.log 2>&1
+          status=$?
+          tail -n 700 /tmp/section8-physical-fibre-closure.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-section8-physical-fibre-closure-log
+          path: /tmp/section8-physical-fibre-closure.log
+          if-no-files-found: ignore

From 5107924dc7827b582e2cc93c33679d9867b438e6 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:08:24 +0300
Subject: [PATCH 02/26] Validate the physical endpoint block-pairing
 reconstruction

---
 .../Section8EndpointPhysicalBlockReverse.lean | 265 ++++++++++++++++++
 1 file changed, 265 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
new file mode 100644
index 00000000..cabde31e
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
@@ -0,0 +1,265 @@
+import Erdos625.Section8EndpointDecoratedPhysicalInjective
+import Mathlib.Tactic
+
+/-!
+# Section VIII: reconstruct the endpoint block pairing from a physical fibre
+
+This module is the first independently checked half of the endpoint reverse
+map.  It pulls the literal full block pairs of a physical endpoint skeleton
+back through a fixed four-type slot indexing, proves that they form a typed
+block matching, and proves that their four-by-four type table is the prescribed
+endpoint table.
+
+No local stub matching is reconstructed here.  That dependent step is isolated
+in the next 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 hy' :
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1,
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2) ∈
+        fourEndpointFullPairs alpha hAlpha k S.1.1 := by
+      rw [hleftActual]
+      exact hy.2
+    have hrightActual :
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2 =
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2 :=
+      S.1.2.2.1 _ _ _ hx.2 hy'
+    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 hy' :
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1,
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2) ∈
+        fourEndpointFullPairs alpha hAlpha k S.1.1 := by
+      rw [hrightActual]
+      exact hy.2
+    have hleftActual :
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1 =
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1 :=
+      S.1.2.2.2 _ _ _ hx.2 hy'
+    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
+        · change fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.1 ∈
+            fourEndpointBlockSlots alpha hAlpha k i
+          simpa only [hei] using (slotIndex edge.1.1 edge.1.2).2
+        · change fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.2 ∈
+            fourEndpointBlockSlots alpha hAlpha k j
+          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 endpoint 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⟩
+
+#print axioms fourEndpointBlockSlots_type_unique
+#print axioms fourEndpointPhysicalBlockEdge_typeTable
+#print axioms fourEndpointPhysicalBlockSkeleton_typeTable
+
+end
+
+end Erdos625

From 73e25c322376e9664ea2fe889d1636cac38e2cb7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:09:06 +0300
Subject: [PATCH 03/26] Gate the validated block-reverse checkpoint
 independently

---
 .../workflows/erdos625-section8-physical-fibre-closure.yml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
index afe9e49e..490b01e3 100644
--- a/.github/workflows/erdos625-section8-physical-fibre-closure.yml
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -3,6 +3,7 @@ name: Erdős 625 Section 8 physical-fibre closure
 on:
   pull_request:
     paths:
+      - "625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean"
       - "625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean"
       - "625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean"
       - "625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean"
@@ -25,11 +26,11 @@ jobs:
     runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
-      - name: Reject placeholders and project axioms in closure modules
+      - name: Reject placeholders and project axioms in accepted closure modules
         shell: bash
         run: |
           files=(
-            625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean
+            625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
           )
           for optional in \
             625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean \
@@ -55,7 +56,7 @@ jobs:
         working-directory: 625/formalization
         shell: bash
         run: |
-          target=Erdos625.Section8EndpointPhysicalReverseData
+          target=Erdos625.Section8EndpointPhysicalBlockReverse
           if [[ -f Erdos625/Section8BareSkeletonClosure.lean ]]; then
             target=Erdos625.Section8BareSkeletonClosure
           elif [[ -f Erdos625/Section8AttainedAllDeficitReindexing.lean ]]; then

From 25799095236082b842e76d4ebf336db8ea662dc4 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:11:14 +0300
Subject: [PATCH 04/26] Add the exact partial-cell physical fibre and aggregate
 weight

---
 .../Section8PartialCellPhysicalFibre.lean     | 201 ++++++++++++++++++
 1 file changed, 201 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean

diff --git a/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean b/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
new file mode 100644
index 00000000..1dd33639
--- /dev/null
+++ b/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
@@ -0,0 +1,201 @@
+import Erdos625.Section8EndpointPhysicalBlockReverse
+import Mathlib.Tactic
+
+/-!
+# Section VIII: exact partial-cell physical fibres
+
+Fix one endpoint block pairing.  A deficit vector lowers the full multiplicity
+in each selected cell from `m_e` to `j_e = m_e - h_e`.  The literal local
+physical data are then independent `SingleCellStubMatching` fibres, one per
+selected block pair.
+
+This module proves their exact finite cardinality and attaches the common local
+signed reward and the single ambient falling-factorial normalization.  It is
+the aggregate local-fibre identity needed before any all-deficit comparison.
+It does not yet identify these data with the global attained canonical-demand
+family.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Full endpoint multiplicity in one selected block cell. -/
+def fourEndpointCellFullMultiplicity
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (e : ↥P.1.edges) : Nat :=
+  fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1
+
+/-- Actual multiplicity obtained by subtracting the selected deficit. -/
+def fourEndpointCellMultiplicityOfDeficit
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat)
+    (e : ↥P.1.edges) : Nat :=
+  fourEndpointCellFullMultiplicity alpha hAlpha P e - deficit e
+
+/-- The local partial physical matching in one selected block pair. -/
+abbrev FourEndpointSelectedCellPartialStubMatching
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat)
+    (e : ↥P.1.edges) :=
+  SingleCellStubMatching
+    (fourEndpointSize alpha hAlpha e.1.1.1)
+    (fourEndpointSize alpha hAlpha e.1.2.1)
+    (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e)
+
+/-- Product of the independent literal partial-stub-matching fibres. -/
+abbrev FourEndpointPartialStubDecoration
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) :=
+  ∀ e : ↥P.1.edges,
+    FourEndpointSelectedCellPartialStubMatching
+      alpha hAlpha P deficit e
+
+/-- Product of the local `j_e!` denominators. -/
+def fourEndpointPartialCellFactorialProduct
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+  ∏ e : ↥P.1.edges,
+    (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e).factorial
+
+/-- Product of the two descending-factorial stub selections in each cell. -/
+def fourEndpointPartialCellSelectionProduct
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+  ∏ e : ↥P.1.edges,
+    (fourEndpointSize alpha hAlpha e.1.1.1).descFactorial
+        (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e) *
+      (fourEndpointSize alpha hAlpha e.1.2.1).descFactorial
+        (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e)
+
+/-- Exact cross-multiplied cardinality of the local partial physical fibre. -/
+theorem card_fourEndpointPartialStubDecoration_mul_factorials
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    Fintype.card
+        (FourEndpointPartialStubDecoration alpha hAlpha P deficit) *
+      fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit =
+        fourEndpointPartialCellSelectionProduct alpha hAlpha P deficit := by
+  classical
+  rw [Fintype.card_pi]
+  unfold fourEndpointPartialCellFactorialProduct
+    fourEndpointPartialCellSelectionProduct
+  rw [← Finset.prod_mul_distrib]
+  apply Finset.prod_congr rfl
+  intro e he
+  exact card_singleCellStubMatching_mul_factorial
+    (fourEndpointSize alpha hAlpha e.1.1.1)
+    (fourEndpointSize alpha hAlpha e.1.2.1)
+    (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e)
+
+/-- The product of factorial denominators is positive. -/
+theorem fourEndpointPartialCellFactorialProduct_ne_zero
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit ≠ 0 := by
+  unfold fourEndpointPartialCellFactorialProduct
+  exact Finset.prod_ne_zero_iff.mpr fun _ _ => Nat.factorial_ne_zero _
+
+/-- Division form of the exact local partial-fibre cardinality in `ENNReal`. -/
+theorem ennreal_card_fourEndpointPartialStubDecoration_eq_quotient
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (Fintype.card
+      (FourEndpointPartialStubDecoration alpha hAlpha P deficit) : ENNReal) =
+      (fourEndpointPartialCellSelectionProduct alpha hAlpha P deficit : ENNReal) /
+        (fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit : ENNReal) := by
+  apply (ENNReal.eq_div_iff
+    (Nat.cast_ne_zero.mpr
+      (fourEndpointPartialCellFactorialProduct_ne_zero
+        alpha hAlpha P deficit))
+    (ENNReal.natCast_ne_top _)).2
+  simpa only [Nat.cast_mul, mul_comm] using
+    congrArg (fun x : Nat => (x : ENNReal))
+      (card_fourEndpointPartialStubDecoration_mul_factorials
+        alpha hAlpha P deficit)
+
+/-- Total exposed multiplicity of the selected partial cells. -/
+def fourEndpointPartialTotalMultiplicity
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+  ∑ e : ↥P.1.edges,
+    fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e
+
+/-- Product of the local signed rewards at the actual multiplicities. -/
+def fourEndpointPartialRewardProduct
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+  ∏ e : ↥P.1.edges,
+    (localSignRewardNat
+      (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e) : ENNReal)
+
+/-- Common contribution of one literal local partial-stub decoration. -/
+def fourEndpointPartialAtomWeight
+    (n alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+  fourEndpointPartialRewardProduct alpha hAlpha P deficit /
+    ((n.descFactorial
+      (fourEndpointPartialTotalMultiplicity alpha hAlpha P deficit) : Nat) :
+        ENNReal)
+
+/-- Aggregate weight after summing the entire local partial physical fibre. -/
+def fourEndpointPartialAggregateWeight
+    (n alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+  ((fourEndpointPartialCellSelectionProduct alpha hAlpha P deficit : Nat) :
+      ENNReal) /
+    ((fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit : Nat) :
+      ENNReal) *
+      fourEndpointPartialAtomWeight n alpha hAlpha P deficit
+
+/-- Summing the common atom over the literal local partial fibre gives the
+aggregate weight with exactly one local factorial denominator per cell. -/
+theorem sum_fourEndpointPartialAtomWeight_eq_aggregateWeight
+    (n alpha : Nat) (hAlpha : 5 < alpha)
+    {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
+    (P : FourEndpointBlockPairing alpha hAlpha k L)
+    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (∑ _ : FourEndpointPartialStubDecoration alpha hAlpha P deficit,
+      fourEndpointPartialAtomWeight n alpha hAlpha P deficit) =
+        fourEndpointPartialAggregateWeight n alpha hAlpha P deficit := by
+  rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
+  rw [ennreal_card_fourEndpointPartialStubDecoration_eq_quotient]
+  rfl
+
+#print axioms card_fourEndpointPartialStubDecoration_mul_factorials
+#print axioms ennreal_card_fourEndpointPartialStubDecoration_eq_quotient
+#print axioms sum_fourEndpointPartialAtomWeight_eq_aggregateWeight
+
+end
+
+end Erdos625

From 1864198afc24ba810f2785d10f01e73635f83986 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:21:39 +0300
Subject: [PATCH 05/26] Discharge the endpoint slot coercions explicitly

---
 .../Erdos625/Section8EndpointPhysicalBlockReverse.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
index cabde31e..1e4927f8 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
@@ -218,12 +218,10 @@ theorem fourEndpointPhysicalBlockSkeleton_typeTable
       constructor
       · apply Finset.mem_product.mpr
         constructor
-        · change fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.1 ∈
-            fourEndpointBlockSlots alpha hAlpha k i
-          simpa only [hei] using (slotIndex edge.1.1 edge.1.2).2
-        · change fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex edge.2 ∈
-            fourEndpointBlockSlots alpha hAlpha k j
-          simpa only [hej] using (slotIndex edge.2.1 edge.2.2).2
+        · simpa only [fourEndpointActualBlockOfAtom, hei] using
+            (slotIndex edge.1.1 edge.1.2).2
+        · simpa only [fourEndpointActualBlockOfAtom, 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

From bcbf1effdefa9e2e4c038324456bfafb384d4758 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:31:59 +0300
Subject: [PATCH 06/26] Unfold the local block-pair abbreviation in the reverse
 map

---
 .../Erdos625/Section8EndpointPhysicalBlockReverse.lean        | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
index 1e4927f8..455d9abc 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
@@ -218,9 +218,9 @@ theorem fourEndpointPhysicalBlockSkeleton_typeTable
       constructor
       · apply Finset.mem_product.mpr
         constructor
-        · simpa only [fourEndpointActualBlockOfAtom, hei] using
+        · simpa only [F, fourEndpointActualBlockOfAtom, hei] using
             (slotIndex edge.1.1 edge.1.2).2
-        · simpa only [fourEndpointActualBlockOfAtom, hej] using
+        · simpa only [F, fourEndpointActualBlockOfAtom, hej] using
             (slotIndex edge.2.1 edge.2.2).2
       · simpa only [hei, hej] using
           fourEndpointPhysicalBlockEdge_typeTable

From 320b3f335923f1400a118f4aa8ff0463e765cbf9 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:34:28 +0300
Subject: [PATCH 07/26] Reconstruct local endpoint stub matchings from a
 physical fibre

---
 .../Section8EndpointPhysicalCellReverse.lean  | 285 ++++++++++++++++++
 1 file changed, 285 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
new file mode 100644
index 00000000..7be7f1aa
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
@@ -0,0 +1,285 @@
+import Erdos625.Section8EndpointPhysicalBlockReverse
+import Mathlib.Tactic
+
+/-!
+# Section VIII: reconstruct local endpoint stub matchings
+
+After the block-level endpoint pairing has been reconstructed, every selected
+physical block cell can be pulled back to a unit-typed local stub matching.  We
+use explicit finite equivalences for the dependent stub bounds, so no numerical
+information is hidden in `Fin.cast` projections.
+
+This module constructs the local reverse data and proves its exact cell
+multiplicity.  The global round trips are isolated in the subsequent endpoint
+equivalence module.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- The finite equivalence from a physical stub index in one endpoint block to
+its canonical local endpoint coordinate. -/
+noncomputable def fourEndpointPhysicalStubToLocalEquiv
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (a : FourEndpointBlockAtom alpha hAlpha k) :
+    Fin (profileBlockMargin k
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) ≃
+      Fin (fourEndpointSize alpha hAlpha a.1) :=
+  Equiv.cast (congrArg Fin
+    (profileBlockMargin_fourEndpointActualBlockOfAtom
+      alpha hAlpha k slotIndex a))
+
+/-- Pull one physical cell edge back to the corresponding unit-typed local
+stub edge. -/
+noncomputable def fourEndpointPhysicalCellEdgeToLocal
+    (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) :
+    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) :=
+  fun p =>
+    (⟨(), fourEndpointPhysicalStubToLocalEquiv
+      alpha hAlpha k slotIndex e.1.1 p.1⟩,
+     ⟨(), fourEndpointPhysicalStubToLocalEquiv
+      alpha hAlpha k slotIndex e.1.2 p.2⟩)
+
+/-- The local pullback map is injective because both coordinate maps are
+finite equivalences. -/
+theorem fourEndpointPhysicalCellEdgeToLocal_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
+      (fourEndpointPhysicalCellEdgeToLocal
+        alpha hAlpha k L slotIndex S e) := by
+  intro p q hpq
+  apply Prod.ext
+  · apply (fourEndpointPhysicalStubToLocalEquiv
+      alpha hAlpha k slotIndex e.1.1).injective
+    exact eq_of_heq (Sigma.mk.inj_iff.mp
+      (congrArg Prod.fst hpq)).2
+  · apply (fourEndpointPhysicalStubToLocalEquiv
+      alpha hAlpha k slotIndex e.1.2).injective
+    exact eq_of_heq (Sigma.mk.inj_iff.mp
+      (congrArg Prod.snd hpq)).2
+
+/-- Local physical cell edges in canonical unit-typed coordinates. -/
+noncomputable def fourEndpointPhysicalCellLocalEdgesValidated
+    (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
+    (fourEndpointPhysicalCellEdgeToLocal
+      alpha hAlpha k L slotIndex S e)
+
+/-- Public cell-cardinality identity for a physical typed matching. -/
+theorem physicalCellEdges_card_eq_typeTable_public
+    {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 edge hedge
+    rw [Finset.mem_filter] at hedge
+    obtain ⟨hEdge, hI, hJ⟩ := hedge
+    obtain ⟨⟨i', r⟩, ⟨j', c⟩⟩ := edge
+    simp only at hI hJ
+    subst i'
+    subst j'
+    exact ⟨(r, c), by simp [hEdge], rfl⟩
+
+/-- Pulled-back local physical cell matching. -/
+noncomputable def fourEndpointPhysicalCellLocalSkeletonValidated
+    (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 := fourEndpointPhysicalCellLocalEdgesValidated
+    alpha hAlpha k L slotIndex S e
+  leftUnique := by
+    classical
+    intro x hx y hy hleft
+    rw [fourEndpointPhysicalCellLocalEdgesValidated, Finset.mem_image] at hx hy
+    obtain ⟨p, hp, rfl⟩ := hx
+    obtain ⟨q, hq, rfl⟩ := hy
+    have hLocalFirst :
+        fourEndpointPhysicalStubToLocalEquiv
+            alpha hAlpha k slotIndex e.1.1 p.1 =
+          fourEndpointPhysicalStubToLocalEquiv
+            alpha hAlpha k slotIndex e.1.1 q.1 :=
+      eq_of_heq (Sigma.mk.inj_iff.mp hleft).2
+    have hpFirst : p.1 = q.1 :=
+      (fourEndpointPhysicalStubToLocalEquiv
+        alpha hAlpha k slotIndex e.1.1).injective hLocalFirst
+    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
+    exact congrArg
+      (fourEndpointPhysicalCellEdgeToLocal
+        alpha hAlpha k L slotIndex S e)
+      (Prod.ext hpFirst hpSecond)
+  rightUnique := by
+    classical
+    intro x hx y hy hright
+    rw [fourEndpointPhysicalCellLocalEdgesValidated, Finset.mem_image] at hx hy
+    obtain ⟨p, hp, rfl⟩ := hx
+    obtain ⟨q, hq, rfl⟩ := hy
+    have hLocalSecond :
+        fourEndpointPhysicalStubToLocalEquiv
+            alpha hAlpha k slotIndex e.1.2 p.2 =
+          fourEndpointPhysicalStubToLocalEquiv
+            alpha hAlpha k slotIndex e.1.2 q.2 :=
+      eq_of_heq (Sigma.mk.inj_iff.mp hright).2
+    have hpSecond : p.2 = q.2 :=
+      (fourEndpointPhysicalStubToLocalEquiv
+        alpha hAlpha k slotIndex e.1.2).injective hLocalSecond
+    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
+    exact congrArg
+      (fourEndpointPhysicalCellEdgeToLocal
+        alpha hAlpha k L slotIndex S e)
+      (Prod.ext hpFirst hpSecond)
+
+/-- The pulled-back local skeleton has exactly the full endpoint multiplicity
+of its selected block cell. -/
+theorem fourEndpointPhysicalCellLocalSkeletonValidated_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) :
+    (fourEndpointPhysicalCellLocalSkeletonValidated
+      alpha hAlpha k L slotIndex S e).typeTable () () =
+        fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1 := by
+  change
+    ((fourEndpointPhysicalCellLocalEdgesValidated
+      alpha hAlpha k L slotIndex S e).filter
+        (fun z => z.1.1 = () ∧ z.2.1 = ())).card =
+      fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1
+  have hAll :
+      (fourEndpointPhysicalCellLocalEdgesValidated
+        alpha hAlpha k L slotIndex S e).filter
+          (fun z => z.1.1 = () ∧ z.2.1 = ()) =
+        fourEndpointPhysicalCellLocalEdgesValidated
+          alpha hAlpha k L slotIndex S e := by
+    ext z
+    simp
+  rw [hAll]
+  rw [fourEndpointPhysicalCellLocalEdgesValidated,
+    Finset.card_image_of_injective]
+  · rw [physicalCellEdges_card_eq_typeTable_public]
+    exact fourEndpointPhysicalBlockEdge_typeTable
+      alpha hAlpha k L slotIndex S e.1 e.2
+  · exact fourEndpointPhysicalCellEdgeToLocal_injective
+      alpha hAlpha k L slotIndex S e
+
+/-- One reconstructed literal full-cell matching. -/
+noncomputable def fourEndpointPhysicalCellStubMatchingValidated
+    (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 :=
+  ⟨fourEndpointPhysicalCellLocalSkeletonValidated
+      alpha hAlpha k L slotIndex S e,
+    fourEndpointPhysicalCellLocalSkeletonValidated_typeTable
+      alpha hAlpha k L slotIndex S e⟩
+
+/-- Reverse decorated data reconstructed from one physical endpoint fibre
+member. -/
+noncomputable def fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+    (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 => fourEndpointPhysicalCellStubMatchingValidated
+      alpha hAlpha k L slotIndex S e⟩
+
+#print axioms fourEndpointPhysicalCellEdgeToLocal_injective
+#print axioms physicalCellEdges_card_eq_typeTable_public
+#print axioms fourEndpointPhysicalCellLocalSkeletonValidated_typeTable
+
+end
+
+end Erdos625

From d67206fd1ccdf38d487d51948365946af6fd6605 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:35:44 +0300
Subject: [PATCH 08/26] Build every accepted Section 8 closure checkpoint

---
 ...dos625-section8-physical-fibre-closure.yml | 50 ++++++++++++-------
 1 file changed, 31 insertions(+), 19 deletions(-)

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
index 490b01e3..becfdd84 100644
--- a/.github/workflows/erdos625-section8-physical-fibre-closure.yml
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -4,7 +4,7 @@ on:
   pull_request:
     paths:
       - "625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean"
-      - "625/formalization/Erdos625/Section8EndpointPhysicalReverseData.lean"
+      - "625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean"
       - "625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean"
       - "625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean"
       - "625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean"
@@ -31,10 +31,11 @@ jobs:
         run: |
           files=(
             625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
+            625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
+            625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
           )
           for optional in \
             625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean \
-            625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean \
             625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean \
             625/formalization/Erdos625/Section8BareSkeletonClosure.lean; do
             if [[ -f "$optional" ]]; then files+=("$optional"); fi
@@ -52,26 +53,37 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build the current physical-fibre closure frontier warning-fatally
+      - name: Build every accepted closure checkpoint warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
-          target=Erdos625.Section8EndpointPhysicalBlockReverse
-          if [[ -f Erdos625/Section8BareSkeletonClosure.lean ]]; then
-            target=Erdos625.Section8BareSkeletonClosure
-          elif [[ -f Erdos625/Section8AttainedAllDeficitReindexing.lean ]]; then
-            target=Erdos625.Section8AttainedAllDeficitReindexing
-          elif [[ -f Erdos625/Section8PartialCellPhysicalFibre.lean ]]; then
-            target=Erdos625.Section8PartialCellPhysicalFibre
-          elif [[ -f Erdos625/Section8EndpointPhysicalEquiv.lean ]]; then
-            target=Erdos625.Section8EndpointPhysicalEquiv
-          fi
-          set +e
-          lake build "$target" --wfail \
-            > /tmp/section8-physical-fibre-closure.log 2>&1
-          status=$?
-          tail -n 700 /tmp/section8-physical-fibre-closure.log
-          exit $status
+          targets=(
+            Erdos625.Section8EndpointPhysicalBlockReverse
+            Erdos625.Section8EndpointPhysicalCellReverse
+            Erdos625.Section8PartialCellPhysicalFibre
+          )
+          for optional in \
+            Erdos625.Section8EndpointPhysicalEquiv \
+            Erdos625.Section8AttainedAllDeficitReindexing \
+            Erdos625.Section8BareSkeletonClosure; do
+            path="${optional//./\/}.lean"
+            path="${path#Erdos625\/}"
+            if [[ -f "Erdos625/$path" ]]; then targets+=("$optional"); fi
+          done
+          : > /tmp/section8-physical-fibre-closure.log
+          for target in "${targets[@]}"; do
+            echo "=== $target ===" | tee -a /tmp/section8-physical-fibre-closure.log
+            set +e
+            lake build "$target" --wfail \
+              >> /tmp/section8-physical-fibre-closure.log 2>&1
+            status=$?
+            set -e
+            if [[ $status -ne 0 ]]; then
+              tail -n 900 /tmp/section8-physical-fibre-closure.log
+              exit $status
+            fi
+          done
+          tail -n 900 /tmp/section8-physical-fibre-closure.log
       - name: Upload focused compiler log
         if: always()
         uses: actions/upload-artifact@v4

From c365b524373bbfe7af83cc16238959f2e802741e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:40:28 +0300
Subject: [PATCH 09/26] Add exact regression checks for the physical-fibre
 closure

---
 ...tion8_physical_fibre_closure_regression.py | 217 ++++++++++++++++++
 1 file changed, 217 insertions(+)
 create mode 100644 625/experiments/section8_physical_fibre_closure_regression.py

diff --git a/625/experiments/section8_physical_fibre_closure_regression.py b/625/experiments/section8_physical_fibre_closure_regression.py
new file mode 100644
index 00000000..9e227307
--- /dev/null
+++ b/625/experiments/section8_physical_fibre_closure_regression.py
@@ -0,0 +1,217 @@
+#!/usr/bin/env python3
+"""Exact finite regression for the Section VIII physical-fibre closure.
+
+The script checks the arithmetic identities used after the finite reindexing:
+local partial-matching cardinalities, aggregate deficit ratios, the single
+global falling-factorial loss, and the all-high geometric budget.  It does not
+prove the Lean equivalence or the random-graph asymptotics.
+"""
+
+from __future__ import annotations
+
+from fractions import Fraction
+from itertools import product
+from math import comb, factorial
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def falling(n: int, k: int) -> int:
+    require(0 <= k <= n, f"invalid falling factorial ({n})_{k}")
+    value = 1
+    for offset in range(k):
+        value *= n - offset
+    return value
+
+
+def local_reward(j: int) -> int:
+    if j <= 2:
+        return 1
+    return 2 ** (comb(j, 2) - 1)
+
+
+def local_matching_count(u: int, v: int, j: int) -> int:
+    """Number of unlabelled size-j partial matchings in one u-by-v cell."""
+
+    return comb(u, j) * comb(v, j) * factorial(j)
+
+
+def local_aggregate_weight(u: int, v: int, j: int) -> Fraction:
+    return Fraction(falling(u, j) * falling(v, j), factorial(j)) * local_reward(j)
+
+
+def deficit_ratio_formula(m: int, d: int, h: int) -> Fraction:
+    denominator = 1
+    for t in range(1, h + 1):
+        denominator *= d + t
+    exponent = h * m - h * (h + 1) // 2
+    return Fraction(comb(m, h), denominator * 2**exponent)
+
+
+def check_single_cell_cardinality(max_u: int = 40) -> int:
+    checked = 0
+    for u in range(max_u + 1):
+        for v in range(max_u + 1):
+            for j in range(min(u, v) + 1):
+                count = local_matching_count(u, v, j)
+                require(
+                    count * factorial(j) == falling(u, j) * falling(v, j),
+                    f"single-cell cardinality failed: u={u}, v={v}, j={j}",
+                )
+                checked += 1
+    return checked
+
+
+def check_product_fibre_cardinality() -> int:
+    """Check products of independent selected-cell fibres."""
+
+    cells = [(5, 7, 4), (6, 6, 5), (8, 9, 6), (7, 10, 3)]
+    checked = 0
+    for length in range(5):
+        for chosen in product(cells, repeat=length):
+            card = 1
+            factorial_product = 1
+            selection_product = 1
+            for u, v, j in chosen:
+                card *= local_matching_count(u, v, j)
+                factorial_product *= factorial(j)
+                selection_product *= falling(u, j) * falling(v, j)
+            require(
+                card * factorial_product == selection_product,
+                f"product fibre identity failed: {chosen}",
+            )
+            checked += 1
+    return checked
+
+
+def check_exact_local_deficit_ratio(max_m: int = 100) -> int:
+    checked = 0
+    for m in range(5, max_m + 1):
+        for d in range(4):
+            for h in range(m):
+                if 2 * h >= m:
+                    continue
+                j = m - h
+                require(j >= 3, "high multiplicity left the signed-reward range")
+                actual = local_aggregate_weight(m, m + d, j) / local_aggregate_weight(
+                    m, m + d, m
+                )
+                expected = deficit_ratio_formula(m, d, h)
+                require(
+                    actual == expected,
+                    f"local deficit ratio failed: m={m}, d={d}, h={h}",
+                )
+                checked += 1
+    return checked
+
+
+def check_global_denominator(max_n: int = 150) -> int:
+    checked = 0
+    for n in range(max_n + 1):
+        for j in range(n + 1):
+            for h in range(n - j + 1):
+                ratio = Fraction(falling(n, j + h), falling(n, j))
+                require(
+                    ratio == falling(n - j, h),
+                    f"global denominator identity failed: n={n}, J={j}, H={h}",
+                )
+                require(
+                    ratio <= n**h,
+                    f"global denominator bound failed: n={n}, J={j}, H={h}",
+                )
+                checked += 1
+    return checked
+
+
+def check_multi_cell_aggregate_comparison() -> int:
+    """Exhaust small matching supports and verify the charged product bound."""
+
+    options = [
+        (m, d, h)
+        for m in range(5, 11)
+        for d in range(4)
+        for h in range(m)
+        if 2 * h < m
+    ]
+    checked = 0
+    for cell_count in range(1, 4):
+        for cells in product(options, repeat=cell_count):
+            full_total = sum(m for m, _d, _h in cells)
+            actual_total = sum(m - h for m, _d, h in cells)
+            total_deficit = full_total - actual_total
+            n = full_total + 7
+
+            local_ratio = Fraction(1, 1)
+            charged_product = Fraction(1, 1)
+            for m, d, h in cells:
+                ratio = deficit_ratio_formula(m, d, h)
+                local_ratio *= ratio
+                charged_product *= n**h * ratio
+
+            denominator_ratio = Fraction(
+                falling(n, full_total), falling(n, actual_total)
+            )
+            exact_global_ratio = denominator_ratio * local_ratio
+            require(
+                denominator_ratio == falling(n - actual_total, total_deficit),
+                f"multi-cell denominator factorization failed: {cells}",
+            )
+            require(
+                exact_global_ratio <= charged_product,
+                f"multi-cell charged comparison failed: {cells}",
+            )
+            checked += 1
+    return checked
+
+
+def check_two_thirds_budget(max_m: int = 2000) -> int:
+    checked = 0
+    for m in range(1, max_m + 1):
+        for h in range(1, m + 1):
+            if 2 * h >= m:
+                continue
+            lhs = h * ((2 * m) // 3)
+            rhs = h * m - h * (h + 1) // 2
+            require(lhs <= rhs, f"two-thirds budget failed: m={m}, h={h}")
+            checked += 1
+    return checked
+
+
+def check_geometric_fibre() -> int:
+    checked = 0
+    for denominator in range(2, 101):
+        for numerator in range(1, denominator // 2 + 1):
+            rho = Fraction(numerator, denominator)
+            for cutoff in range(1, 80):
+                finite_sum = sum((rho**h for h in range(1, cutoff + 1)), Fraction())
+                require(finite_sum <= rho / (1 - rho), "geometric majorant failed")
+                require(finite_sum <= 2 * rho, "two-rho majorant failed")
+                checked += 1
+    return checked
+
+
+def main() -> None:
+    single = check_single_cell_cardinality()
+    products = check_product_fibre_cardinality()
+    local_ratios = check_exact_local_deficit_ratio()
+    denominators = check_global_denominator()
+    aggregate = check_multi_cell_aggregate_comparison()
+    budgets = check_two_thirds_budget()
+    geometric = check_geometric_fibre()
+
+    print("ERDOS 625 SECTION 8 PHYSICAL-FIBRE CLOSURE REGRESSION: PASS")
+    print(f"  single-cell cardinalities: {single}")
+    print(f"  product-fibre cardinalities: {products}")
+    print(f"  exact local deficit ratios: {local_ratios}")
+    print(f"  global denominator cases: {denominators}")
+    print(f"  multi-cell aggregate comparisons: {aggregate}")
+    print(f"  two-thirds exponent cases: {budgets}")
+    print(f"  geometric-fibre cases: {geometric}")
+    print("  scope: exact finite arithmetic; the Lean global reindexing remains separate")
+
+
+if __name__ == "__main__":
+    main()

From f57cad155e89ced339faa02aca3f63043a44faab Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:41:52 +0300
Subject: [PATCH 10/26] Run exact closure regression beside the Lean
 checkpoints

---
 .../erdos625-section8-physical-fibre-closure.yml     | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
index becfdd84..ddee0c70 100644
--- a/.github/workflows/erdos625-section8-physical-fibre-closure.yml
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -11,6 +11,7 @@ on:
       - "625/formalization/Erdos625/Section8BareSkeletonClosure.lean"
       - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
       - "625/formalization/SECTION8_PHYSICAL_FIBRE_CLOSURE_AUDIT.md"
+      - "625/experiments/section8_physical_fibre_closure_regression.py"
       - ".github/workflows/erdos625-section8-physical-fibre-closure.yml"
   workflow_dispatch:
 
@@ -22,6 +23,17 @@ permissions:
   contents: read
 
 jobs:
+  exact-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile the exact closure regression
+        run: python -m py_compile 625/experiments/section8_physical_fibre_closure_regression.py
+      - name: Run the exact closure regression
+        run: python 625/experiments/section8_physical_fibre_closure_regression.py
+      - name: Run with Python optimization enabled
+        run: python -O 625/experiments/section8_physical_fibre_closure_regression.py
+
   focused-lean-check:
     runs-on: ubuntu-24.04
     steps:

From 33410747ddd87dfffcddbff804e4741236c8b00d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:49:44 +0300
Subject: [PATCH 11/26] Make the independent deficit-function binders anonymous

---
 .../Section8PartialCellPhysicalFibre.lean     | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean b/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
index 1dd33639..320d0db8 100644
--- a/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
+++ b/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
@@ -37,7 +37,7 @@ def fourEndpointCellMultiplicityOfDeficit
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat)
+    (deficit : ∀ _e : ↥P.1.edges, Nat)
     (e : ↥P.1.edges) : Nat :=
   fourEndpointCellFullMultiplicity alpha hAlpha P e - deficit e
 
@@ -46,7 +46,7 @@ abbrev FourEndpointSelectedCellPartialStubMatching
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat)
+    (deficit : ∀ _e : ↥P.1.edges, Nat)
     (e : ↥P.1.edges) :=
   SingleCellStubMatching
     (fourEndpointSize alpha hAlpha e.1.1.1)
@@ -58,7 +58,7 @@ abbrev FourEndpointPartialStubDecoration
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) :=
   ∀ e : ↥P.1.edges,
     FourEndpointSelectedCellPartialStubMatching
       alpha hAlpha P deficit e
@@ -68,7 +68,7 @@ def fourEndpointPartialCellFactorialProduct
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : Nat :=
   ∏ e : ↥P.1.edges,
     (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e).factorial
 
@@ -77,7 +77,7 @@ def fourEndpointPartialCellSelectionProduct
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : Nat :=
   ∏ e : ↥P.1.edges,
     (fourEndpointSize alpha hAlpha e.1.1.1).descFactorial
         (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e) *
@@ -89,7 +89,7 @@ theorem card_fourEndpointPartialStubDecoration_mul_factorials
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (deficit : ∀ _e : ↥P.1.edges, Nat) :
     Fintype.card
         (FourEndpointPartialStubDecoration alpha hAlpha P deficit) *
       fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit =
@@ -100,7 +100,7 @@ theorem card_fourEndpointPartialStubDecoration_mul_factorials
     fourEndpointPartialCellSelectionProduct
   rw [← Finset.prod_mul_distrib]
   apply Finset.prod_congr rfl
-  intro e he
+  intro e _he
   exact card_singleCellStubMatching_mul_factorial
     (fourEndpointSize alpha hAlpha e.1.1.1)
     (fourEndpointSize alpha hAlpha e.1.2.1)
@@ -111,7 +111,7 @@ theorem fourEndpointPartialCellFactorialProduct_ne_zero
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (deficit : ∀ _e : ↥P.1.edges, Nat) :
     fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit ≠ 0 := by
   unfold fourEndpointPartialCellFactorialProduct
   exact Finset.prod_ne_zero_iff.mpr fun _ _ => Nat.factorial_ne_zero _
@@ -121,7 +121,7 @@ theorem ennreal_card_fourEndpointPartialStubDecoration_eq_quotient
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (deficit : ∀ _e : ↥P.1.edges, Nat) :
     (Fintype.card
       (FourEndpointPartialStubDecoration alpha hAlpha P deficit) : ENNReal) =
       (fourEndpointPartialCellSelectionProduct alpha hAlpha P deficit : ENNReal) /
@@ -141,7 +141,7 @@ def fourEndpointPartialTotalMultiplicity
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : Nat :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : Nat :=
   ∑ e : ↥P.1.edges,
     fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e
 
@@ -150,7 +150,7 @@ def fourEndpointPartialRewardProduct
     (alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : ENNReal :=
   ∏ e : ↥P.1.edges,
     (localSignRewardNat
       (fourEndpointCellMultiplicityOfDeficit alpha hAlpha P deficit e) : ENNReal)
@@ -160,7 +160,7 @@ def fourEndpointPartialAtomWeight
     (n alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : ENNReal :=
   fourEndpointPartialRewardProduct alpha hAlpha P deficit /
     ((n.descFactorial
       (fourEndpointPartialTotalMultiplicity alpha hAlpha P deficit) : Nat) :
@@ -171,7 +171,7 @@ def fourEndpointPartialAggregateWeight
     (n alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) : ENNReal :=
+    (deficit : ∀ _e : ↥P.1.edges, Nat) : ENNReal :=
   ((fourEndpointPartialCellSelectionProduct alpha hAlpha P deficit : Nat) :
       ENNReal) /
     ((fourEndpointPartialCellFactorialProduct alpha hAlpha P deficit : Nat) :
@@ -184,7 +184,7 @@ theorem sum_fourEndpointPartialAtomWeight_eq_aggregateWeight
     (n alpha : Nat) (hAlpha : 5 < alpha)
     {k : ColoringProfile (alpha + 1)} {L : FourEndpointFullTable}
     (P : FourEndpointBlockPairing alpha hAlpha k L)
-    (deficit : ∀ e : ↥P.1.edges, Nat) :
+    (deficit : ∀ _e : ↥P.1.edges, Nat) :
     (∑ _ : FourEndpointPartialStubDecoration alpha hAlpha P deficit,
       fourEndpointPartialAtomWeight n alpha hAlpha P deficit) =
         fourEndpointPartialAggregateWeight n alpha hAlpha P deficit := by

From bcfa19fa2409216bcb83487ad220994cf7b3fc44 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 19:54:03 +0300
Subject: [PATCH 12/26] Prove the endpoint decorated/physical equivalence

---
 .../Section8EndpointPhysicalEquiv.lean        | 204 ++++++++++++++++++
 1 file changed, 204 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
new file mode 100644
index 00000000..810503ad
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -0,0 +1,204 @@
+import Erdos625.Section8EndpointPhysicalCellReverse
+import Mathlib.Tactic
+
+/-!
+# Section VIII: endpoint decorated/physical equivalence
+
+The forward map unions the physical edges supplied by the local full-cell
+stub matchings.  The reverse map recovers the selected block pairs and pulls
+each physical cell back to its canonical local coordinates.
+
+This module proves both round trips.  It closes the endpoint-only physical
+fibre equivalence, but makes no claim about nonendpoint deficits or the global
+canonical high-skeleton sum.
+-/
+
+namespace Erdos625
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Pulling a physical cell edge to local coordinates and mapping it forward
+again preserves the literal physical edge. -/
+theorem fourEndpointPhysicalEdge_local_roundtrip
+    (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))) :
+    fourEndpointPhysicalEdgeOfLocalEdge alpha hAlpha k L slotIndex
+        (fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+          alpha hAlpha k L slotIndex S)
+        e
+        (fourEndpointPhysicalCellEdgeToLocal
+          alpha hAlpha k L slotIndex S e p) =
+      ((⟨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)) := by
+  apply Prod.ext
+  · apply Sigma.ext rfl
+    apply heq_of_eq
+    apply Fin.ext
+    rfl
+  · apply Sigma.ext rfl
+    apply heq_of_eq
+    apply Fin.ext
+    rfl
+
+/-- The physical skeleton underlying forward-after-reverse is the original
+physical skeleton. -/
+theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (L : FourEndpointFullTable)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (S : FourEndpointPhysicalFibre alpha hAlpha k L) :
+    fourEndpointDecoratedPhysicalSkeleton alpha hAlpha k L slotIndex
+        (fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+          alpha hAlpha k L slotIndex S) =
+      S.1.1 := by
+  apply UnlabelledTypedSkeleton.ext
+  ext z
+  constructor
+  · intro hz
+    simp only [fourEndpointDecoratedPhysicalSkeleton,
+      fourEndpointDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and, Finset.mem_image] at hz
+    obtain ⟨e, p, hp, rfl⟩ := hz
+    change p ∈ fourEndpointPhysicalCellLocalEdgesValidated
+      alpha hAlpha k L slotIndex S e at hp
+    rw [fourEndpointPhysicalCellLocalEdgesValidated, Finset.mem_image] at hp
+    obtain ⟨q, hq, rfl⟩ := hp
+    rw [fourEndpointPhysicalEdge_local_roundtrip]
+    simpa [UnlabelledTypedSkeleton.cellEdges] using hq
+  · intro hz
+    obtain ⟨i, j, hi, hj, htable⟩ := S.1.2.1 z hz
+    let ai := (slotIndex i).symm ⟨z.1.1, hi⟩
+    let bj := (slotIndex j).symm ⟨z.2.1, hj⟩
+    let a : FourEndpointBlockAtom alpha hAlpha k := ⟨i, ai⟩
+    let b : FourEndpointBlockAtom alpha hAlpha k := ⟨j, bj⟩
+    let edge : FourEndpointBlockAtom alpha hAlpha k ×
+        FourEndpointBlockAtom alpha hAlpha k := (a, b)
+    have ha :
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a = z.1.1 := by
+      exact congrArg Subtype.val ((slotIndex i).apply_symm_apply ⟨z.1.1, hi⟩)
+    have hb :
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b = z.2.1 := by
+      exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨z.2.1, hj⟩)
+    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 [ha] using hi
+        · simpa only [hb] using hj
+        · simpa only [ha, hb] using htable
+    let e : ↥(fourEndpointPhysicalBlockPairing
+        alpha hAlpha k L slotIndex S).1.edges := ⟨edge, hedge⟩
+    let qa : Fin (profileBlockMargin k
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) :=
+      Fin.cast (congrArg (profileBlockMargin k) ha).symm z.1.2
+    let qb : Fin (profileBlockMargin k
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
+      Fin.cast (congrArg (profileBlockMargin k) hb).symm z.2.2
+    let q := (qa, qb)
+    have hglobal :
+        ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,
+          ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩) :
+          RowStub (profileBlockMargin k) ×
+            ColumnStub (profileBlockMargin k)) = z := by
+      apply Prod.ext
+      · apply Sigma.ext ha
+        apply heq_of_eq
+        apply Fin.ext
+        rfl
+      · apply Sigma.ext hb
+        apply heq_of_eq
+        apply Fin.ext
+        rfl
+    have hq : q ∈ S.1.1.cellEdges
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) := by
+      rw [UnlabelledTypedSkeleton.cellEdges, Finset.mem_filter]
+      exact ⟨Finset.mem_univ q, by simpa only [hglobal] using hz⟩
+    let p := fourEndpointPhysicalCellEdgeToLocal
+      alpha hAlpha k L slotIndex S e q
+    have hp : p ∈ fourEndpointPhysicalCellLocalEdgesValidated
+        alpha hAlpha k L slotIndex S e := by
+      rw [fourEndpointPhysicalCellLocalEdgesValidated, Finset.mem_image]
+      exact ⟨q, hq, rfl⟩
+    simp only [fourEndpointDecoratedPhysicalSkeleton,
+      fourEndpointDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and]
+    refine ⟨e, Finset.mem_image.mpr ⟨p, hp, ?_⟩⟩
+    rw [fourEndpointPhysicalEdge_local_roundtrip]
+    exact hglobal
+
+/-- Forward after reverse is the identity on the endpoint physical fibre. -/
+theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (L : FourEndpointFullTable)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) :
+    Function.RightInverse
+      (fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+        alpha hAlpha k L slotIndex)
+      (fourEndpointDecoratedBlockPairingToPhysicalFibre
+        alpha hAlpha k L slotIndex) := by
+  intro S
+  apply Subtype.ext
+  apply Subtype.ext
+  exact fourEndpointDecoratedPhysicalSkeleton_reverse_eq
+    alpha hAlpha k L slotIndex S
+
+/-- Reverse after forward is the identity on decorated endpoint block
+pairings. -/
+theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_leftInverse
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (L : FourEndpointFullTable)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) :
+    Function.LeftInverse
+      (fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+        alpha hAlpha k L slotIndex)
+      (fourEndpointDecoratedBlockPairingToPhysicalFibre
+        alpha hAlpha k L slotIndex) := by
+  intro D
+  apply fourEndpointDecoratedBlockPairingToPhysicalFibre_injective
+    alpha hAlpha k L slotIndex
+  exact fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse
+    alpha hAlpha k L slotIndex
+    (fourEndpointDecoratedBlockPairingToPhysicalFibre
+      alpha hAlpha k L slotIndex D)
+
+/-- Exact finite equivalence between decorated full endpoint data and the
+literal physical endpoint fibre. -/
+noncomputable def fourEndpointDecoratedPhysicalEquiv
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (L : FourEndpointFullTable)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) :
+    FourEndpointDecoratedBlockPairing alpha hAlpha k L ≃
+      FourEndpointPhysicalFibre alpha hAlpha k L where
+  toFun := fourEndpointDecoratedBlockPairingToPhysicalFibre
+    alpha hAlpha k L slotIndex
+  invFun := fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
+    alpha hAlpha k L slotIndex
+  left_inv := fourEndpointDecoratedBlockPairingToPhysicalFibre_leftInverse
+    alpha hAlpha k L slotIndex
+  right_inv := fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse
+    alpha hAlpha k L slotIndex
+
+#print axioms fourEndpointPhysicalEdge_local_roundtrip
+#print axioms fourEndpointDecoratedPhysicalSkeleton_reverse_eq
+#print axioms fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse
+#print axioms fourEndpointDecoratedBlockPairingToPhysicalFibre_leftInverse
+
+end
+
+end Erdos625

From 0e3bd117fd05794d1ec31a88cdb3a60bb1156e0e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 20:03:03 +0300
Subject: [PATCH 13/26] Resolve the endpoint round trips by block substitution

---
 .../Section8EndpointPhysicalEquiv.lean        | 64 ++++++++-----------
 1 file changed, 26 insertions(+), 38 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index 810503ad..b59ee847 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -42,6 +42,9 @@ theorem fourEndpointPhysicalEdge_local_roundtrip
         ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, p.2⟩) :
         RowStub (profileBlockMargin k) ×
           ColumnStub (profileBlockMargin k)) := by
+  simp only [fourEndpointPhysicalEdgeOfLocalEdge,
+    fourEndpointPhysicalCellEdgeToLocal,
+    fourEndpointPhysicalStubToLocalEquiv, Equiv.cast_apply]
   apply Prod.ext
   · apply Sigma.ext rfl
     apply heq_of_eq
@@ -63,6 +66,7 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
         (fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
           alpha hAlpha k L slotIndex S) =
       S.1.1 := by
+  classical
   apply UnlabelledTypedSkeleton.ext
   ext z
   constructor
@@ -77,58 +81,42 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
     obtain ⟨q, hq, rfl⟩ := hp
     rw [fourEndpointPhysicalEdge_local_roundtrip]
     simpa [UnlabelledTypedSkeleton.cellEdges] using hq
-  · intro hz
-    obtain ⟨i, j, hi, hj, htable⟩ := S.1.2.1 z hz
-    let ai := (slotIndex i).symm ⟨z.1.1, hi⟩
-    let bj := (slotIndex j).symm ⟨z.2.1, hj⟩
+  · rintro ⟨⟨za, zx⟩, ⟨zb, zy⟩⟩ hz
+    obtain ⟨i, j, hi, hj, htable⟩ :=
+      S.1.2.1 ((⟨za, zx⟩, ⟨zb, zy⟩) :
+        RowStub (profileBlockMargin k) × ColumnStub (profileBlockMargin k)) hz
+    let ai := (slotIndex i).symm ⟨za, hi⟩
+    let bj := (slotIndex j).symm ⟨zb, hj⟩
     let a : FourEndpointBlockAtom alpha hAlpha k := ⟨i, ai⟩
     let b : FourEndpointBlockAtom alpha hAlpha k := ⟨j, bj⟩
-    let edge : FourEndpointBlockAtom alpha hAlpha k ×
-        FourEndpointBlockAtom alpha hAlpha k := (a, b)
     have ha :
-        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a = z.1.1 := by
-      exact congrArg Subtype.val ((slotIndex i).apply_symm_apply ⟨z.1.1, hi⟩)
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a = za := by
+      exact congrArg Subtype.val ((slotIndex i).apply_symm_apply ⟨za, hi⟩)
     have hb :
-        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b = z.2.1 := by
-      exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨z.2.1, hj⟩)
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b = zb := by
+      exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨zb, hj⟩)
+    subst za
+    subst zb
+    let edge : FourEndpointBlockAtom alpha hAlpha k ×
+        FourEndpointBlockAtom alpha hAlpha k := (a, b)
     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 [ha] using hi
-        · simpa only [hb] using hj
-        · simpa only [ha, hb] using htable
+        exact ⟨by simp, i, j, hi, hj, htable⟩
     let e : ↥(fourEndpointPhysicalBlockPairing
         alpha hAlpha k L slotIndex S).1.edges := ⟨edge, hedge⟩
-    let qa : Fin (profileBlockMargin k
-        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) :=
-      Fin.cast (congrArg (profileBlockMargin k) ha).symm z.1.2
-    let qb : Fin (profileBlockMargin k
-        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
-      Fin.cast (congrArg (profileBlockMargin k) hb).symm z.2.2
-    let q := (qa, qb)
-    have hglobal :
-        ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,
-          ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩) :
-          RowStub (profileBlockMargin k) ×
-            ColumnStub (profileBlockMargin k)) = z := by
-      apply Prod.ext
-      · apply Sigma.ext ha
-        apply heq_of_eq
-        apply Fin.ext
-        rfl
-      · apply Sigma.ext hb
-        apply heq_of_eq
-        apply Fin.ext
-        rfl
+    let q : Fin (profileBlockMargin k
+          (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) ×
+        Fin (profileBlockMargin k
+          (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
+      (zx, zy)
     have hq : q ∈ S.1.1.cellEdges
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) := by
-      rw [UnlabelledTypedSkeleton.cellEdges, Finset.mem_filter]
-      exact ⟨Finset.mem_univ q, by simpa only [hglobal] using hz⟩
+      simpa [q, UnlabelledTypedSkeleton.cellEdges] using hz
     let p := fourEndpointPhysicalCellEdgeToLocal
       alpha hAlpha k L slotIndex S e q
     have hp : p ∈ fourEndpointPhysicalCellLocalEdgesValidated
@@ -140,7 +128,7 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
       Finset.mem_attach, true_and]
     refine ⟨e, Finset.mem_image.mpr ⟨p, hp, ?_⟩⟩
     rw [fourEndpointPhysicalEdge_local_roundtrip]
-    exact hglobal
+    rfl
 
 /-- Forward after reverse is the identity on the endpoint physical fibre. -/
 theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse

From 02ed1a33cdbecf6b951cb824ccefbe5b1d4c1b05 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 20:09:11 +0300
Subject: [PATCH 14/26] Extract the block support and all-high deficits of an
 attained demand

---
 .../Section8AttainedDemandBlockSupport.lean   | 380 ++++++++++++++++++
 1 file changed, 380 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean

diff --git a/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
new file mode 100644
index 00000000..f321a062
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
@@ -0,0 +1,380 @@
+import Erdos625.Section8EndpointPhysicalEquiv
+import Erdos625.Section8PartialCellPhysicalFibre
+import Erdos625.Section8ProfileSkeletonWeight
+import Erdos625.Section8EndpointAllHighDecoration
+import Mathlib.Tactic
+
+/-!
+# Section VIII: block support and deficits of an attained canonical demand
+
+For a profile whose blocks are covered by the four endpoint size classes, a
+fixed slot indexing identifies every actual profile block with one abstract
+four-type block atom.  The positive support of an attained canonical demand is
+a matching; transporting it through this indexing therefore gives a literal
+`FourEndpointBlockPairing`.
+
+Every selected block cell carries one canonical all-high deficit.  This module
+proves the exact reconstruction `m_e - h_e = j_e`, the pointwise feasibility
+`j_e ≤ m_e`, and the strict half-deficit inequality `2 h_e < m_e`.
+
+No weighted sum or asymptotic estimate is asserted here.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Every profile block belongs to one of the four endpoint-size classes. -/
+def IsFourEndpointProfileCover
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1)) : Prop :=
+  ∀ a : ProfileBlockIndex k,
+    ∃ i : Fin 4, a ∈ fourEndpointBlockSlots alpha hAlpha k i
+
+/-- The abstract four-type block atom corresponding to one actual profile
+block. -/
+noncomputable def fourEndpointAtomOfProfileBlock
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (a : ProfileBlockIndex k) : FourEndpointBlockAtom alpha hAlpha k :=
+  let i := Classical.choose (hcover a)
+  let hi := Classical.choose_spec (hcover a)
+  ⟨i, (slotIndex i).symm ⟨a, hi⟩⟩
+
+/-- The abstract-to-physical block map is a right inverse of the cover-based
+physical-to-abstract map. -/
+theorem fourEndpointActualBlock_atomOfProfileBlock
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (a : ProfileBlockIndex k) :
+    fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex
+        (fourEndpointAtomOfProfileBlock alpha hAlpha k hcover slotIndex a) = a := by
+  classical
+  unfold fourEndpointAtomOfProfileBlock
+  exact congrArg Subtype.val
+    ((slotIndex (Classical.choose (hcover a))).apply_symm_apply
+      ⟨a, Classical.choose_spec (hcover a)⟩)
+
+/-- The cover-based inverse also recovers every abstract block atom. -/
+theorem fourEndpointAtomOfProfileBlock_actualBlock
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (a : FourEndpointBlockAtom alpha hAlpha k) :
+    fourEndpointAtomOfProfileBlock alpha hAlpha k hcover slotIndex
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a) = a := by
+  apply fourEndpointActualBlockOfAtom_injective alpha hAlpha k slotIndex
+  rw [fourEndpointActualBlock_atomOfProfileBlock]
+
+/-- Every covered profile block has size at most the largest endpoint size. -/
+theorem profileBlockMargin_le_fourEndpointLargest_of_cover
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (a : ProfileBlockIndex k) :
+    profileBlockMargin k a ≤ fourEndpointLargestSize alpha hAlpha := by
+  obtain ⟨i, hi⟩ := hcover a
+  have hsize : profileBlockMargin k a = fourEndpointSize alpha hAlpha i := by
+    simpa only [fourEndpointBlockSlots, Finset.mem_filter,
+      Finset.mem_univ, true_and] using hi
+  rw [hsize]
+  simpa [fourEndpointOverlapSize] using
+    fourEndpointOverlapSize_le_largest alpha hAlpha i i
+
+/-- Transport the positive support of one attained demand to abstract endpoint
+block atoms. -/
+noncomputable def fourEndpointDemandBlockEdges
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha)) :
+    Finset (FourEndpointBlockAtom alpha hAlpha k ×
+      FourEndpointBlockAtom alpha hAlpha k) :=
+  (positiveDemandSupport demand.1).image fun ab =>
+    (fourEndpointAtomOfProfileBlock alpha hAlpha k hcover slotIndex ab.1,
+      fourEndpointAtomOfProfileBlock alpha hAlpha k hcover slotIndex ab.2)
+
+/-- Membership in the transported block support is exactly membership of the
+corresponding actual block pair in the positive demand support. -/
+theorem mem_fourEndpointDemandBlockEdges_iff
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha))
+    (e : FourEndpointBlockAtom alpha hAlpha k ×
+      FourEndpointBlockAtom alpha hAlpha k) :
+    e ∈ fourEndpointDemandBlockEdges
+        alpha hAlpha k hcover slotIndex demand ↔
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1,
+        fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2) ∈
+        positiveDemandSupport demand.1 := by
+  classical
+  constructor
+  · intro he
+    rw [fourEndpointDemandBlockEdges, Finset.mem_image] at he
+    obtain ⟨ab, hab, rfl⟩ := he
+    simpa only [fourEndpointActualBlock_atomOfProfileBlock] using hab
+  · intro he
+    rw [fourEndpointDemandBlockEdges, Finset.mem_image]
+    refine ⟨(fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1,
+      fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.2), he, ?_⟩
+    apply Prod.ext
+    · exact fourEndpointAtomOfProfileBlock_actualBlock
+        alpha hAlpha k hcover slotIndex e.1
+    · exact fourEndpointAtomOfProfileBlock_actualBlock
+        alpha hAlpha k hcover slotIndex e.2
+
+/-- The transported positive support is a literal typed block matching. -/
+noncomputable def fourEndpointDemandBlockSkeleton
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha)) :
+    UnlabelledTypedSkeleton
+      (fun i : Fin 4 => fourEndpointMultiplicity alpha hAlpha k i)
+      (fun j : Fin 4 => fourEndpointMultiplicity alpha hAlpha k j) where
+  edges := fourEndpointDemandBlockEdges
+    alpha hAlpha k hcover slotIndex demand
+  leftUnique := by
+    intro x hx y hy hleft
+    have hmatching := profileHighSkeleton_positiveSupport_isBipartiteMatching
+      k (fourEndpointLargestSize alpha hAlpha)
+      (profileBlockMargin_le_fourEndpointLargest_of_cover
+        alpha hAlpha k hcover) demand
+    have hx' := (mem_fourEndpointDemandBlockEdges_iff
+      alpha hAlpha k hcover slotIndex demand x).mp hx
+    have hy' := (mem_fourEndpointDemandBlockEdges_iff
+      alpha hAlpha k hcover slotIndex demand y).mp 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 := hmatching.1 _ _ _ hx' hy' hleftActual
+    exact Prod.ext hleft
+      (fourEndpointActualBlockOfAtom_injective
+        alpha hAlpha k slotIndex hrightActual)
+  rightUnique := by
+    intro x hx y hy hright
+    have hmatching := profileHighSkeleton_positiveSupport_isBipartiteMatching
+      k (fourEndpointLargestSize alpha hAlpha)
+      (profileBlockMargin_le_fourEndpointLargest_of_cover
+        alpha hAlpha k hcover) demand
+    have hx' := (mem_fourEndpointDemandBlockEdges_iff
+      alpha hAlpha k hcover slotIndex demand x).mp hx
+    have hy' := (mem_fourEndpointDemandBlockEdges_iff
+      alpha hAlpha k hcover slotIndex demand y).mp 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 := hmatching.2 _ _ _ hx' hy' hrightActual
+    exact Prod.ext
+      (fourEndpointActualBlockOfAtom_injective
+        alpha hAlpha k slotIndex hleftActual) hright
+
+/-- The endpoint reference table attached to the positive block support. -/
+noncomputable def fourEndpointDemandSupportTable
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha)) : FourEndpointFullTable where
+  toFun := (fourEndpointDemandBlockSkeleton
+    alpha hAlpha k hcover slotIndex demand).typeTable
+
+/-- The transported support, regarded as one block pairing over its exact
+endpoint reference table. -/
+noncomputable def fourEndpointDemandBlockPairing
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha)) :
+    FourEndpointBlockPairing alpha hAlpha k
+      (fourEndpointDemandSupportTable
+        alpha hAlpha k hcover slotIndex demand) :=
+  ⟨fourEndpointDemandBlockSkeleton alpha hAlpha k hcover slotIndex demand, rfl⟩
+
+/-- Every attained demand cell is bounded by its ambient row degree. -/
+theorem profileCanonicalDemand_cell_le_row
+    {b : Nat} (k : ColoringProfile b) (U : Nat)
+    (demand : ProfileCanonicalHighSkeleton k U)
+    (a b' : ProfileBlockIndex k) :
+    demand.1 a b' ≤ profileBlockMargin k a := by
+  let witness := canonicalDemandReferenceWitness
+    (profileBlockMargin k) (profileBlockMargin k) U demand
+  let matching :=
+    (typedPartialMatchingEquivPrescribedDemandWitness demand.1
+      (profileBlockMargin k) (profileBlockMargin k)).symm witness
+  have hcard := card_typedPartialMatching_rowCell matching a b'
+  calc
+    demand.1 a b' = ((matching.rowAllocation a).1 b').card := by
+      simpa using hcard.symm
+    _ ≤ (Finset.univ : Finset (Fin (profileBlockMargin k a))).card :=
+      Finset.card_le_univ _
+    _ = profileBlockMargin k a := by simp
+
+/-- Every attained demand cell is bounded by its ambient column degree. -/
+theorem profileCanonicalDemand_cell_le_column
+    {b : Nat} (k : ColoringProfile b) (U : Nat)
+    (demand : ProfileCanonicalHighSkeleton k U)
+    (a b' : ProfileBlockIndex k) :
+    demand.1 a b' ≤ profileBlockMargin k b' := by
+  let witness := canonicalDemandReferenceWitness
+    (profileBlockMargin k) (profileBlockMargin k) U demand
+  let matching :=
+    (typedPartialMatchingEquivPrescribedDemandWitness demand.1
+      (profileBlockMargin k) (profileBlockMargin k)).symm witness
+  have hcard := card_typedPartialMatching_columnCell matching a b'
+  calc
+    demand.1 a b' = ((matching.columnAllocation b').1 a).card := by
+      simpa using hcard.symm
+    _ ≤ (Finset.univ : Finset (Fin (profileBlockMargin k b'))).card :=
+      Finset.card_le_univ _
+    _ = profileBlockMargin k b' := by simp
+
+/-- Canonical deficit of one selected block cell. -/
+def fourEndpointDemandDeficit
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha))
+    (e : ↥(fourEndpointDemandBlockPairing
+      alpha hAlpha k hcover slotIndex demand).1.edges) : Nat :=
+  fourEndpointCellFullMultiplicity alpha hAlpha
+      (fourEndpointDemandBlockPairing
+        alpha hAlpha k hcover slotIndex demand) e -
+    demand.1
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2)
+
+/-- The actual attained multiplicity is at most the full endpoint
+multiplicity. -/
+theorem fourEndpointDemandCell_le_fullMultiplicity
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha))
+    (e : ↥(fourEndpointDemandBlockPairing
+      alpha hAlpha k hcover slotIndex demand).1.edges) :
+    demand.1
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2) ≤
+      fourEndpointCellFullMultiplicity alpha hAlpha
+        (fourEndpointDemandBlockPairing
+          alpha hAlpha k hcover slotIndex demand) e := by
+  have hr := profileCanonicalDemand_cell_le_row k
+    (fourEndpointLargestSize alpha hAlpha) demand
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2)
+  have hc := profileCanonicalDemand_cell_le_column k
+    (fourEndpointLargestSize alpha hAlpha) demand
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2)
+  rw [profileBlockMargin_fourEndpointActualBlockOfAtom] at hr hc
+  simpa [fourEndpointCellFullMultiplicity, fourEndpointOverlapSize] using
+    (le_min hr hc)
+
+/-- Subtracting the canonical deficit reconstructs the attained cell
+multiplicity exactly. -/
+theorem fourEndpointCellMultiplicity_demandDeficit_eq
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha))
+    (e : ↥(fourEndpointDemandBlockPairing
+      alpha hAlpha k hcover slotIndex demand).1.edges) :
+    fourEndpointCellMultiplicityOfDeficit alpha hAlpha
+        (fourEndpointDemandBlockPairing
+          alpha hAlpha k hcover slotIndex demand)
+        (fourEndpointDemandDeficit
+          alpha hAlpha k hcover slotIndex demand) e =
+      demand.1
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2) := by
+  unfold fourEndpointCellMultiplicityOfDeficit fourEndpointDemandDeficit
+  have hle := fourEndpointDemandCell_le_fullMultiplicity
+    alpha hAlpha k hcover slotIndex demand e
+  omega
+
+/-- Every selected attained deficit lies strictly below half of its endpoint
+multiplicity. -/
+theorem fourEndpointDemandDeficit_twice_lt
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hcover : IsFourEndpointProfileCover alpha hAlpha k)
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (demand : ProfileCanonicalHighSkeleton k
+      (fourEndpointLargestSize alpha hAlpha))
+    (e : ↥(fourEndpointDemandBlockPairing
+      alpha hAlpha k hcover slotIndex demand).1.edges) :
+    2 * fourEndpointDemandDeficit
+        alpha hAlpha k hcover slotIndex demand e <
+      fourEndpointCellFullMultiplicity alpha hAlpha
+        (fourEndpointDemandBlockPairing
+          alpha hAlpha k hcover slotIndex demand) e := by
+  have hsupp := (mem_fourEndpointDemandBlockEdges_iff
+    alpha hAlpha k hcover slotIndex demand e.1).mp e.2
+  have hne : demand.1
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2) ≠ 0 := by
+    simpa only [positiveDemandSupport, Finset.mem_filter,
+      Finset.mem_univ, true_and] using hsupp
+  have hhigh := canonicalDemandImage_high
+    (profileBlockMargin k) (profileBlockMargin k)
+    (fourEndpointLargestSize alpha hAlpha) demand
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+    (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2) hne
+  have hm :
+      fourEndpointCellFullMultiplicity alpha hAlpha
+        (fourEndpointDemandBlockPairing
+          alpha hAlpha k hcover slotIndex demand) e ≤
+        fourEndpointLargestSize alpha hAlpha := by
+    exact fourEndpointOverlapSize_le_largest alpha hAlpha e.1.1.1 e.1.2.1
+  have hle := fourEndpointDemandCell_le_fullMultiplicity
+    alpha hAlpha k hcover slotIndex demand e
+  have hhalf := highMultiplicity_deficit_twice_lt
+    (fourEndpointLargestSize alpha hAlpha)
+    (fourEndpointCellFullMultiplicity alpha hAlpha
+      (fourEndpointDemandBlockPairing
+        alpha hAlpha k hcover slotIndex demand) e)
+    (demand.1
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2))
+    hm hhigh hle
+  simpa only [fourEndpointDemandDeficit] using hhalf
+
+#print axioms fourEndpointActualBlock_atomOfProfileBlock
+#print axioms fourEndpointAtomOfProfileBlock_actualBlock
+#print axioms fourEndpointDemandBlockSkeleton
+#print axioms profileCanonicalDemand_cell_le_row
+#print axioms profileCanonicalDemand_cell_le_column
+#print axioms fourEndpointCellMultiplicity_demandDeficit_eq
+#print axioms fourEndpointDemandDeficit_twice_lt
+
+end
+
+end Erdos625

From d47f9546f6400b7f30b8ffcde2f79ec318ef9e6c Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 20:14:16 +0300
Subject: [PATCH 15/26] Expose the numerical value preserved by the endpoint
 stub cast

---
 .../Section8EndpointPhysicalCellReverse.lean    | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
index 7be7f1aa..bda295f6 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
@@ -35,6 +35,22 @@ noncomputable def fourEndpointPhysicalStubToLocalEquiv
     (profileBlockMargin_fourEndpointActualBlockOfAtom
       alpha hAlpha k slotIndex a))
 
+/-- The endpoint stub cast changes only its dependent type, not its numerical
+coordinate. -/
+@[simp] theorem fourEndpointPhysicalStubToLocalEquiv_val
+    (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1))
+    (slotIndex : FourEndpointSlotIndexing alpha hAlpha k)
+    (a : FourEndpointBlockAtom alpha hAlpha k)
+    (x : Fin (profileBlockMargin k
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a))) :
+    (fourEndpointPhysicalStubToLocalEquiv
+      alpha hAlpha k slotIndex a x).val = x.val := by
+  unfold fourEndpointPhysicalStubToLocalEquiv
+  exact cast_fin_val
+    (congrArg Fin
+      (profileBlockMargin_fourEndpointActualBlockOfAtom
+        alpha hAlpha k slotIndex a)) x
+
 /-- Pull one physical cell edge back to the corresponding unit-typed local
 stub edge. -/
 noncomputable def fourEndpointPhysicalCellEdgeToLocal
@@ -276,6 +292,7 @@ noncomputable def fourEndpointPhysicalFibreToDecoratedBlockPairingValidated
     fun e => fourEndpointPhysicalCellStubMatchingValidated
       alpha hAlpha k L slotIndex S e⟩
 
+#print axioms fourEndpointPhysicalStubToLocalEquiv_val
 #print axioms fourEndpointPhysicalCellEdgeToLocal_injective
 #print axioms physicalCellEdges_card_eq_typeTable_public
 #print axioms fourEndpointPhysicalCellLocalSkeletonValidated_typeTable

From 62bc992ee9dc05867ef6a61ee150315ed87d7d34 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 21:29:00 +0300
Subject: [PATCH 16/26] Repair the endpoint physical round-trip equalities

---
 .../Section8EndpointPhysicalEquiv.lean        | 20 +++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index b59ee847..75493d3e 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -42,18 +42,21 @@ theorem fourEndpointPhysicalEdge_local_roundtrip
         ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, p.2⟩) :
         RowStub (profileBlockMargin k) ×
           ColumnStub (profileBlockMargin k)) := by
-  simp only [fourEndpointPhysicalEdgeOfLocalEdge,
-    fourEndpointPhysicalCellEdgeToLocal,
-    fourEndpointPhysicalStubToLocalEquiv, Equiv.cast_apply]
   apply Prod.ext
-  · apply Sigma.ext rfl
+  · simp only [fourEndpointPhysicalEdgeOfLocalEdge,
+      fourEndpointPhysicalCellEdgeToLocal, Prod.fst]
+    apply Sigma.ext rfl
     apply heq_of_eq
     apply Fin.ext
-    rfl
-  · apply Sigma.ext rfl
+    exact fourEndpointPhysicalStubToLocalEquiv_val
+      alpha hAlpha k slotIndex e.1.1 p.1
+  · simp only [fourEndpointPhysicalEdgeOfLocalEdge,
+      fourEndpointPhysicalCellEdgeToLocal, Prod.snd]
+    apply Sigma.ext rfl
     apply heq_of_eq
     apply Fin.ext
-    rfl
+    exact fourEndpointPhysicalStubToLocalEquiv_val
+      alpha hAlpha k slotIndex e.1.2 p.2
 
 /-- The physical skeleton underlying forward-after-reverse is the original
 physical skeleton. -/
@@ -81,7 +84,8 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
     obtain ⟨q, hq, rfl⟩ := hp
     rw [fourEndpointPhysicalEdge_local_roundtrip]
     simpa [UnlabelledTypedSkeleton.cellEdges] using hq
-  · rintro ⟨⟨za, zx⟩, ⟨zb, zy⟩⟩ hz
+  · intro hz
+    rcases z with ⟨⟨za, zx⟩, ⟨zb, zy⟩⟩
     obtain ⟨i, j, hi, hj, htable⟩ :=
       S.1.2.1 ((⟨za, zx⟩, ⟨zb, zy⟩) :
         RowStub (profileBlockMargin k) × ColumnStub (profileBlockMargin k)) hz

From 51924ad107c86594b8fa6a30ace1709e323a2b2d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 21:30:10 +0300
Subject: [PATCH 17/26] Add the attained-demand support checkpoint to focused
 CI

---
 .github/workflows/erdos625-section8-physical-fibre-closure.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
index ddee0c70..839b9374 100644
--- a/.github/workflows/erdos625-section8-physical-fibre-closure.yml
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -7,6 +7,7 @@ on:
       - "625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean"
       - "625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean"
       - "625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean"
+      - "625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean"
       - "625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean"
       - "625/formalization/Erdos625/Section8BareSkeletonClosure.lean"
       - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
@@ -48,6 +49,7 @@ jobs:
           )
           for optional in \
             625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean \
+            625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean \
             625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean \
             625/formalization/Erdos625/Section8BareSkeletonClosure.lean; do
             if [[ -f "$optional" ]]; then files+=("$optional"); fi
@@ -76,6 +78,7 @@ jobs:
           )
           for optional in \
             Erdos625.Section8EndpointPhysicalEquiv \
+            Erdos625.Section8AttainedDemandBlockSupport \
             Erdos625.Section8AttainedAllDeficitReindexing \
             Erdos625.Section8BareSkeletonClosure; do
             path="${optional//./\/}.lean"

From 06eab2a303ae8aaa08cfc30d5b2c4e5e1a99b638 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 21:38:14 +0300
Subject: [PATCH 18/26] Eliminate dependent Sigma and substitution failures in
 the endpoint equivalence

---
 .../Section8EndpointPhysicalEquiv.lean        | 40 +++++++++++++------
 1 file changed, 28 insertions(+), 12 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index 75493d3e..76ff120c 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -44,16 +44,22 @@ theorem fourEndpointPhysicalEdge_local_roundtrip
           ColumnStub (profileBlockMargin k)) := by
   apply Prod.ext
   · simp only [fourEndpointPhysicalEdgeOfLocalEdge,
-      fourEndpointPhysicalCellEdgeToLocal, Prod.fst]
-    apply Sigma.ext rfl
-    apply heq_of_eq
+      fourEndpointPhysicalCellEdgeToLocal]
+    refine congrArg
+      (fun x : Fin (profileBlockMargin k
+          (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1)) =>
+        (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.1, x⟩ :
+          RowStub (profileBlockMargin k))) ?_
     apply Fin.ext
     exact fourEndpointPhysicalStubToLocalEquiv_val
       alpha hAlpha k slotIndex e.1.1 p.1
   · simp only [fourEndpointPhysicalEdgeOfLocalEdge,
-      fourEndpointPhysicalCellEdgeToLocal, Prod.snd]
-    apply Sigma.ext rfl
-    apply heq_of_eq
+      fourEndpointPhysicalCellEdgeToLocal]
+    refine congrArg
+      (fun x : Fin (profileBlockMargin k
+          (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2)) =>
+        (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex e.1.2, x⟩ :
+          ColumnStub (profileBlockMargin k))) ?_
     apply Fin.ext
     exact fourEndpointPhysicalStubToLocalEquiv_val
       alpha hAlpha k slotIndex e.1.2 p.2
@@ -99,8 +105,6 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
     have hb :
         fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b = zb := by
       exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨zb, hj⟩)
-    subst za
-    subst zb
     let edge : FourEndpointBlockAtom alpha hAlpha k ×
         FourEndpointBlockAtom alpha hAlpha k := (a, b)
     have hedge : edge ∈ fourEndpointPhysicalBlockEdges
@@ -109,18 +113,30 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
       constructor
       · simp
       · rw [fourEndpointFullPairs, Finset.mem_filter]
-        exact ⟨by simp, i, j, hi, hj, htable⟩
+        refine ⟨by simp, i, j, ?_, ?_, ?_⟩
+        · simpa only [ha] using hi
+        · simpa only [hb] using hj
+        · simpa only [ha, hb] using htable
     let e : ↥(fourEndpointPhysicalBlockPairing
         alpha hAlpha k L slotIndex S).1.edges := ⟨edge, hedge⟩
+    let qa : Fin (profileBlockMargin k
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) :=
+      Fin.cast (congrArg (profileBlockMargin k) ha).symm zx
+    let qb : Fin (profileBlockMargin k
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
+      Fin.cast (congrArg (profileBlockMargin k) hb).symm zy
     let q : Fin (profileBlockMargin k
           (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)) ×
         Fin (profileBlockMargin k
           (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
-      (zx, zy)
+      (qa, qb)
     have hq : q ∈ S.1.1.cellEdges
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) := by
-      simpa [q, UnlabelledTypedSkeleton.cellEdges] using hz
+      rw [UnlabelledTypedSkeleton.cellEdges, Finset.mem_filter]
+      constructor
+      · exact Finset.mem_univ q
+      · simpa [q, qa, qb, ha, hb] using hz
     let p := fourEndpointPhysicalCellEdgeToLocal
       alpha hAlpha k L slotIndex S e q
     have hp : p ∈ fourEndpointPhysicalCellLocalEdgesValidated
@@ -132,7 +148,7 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
       Finset.mem_attach, true_and]
     refine ⟨e, Finset.mem_image.mpr ⟨p, hp, ?_⟩⟩
     rw [fourEndpointPhysicalEdge_local_roundtrip]
-    rfl
+    simpa [q, qa, qb, ha, hb]
 
 /-- Forward after reverse is the identity on the endpoint physical fibre. -/
 theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse

From ec7b7303ba7b39bfc089c097aeb6962b8ee9a03d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 21:48:44 +0300
Subject: [PATCH 19/26] Make the endpoint reverse edge equality explicit

---
 .../Section8EndpointPhysicalEquiv.lean        | 39 +++++++++++++++----
 1 file changed, 31 insertions(+), 8 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index 76ff120c..bbd2b7c6 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -114,9 +114,9 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
       · simp
       · rw [fourEndpointFullPairs, Finset.mem_filter]
         refine ⟨by simp, i, j, ?_, ?_, ?_⟩
-        · simpa only [ha] using hi
-        · simpa only [hb] using hj
-        · simpa only [ha, hb] using htable
+        · simpa only [edge, ha] using hi
+        · simpa only [edge, hb] using hj
+        · simpa only [edge, ha, hb] using htable
     let e : ↥(fourEndpointPhysicalBlockPairing
         alpha hAlpha k L slotIndex S).1.edges := ⟨edge, hedge⟩
     let qa : Fin (profileBlockMargin k
@@ -130,13 +130,36 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
         Fin (profileBlockMargin k
           (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b)) :=
       (qa, qb)
+    have hrow :
+        (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩ :
+          RowStub (profileBlockMargin k)) = ⟨za, zx⟩ := by
+      dsimp only [qa]
+      cases ha
+      rfl
+    have hcol :
+        (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩ :
+          ColumnStub (profileBlockMargin k)) = ⟨zb, zy⟩ := by
+      dsimp only [qb]
+      cases hb
+      rfl
+    have hglobal :
+        ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,
+          ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩) :
+          RowStub (profileBlockMargin k) × ColumnStub (profileBlockMargin k)) =
+        (⟨za, zx⟩, ⟨zb, zy⟩) :=
+      Prod.ext hrow hcol
+    have hz' :
+        ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,
+          ⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩) :
+          RowStub (profileBlockMargin k) × ColumnStub (profileBlockMargin k)) ∈
+        S.1.1.edges := by
+      rw [hglobal]
+      exact hz
     have hq : q ∈ S.1.1.cellEdges
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a)
         (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) := by
-      rw [UnlabelledTypedSkeleton.cellEdges, Finset.mem_filter]
-      constructor
-      · exact Finset.mem_univ q
-      · simpa [q, qa, qb, ha, hb] using hz
+      simpa only [UnlabelledTypedSkeleton.cellEdges, Finset.mem_filter,
+        Finset.mem_univ, true_and, q] using hz'
     let p := fourEndpointPhysicalCellEdgeToLocal
       alpha hAlpha k L slotIndex S e q
     have hp : p ∈ fourEndpointPhysicalCellLocalEdgesValidated
@@ -148,7 +171,7 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
       Finset.mem_attach, true_and]
     refine ⟨e, Finset.mem_image.mpr ⟨p, hp, ?_⟩⟩
     rw [fourEndpointPhysicalEdge_local_roundtrip]
-    simpa [q, qa, qb, ha, hb]
+    exact hglobal
 
 /-- Forward after reverse is the identity on the endpoint physical fibre. -/
 theorem fourEndpointDecoratedBlockPairingToPhysicalFibre_rightInverse

From 2ce7afebdabe5d0543e355ef0f99d4bab2a00775 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 21:55:54 +0300
Subject: [PATCH 20/26] Use Fin heterogeneous extensionality in the endpoint
 inverse

---
 .../Erdos625/Section8EndpointPhysicalEquiv.lean        | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index bbd2b7c6..2e643dd6 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -133,14 +133,16 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
     have hrow :
         (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩ :
           RowStub (profileBlockMargin k)) = ⟨za, zx⟩ := by
-      dsimp only [qa]
-      cases ha
+      apply Sigma.ext ha
+      apply (Fin.heq_ext_iff
+        (congrArg Fin (congrArg (profileBlockMargin k) ha))).2
       rfl
     have hcol :
         (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩ :
           ColumnStub (profileBlockMargin k)) = ⟨zb, zy⟩ := by
-      dsimp only [qb]
-      cases hb
+      apply Sigma.ext hb
+      apply (Fin.heq_ext_iff
+        (congrArg Fin (congrArg (profileBlockMargin k) hb))).2
       rfl
     have hglobal :
         ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,

From ad52e5eca0db37ec01b920567622198d79634127 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:02:17 +0300
Subject: [PATCH 21/26] Pass natural bound equalities to Fin heterogeneous
 extensionality

---
 625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
index 2e643dd6..80473a7f 100644
--- a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -135,14 +135,14 @@ theorem fourEndpointDecoratedPhysicalSkeleton_reverse_eq
           RowStub (profileBlockMargin k)) = ⟨za, zx⟩ := by
       apply Sigma.ext ha
       apply (Fin.heq_ext_iff
-        (congrArg Fin (congrArg (profileBlockMargin k) ha))).2
+        (congrArg (profileBlockMargin k) ha)).2
       rfl
     have hcol :
         (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b, qb⟩ :
           ColumnStub (profileBlockMargin k)) = ⟨zb, zy⟩ := by
       apply Sigma.ext hb
       apply (Fin.heq_ext_iff
-        (congrArg Fin (congrArg (profileBlockMargin k) hb))).2
+        (congrArg (profileBlockMargin k) hb)).2
       rfl
     have hglobal :
         ((⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩,

From ce4c6832bbf9ffb6c0dc393e220d6238647b7e8a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:11:38 +0300
Subject: [PATCH 22/26] Rewrite shared endpoints before applying support
 matchingness

---
 .../Section8AttainedDemandBlockSupport.lean   | 24 +++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
index f321a062..da68bec5 100644
--- a/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
+++ b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
@@ -164,7 +164,17 @@ noncomputable def fourEndpointDemandBlockSkeleton
         fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1 =
           fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1 :=
       congrArg (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex) hleft
-    have hrightActual := hmatching.1 _ _ _ hx' hy' hleftActual
+    have hy'' :
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1,
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2) ∈
+        positiveDemandSupport demand.1 := by
+      rw [hleftActual]
+      exact hy'
+    have hrightActual := hmatching.1
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2)
+      hx' hy''
     exact Prod.ext hleft
       (fourEndpointActualBlockOfAtom_injective
         alpha hAlpha k slotIndex hrightActual)
@@ -182,7 +192,17 @@ noncomputable def fourEndpointDemandBlockSkeleton
         fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2 =
           fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.2 :=
       congrArg (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex) hright
-    have hleftActual := hmatching.2 _ _ _ hx' hy' hrightActual
+    have hy'' :
+        (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1,
+          fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2) ∈
+        positiveDemandSupport demand.1 := by
+      rw [hrightActual]
+      exact hy'
+    have hleftActual := hmatching.2
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.2)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex x.1)
+      (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex y.1)
+      hx' hy''
     exact Prod.ext
       (fourEndpointActualBlockOfAtom_injective
         alpha hAlpha k slotIndex hleftActual) hright

From 6ce121df717a2f79b0ced796571ac1ead90a1cb2 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:19:02 +0300
Subject: [PATCH 23/26] Derive the endpoint block cover from four-deficit
 support

---
 .../Section8FourDeficitProfileCover.lean      | 73 +++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section8FourDeficitProfileCover.lean

diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
new file mode 100644
index 00000000..e9115b25
--- /dev/null
+++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
@@ -0,0 +1,73 @@
+import Erdos625.Section8AttainedDemandBlockSupport
+import Erdos625.MidpointProfileCoordinates
+import Mathlib.Tactic
+
+/-!
+# Section VIII: the four-deficit profile gives an endpoint block cover
+
+The attained-demand support/deficit construction is phrased for a profile whose
+actual blocks are covered by the four endpoint size classes.  The midpoint
+profile is already known to be supported on the four distinguished deficit
+coordinates.  This module supplies the finite adapter between those two
+statements.
+-/
+
+namespace Erdos625
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- A profile supported on the four distinguished deficit coordinates has every
+actual block in one of the four endpoint-size slot families. -/
+theorem isFourEndpointProfileCover_of_isFourDeficitSupported
+    (alpha : Nat) (hAlpha : 5 < alpha)
+    (k : ColoringProfile (alpha + 1))
+    (hsupport : IsFourDeficitSupported alpha k) :
+    IsFourEndpointProfileCover alpha hAlpha k := by
+  intro a
+  have haMem : (a.1 : Nat) ∈ ColoringProfile.sizes k :=
+    Multiset.mem_toFinset.mp a.1.2
+  simp only [ColoringProfile.sizes, Multiset.mem_sum] at haMem
+  obtain ⟨coord, _hcoord, hrep⟩ := haMem
+  simp only [Multiset.mem_replicate] at hrep
+  obtain ⟨hkpos, hsize⟩ := hrep
+  have hcoord := hsupport coord (by omega)
+  rcases hcoord with h0 | h1 | h2 | h3
+  · refine ⟨0, ?_⟩
+    simp only [fourEndpointBlockSlots, Finset.mem_filter,
+      Finset.mem_univ, true_and]
+    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 0
+    simpa [fourEndpointSize, fourEndpointCoordinate, h0] using hsize
+  · refine ⟨1, ?_⟩
+    simp only [fourEndpointBlockSlots, Finset.mem_filter,
+      Finset.mem_univ, true_and]
+    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 1
+    simpa [fourEndpointSize, fourEndpointCoordinate, h1] using hsize
+  · refine ⟨2, ?_⟩
+    simp only [fourEndpointBlockSlots, Finset.mem_filter,
+      Finset.mem_univ, true_and]
+    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 2
+    simpa [fourEndpointSize, fourEndpointCoordinate, h2] using hsize
+  · refine ⟨3, ?_⟩
+    simp only [fourEndpointBlockSlots, Finset.mem_filter,
+      Finset.mem_univ, true_and]
+    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 3
+    simpa [fourEndpointSize, fourEndpointCoordinate, h3] using hsize
+
+/-- The concrete four-deficit embedding used by the midpoint construction
+satisfies the endpoint-cover hypothesis needed by the Section VIII block
+support and deficit reconstruction. -/
+theorem fourDeficitEmbedding_isFourEndpointProfileCover
+    (alpha : Nat) (hAlpha : 5 < alpha) (m : Fin 4 → Nat) :
+    IsFourEndpointProfileCover alpha hAlpha
+      (fourDeficitEmbedding alpha hAlpha m) := by
+  apply isFourEndpointProfileCover_of_isFourDeficitSupported
+  exact (fourDeficitEmbedding_profile_invariants alpha hAlpha m).2.2
+
+#print axioms isFourEndpointProfileCover_of_isFourDeficitSupported
+#print axioms fourDeficitEmbedding_isFourEndpointProfileCover
+
+end
+
+end Erdos625

From 20a7238d37a33c382b5a8d99522b4032492d3bff Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:20:05 +0300
Subject: [PATCH 24/26] Build the four-deficit endpoint-cover adapter in
 focused CI

---
 .github/workflows/erdos625-section8-physical-fibre-closure.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.github/workflows/erdos625-section8-physical-fibre-closure.yml b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
index 839b9374..8d9ad0e8 100644
--- a/.github/workflows/erdos625-section8-physical-fibre-closure.yml
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -8,6 +8,7 @@ on:
       - "625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean"
       - "625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean"
       - "625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean"
+      - "625/formalization/Erdos625/Section8FourDeficitProfileCover.lean"
       - "625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean"
       - "625/formalization/Erdos625/Section8BareSkeletonClosure.lean"
       - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
@@ -50,6 +51,7 @@ jobs:
           for optional in \
             625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean \
             625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean \
+            625/formalization/Erdos625/Section8FourDeficitProfileCover.lean \
             625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean \
             625/formalization/Erdos625/Section8BareSkeletonClosure.lean; do
             if [[ -f "$optional" ]]; then files+=("$optional"); fi
@@ -79,6 +81,7 @@ jobs:
           for optional in \
             Erdos625.Section8EndpointPhysicalEquiv \
             Erdos625.Section8AttainedDemandBlockSupport \
+            Erdos625.Section8FourDeficitProfileCover \
             Erdos625.Section8AttainedAllDeficitReindexing \
             Erdos625.Section8BareSkeletonClosure; do
             path="${optional//./\/}.lean"

From 5ca2856e15e25d4f7f9c9d50a678460db7c825a8 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:31:49 +0300
Subject: [PATCH 25/26] Split the four-support alternatives explicitly

---
 .../Section8FourDeficitProfileCover.lean      | 43 +++++++++++--------
 1 file changed, 24 insertions(+), 19 deletions(-)

diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
index e9115b25..21733164 100644
--- a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
+++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
@@ -32,28 +32,33 @@ theorem isFourEndpointProfileCover_of_isFourDeficitSupported
   obtain ⟨coord, _hcoord, hrep⟩ := haMem
   simp only [Multiset.mem_replicate] at hrep
   obtain ⟨hkpos, hsize⟩ := hrep
-  have hcoord := hsupport coord (by omega)
-  rcases hcoord with h0 | h1 | h2 | h3
-  · refine ⟨0, ?_⟩
+  rcases hsupport coord (by omega) with h0 | hrest
+  · subst coord
+    refine ⟨0, ?_⟩
     simp only [fourEndpointBlockSlots, Finset.mem_filter,
       Finset.mem_univ, true_and]
     change (a.1 : Nat) = fourEndpointSize alpha hAlpha 0
-    simpa [fourEndpointSize, fourEndpointCoordinate, h0] using hsize
-  · refine ⟨1, ?_⟩
-    simp only [fourEndpointBlockSlots, Finset.mem_filter,
-      Finset.mem_univ, true_and]
-    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 1
-    simpa [fourEndpointSize, fourEndpointCoordinate, h1] using hsize
-  · refine ⟨2, ?_⟩
-    simp only [fourEndpointBlockSlots, Finset.mem_filter,
-      Finset.mem_univ, true_and]
-    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 2
-    simpa [fourEndpointSize, fourEndpointCoordinate, h2] using hsize
-  · refine ⟨3, ?_⟩
-    simp only [fourEndpointBlockSlots, Finset.mem_filter,
-      Finset.mem_univ, true_and]
-    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 3
-    simpa [fourEndpointSize, fourEndpointCoordinate, h3] using hsize
+    simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
+  · rcases hrest with h1 | hrest
+    · subst coord
+      refine ⟨1, ?_⟩
+      simp only [fourEndpointBlockSlots, Finset.mem_filter,
+        Finset.mem_univ, true_and]
+      change (a.1 : Nat) = fourEndpointSize alpha hAlpha 1
+      simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
+    · rcases hrest with h2 | h3
+      · subst coord
+        refine ⟨2, ?_⟩
+        simp only [fourEndpointBlockSlots, Finset.mem_filter,
+          Finset.mem_univ, true_and]
+        change (a.1 : Nat) = fourEndpointSize alpha hAlpha 2
+        simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
+      · subst coord
+        refine ⟨3, ?_⟩
+        simp only [fourEndpointBlockSlots, Finset.mem_filter,
+          Finset.mem_univ, true_and]
+        change (a.1 : Nat) = fourEndpointSize alpha hAlpha 3
+        simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
 
 /-- The concrete four-deficit embedding used by the midpoint construction
 satisfies the endpoint-cover hypothesis needed by the Section VIII block

From e5752daf4bb2763e2cd5ec875c0e30a629eb26e0 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sun, 26 Jul 2026 22:44:18 +0300
Subject: [PATCH 26/26] Recover the endpoint coordinate from its real deficit

---
 .../Section8FourDeficitProfileCover.lean      | 51 +++++++++----------
 1 file changed, 24 insertions(+), 27 deletions(-)

diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
index 21733164..2d146496 100644
--- a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
+++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
@@ -32,33 +32,30 @@ theorem isFourEndpointProfileCover_of_isFourDeficitSupported
   obtain ⟨coord, _hcoord, hrep⟩ := haMem
   simp only [Multiset.mem_replicate] at hrep
   obtain ⟨hkpos, hsize⟩ := hrep
-  rcases hsupport coord (by omega) with h0 | hrest
-  · subst coord
-    refine ⟨0, ?_⟩
-    simp only [fourEndpointBlockSlots, Finset.mem_filter,
-      Finset.mem_univ, true_and]
-    change (a.1 : Nat) = fourEndpointSize alpha hAlpha 0
-    simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
-  · rcases hrest with h1 | hrest
-    · subst coord
-      refine ⟨1, ?_⟩
-      simp only [fourEndpointBlockSlots, Finset.mem_filter,
-        Finset.mem_univ, true_and]
-      change (a.1 : Nat) = fourEndpointSize alpha hAlpha 1
-      simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
-    · rcases hrest with h2 | h3
-      · subst coord
-        refine ⟨2, ?_⟩
-        simp only [fourEndpointBlockSlots, Finset.mem_filter,
-          Finset.mem_univ, true_and]
-        change (a.1 : Nat) = fourEndpointSize alpha hAlpha 2
-        simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
-      · subst coord
-        refine ⟨3, ?_⟩
-        simp only [fourEndpointBlockSlots, Finset.mem_filter,
-          Finset.mem_univ, true_and]
-        change (a.1 : Nat) = fourEndpointSize alpha hAlpha 3
-        simpa [fourEndpointSize, fourEndpointCoordinate] using hsize
+  obtain ⟨i, hdeficit⟩ := hsupport coord hkpos
+  have hdeficit' :
+      profileDeficit alpha coord =
+        profileDeficit alpha (fourDeficitCoordinate alpha hAlpha i) := by
+    rw [profileDeficit_fourDeficitCoordinate]
+    exact hdeficit
+  have hclass :
+      profileClassSize coord =
+        profileClassSize (fourDeficitCoordinate alpha hAlpha i) := by
+    unfold profileDeficit at hdeficit'
+    linarith
+  have hval :
+      coord.val + 1 =
+        (fourDeficitCoordinate alpha hAlpha i).val + 1 := by
+    unfold profileClassSize at hclass
+    exact_mod_cast hclass
+  refine ⟨i, ?_⟩
+  simp only [fourEndpointBlockSlots, Finset.mem_filter,
+    Finset.mem_univ, true_and]
+  change (a.1 : Nat) = fourEndpointSize alpha hAlpha i
+  calc
+    (a.1 : Nat) = coord.val + 1 := hsize
+    _ = (fourDeficitCoordinate alpha hAlpha i).val + 1 := hval
+    _ = fourEndpointSize alpha hAlpha i := rfl
 
 /-- The concrete four-deficit embedding used by the midpoint construction
 satisfies the endpoint-cover hypothesis needed by the Section VIII block