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..8d9ad0e8
--- /dev/null
+++ b/.github/workflows/erdos625-section8-physical-fibre-closure.yml
@@ -0,0 +1,111 @@
+name: Erdős 625 Section 8 physical-fibre closure
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean"
+      - "625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean"
+      - "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"
+      - "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:
+
+concurrency:
+  group: erdos625-section8-physical-fibre-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+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:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in accepted closure modules
+        shell: bash
+        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/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
+          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 every accepted closure checkpoint warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          targets=(
+            Erdos625.Section8EndpointPhysicalBlockReverse
+            Erdos625.Section8EndpointPhysicalCellReverse
+            Erdos625.Section8PartialCellPhysicalFibre
+          )
+          for optional in \
+            Erdos625.Section8EndpointPhysicalEquiv \
+            Erdos625.Section8AttainedDemandBlockSupport \
+            Erdos625.Section8FourDeficitProfileCover \
+            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
+        with:
+          name: erdos625-section8-physical-fibre-closure-log
+          path: /tmp/section8-physical-fibre-closure.log
+          if-no-files-found: ignore
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()
diff --git a/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
new file mode 100644
index 00000000..da68bec5
--- /dev/null
+++ b/625/formalization/Erdos625/Section8AttainedDemandBlockSupport.lean
@@ -0,0 +1,400 @@
+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 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)
+  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 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
+
+/-- 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
diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
new file mode 100644
index 00000000..455d9abc
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalBlockReverse.lean
@@ -0,0 +1,263 @@
+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
+        · simpa only [F, fourEndpointActualBlockOfAtom, hei] using
+            (slotIndex edge.1.1 edge.1.2).2
+        · simpa only [F, 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
+  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
diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
new file mode 100644
index 00000000..bda295f6
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalCellReverse.lean
@@ -0,0 +1,302 @@
+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))
+
+/-- 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
+    (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 fourEndpointPhysicalStubToLocalEquiv_val
+#print axioms fourEndpointPhysicalCellEdgeToLocal_injective
+#print axioms physicalCellEdges_card_eq_typeTable_public
+#print axioms fourEndpointPhysicalCellLocalSkeletonValidated_typeTable
+
+end
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
new file mode 100644
index 00000000..80473a7f
--- /dev/null
+++ b/625/formalization/Erdos625/Section8EndpointPhysicalEquiv.lean
@@ -0,0 +1,237 @@
+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
+  · simp only [fourEndpointPhysicalEdgeOfLocalEdge,
+      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]
+    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
+
+/-- 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
+  classical
+  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
+    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
+    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⟩
+    have ha :
+        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 = zb := by
+      exact congrArg Subtype.val ((slotIndex j).apply_symm_apply ⟨zb, hj⟩)
+    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 [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
+        (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)) :=
+      (qa, qb)
+    have hrow :
+        (⟨fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a, qa⟩ :
+          RowStub (profileBlockMargin k)) = ⟨za, zx⟩ := by
+      apply Sigma.ext ha
+      apply (Fin.heq_ext_iff
+        (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 (profileBlockMargin k) hb)).2
+      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
+      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
+        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
diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
new file mode 100644
index 00000000..2d146496
--- /dev/null
+++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean
@@ -0,0 +1,75 @@
+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
+  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
+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
diff --git a/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean b/625/formalization/Erdos625/Section8PartialCellPhysicalFibre.lean
new file mode 100644
index 00000000..320d0db8
--- /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