diff --git a/.github/workflows/erdos625-attained-partial-weight-identification.yml b/.github/workflows/erdos625-attained-partial-weight-identification.yml
new file mode 100644
index 00000000..859b9b5b
--- /dev/null
+++ b/.github/workflows/erdos625-attained-partial-weight-identification.yml
@@ -0,0 +1,83 @@
+name: Erdős 625 attained partial weight identification
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean"
+      - "625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean"
+      - "625/proofs/SECTION8_ATTAINED_PARTIAL_WEIGHT_IDENTIFICATION.md"
+      - "625/experiments/section8_attained_partial_weight_identity.py"
+      - ".github/workflows/erdos625-attained-partial-weight-identification.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-attained-partial-weight-${{ 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
+        shell: bash
+        run: |
+          files=(
+            625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean
+          )
+          if [[ -f 625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean ]]; then
+            files+=(625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean)
+          fi
+          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 deepest present identification module warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          if [[ -f Erdos625/Section8ProfilePartialAggregateWeight.lean ]]; then
+            target=Erdos625.Section8ProfilePartialAggregateWeight
+          else
+            target=Erdos625.Section8MatchingDemandCellFibre
+          fi
+          set +e
+          lake build "$target" --wfail \
+            > /tmp/erdos625-attained-partial-weight.log 2>&1
+          status=$?
+          tail -n 900 /tmp/erdos625-attained-partial-weight.log
+          exit $status
+      - name: Upload focused Lean log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-attained-partial-weight-lean-log
+          path: /tmp/erdos625-attained-partial-weight.log
+          if-no-files-found: ignore
+
+  exact-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Run exact regression when present
+        shell: bash
+        run: |
+          if [[ -f 625/experiments/section8_attained_partial_weight_identity.py ]]; then
+            python -m py_compile 625/experiments/section8_attained_partial_weight_identity.py
+            python 625/experiments/section8_attained_partial_weight_identity.py
+            python -O 625/experiments/section8_attained_partial_weight_identity.py
+          else
+            echo "Exact regression will be added with the weight-identification layer."
+          fi
diff --git a/625/experiments/section8_attained_partial_weight_identity.py b/625/experiments/section8_attained_partial_weight_identity.py
new file mode 100644
index 00000000..026eb234
--- /dev/null
+++ b/625/experiments/section8_attained_partial_weight_identity.py
@@ -0,0 +1,135 @@
+#!/usr/bin/env python3
+"""Exact regression for the matching-demand physical-fibre identity.
+
+For small matching-supported demand tables, compare:
+
+1. the global prescribed-demand physical-skeleton cardinality;
+2. the product of the independent one-cell partial-matching cardinalities;
+3. the corresponding reward/incidence aggregate weights.
+
+All arithmetic is integer or Fraction arithmetic.  These checks support but do
+not replace the Lean equivalence.
+"""
+
+from __future__ import annotations
+
+from fractions import Fraction
+from itertools import combinations, permutations, product
+from math import factorial
+
+
+def falling(n: int, k: int) -> int:
+    if k < 0 or k > n:
+        return 0
+    value = 1
+    for offset in range(k):
+        value *= n - offset
+    return value
+
+
+def reward(j: int) -> int:
+    if j <= 2:
+        return 1
+    return 2 ** (j * (j - 1) // 2 - 1)
+
+
+def global_fibre_card(row: tuple[int, ...], col: tuple[int, ...], demand: tuple[tuple[int, ...], ...]) -> int:
+    row_product = 1
+    for i, degree in enumerate(row):
+        row_product *= falling(degree, sum(demand[i]))
+    col_product = 1
+    for j, degree in enumerate(col):
+        col_product *= falling(degree, sum(demand[i][j] for i in range(len(row))))
+    denominator = 1
+    for line in demand:
+        for value in line:
+            denominator *= factorial(value)
+    assert denominator > 0
+    assert (row_product * col_product) % denominator == 0
+    return row_product * col_product // denominator
+
+
+def local_product_card(row: tuple[int, ...], col: tuple[int, ...], demand: tuple[tuple[int, ...], ...]) -> int:
+    value = 1
+    for i, line in enumerate(demand):
+        for j, multiplicity in enumerate(line):
+            if multiplicity:
+                numerator = falling(row[i], multiplicity) * falling(col[j], multiplicity)
+                assert numerator % factorial(multiplicity) == 0
+                value *= numerator // factorial(multiplicity)
+    return value
+
+
+def total_demand(demand: tuple[tuple[int, ...], ...]) -> int:
+    return sum(sum(line) for line in demand)
+
+
+def local_reward(demand: tuple[tuple[int, ...], ...]) -> int:
+    value = 1
+    for line in demand:
+        for multiplicity in line:
+            if multiplicity:
+                value *= reward(multiplicity)
+    return value
+
+
+def aggregate_weight(
+    ambient: int,
+    row: tuple[int, ...],
+    col: tuple[int, ...],
+    demand: tuple[tuple[int, ...], ...],
+) -> Fraction:
+    return Fraction(global_fibre_card(row, col, demand) * local_reward(demand), falling(ambient, total_demand(demand)))
+
+
+def matching_demands(row: tuple[int, ...], col: tuple[int, ...]):
+    rows = range(len(row))
+    cols = range(len(col))
+    yield tuple(tuple(0 for _ in cols) for _ in rows)
+    for size in range(1, min(len(row), len(col)) + 1):
+        for chosen_rows in combinations(rows, size):
+            for chosen_cols in combinations(cols, size):
+                for ordered_cols in permutations(chosen_cols):
+                    bounds = [min(row[i], col[j]) for i, j in zip(chosen_rows, ordered_cols)]
+                    for multiplicities in product(*(range(1, bound + 1) for bound in bounds)):
+                        table = [[0 for _ in cols] for _ in rows]
+                        for i, j, value in zip(chosen_rows, ordered_cols, multiplicities):
+                            table[i][j] = value
+                        yield tuple(tuple(line) for line in table)
+
+
+def run() -> None:
+    cases = 0
+    weighted_cases = 0
+    for row in product(range(1, 5), repeat=3):
+        for col in product(range(1, 5), repeat=3):
+            for demand in matching_demands(row, col):
+                total = total_demand(demand)
+                if total > sum(row) or total > sum(col):
+                    continue
+                global_card = global_fibre_card(row, col, demand)
+                local_card = local_product_card(row, col, demand)
+                assert global_card == local_card, (row, col, demand, global_card, local_card)
+                cases += 1
+                ambient = max(sum(row), total)
+                if falling(ambient, total):
+                    global_weight = aggregate_weight(ambient, row, col, demand)
+                    local_weight = Fraction(local_card * local_reward(demand), falling(ambient, total))
+                    assert global_weight == local_weight
+                    weighted_cases += 1
+
+    # A nonmatching table demonstrates why the factorization requires the
+    # support-matching hypothesis: row selections are shared between cells.
+    row = (3, 3)
+    col = (3, 3)
+    nonmatching = ((1, 1), (0, 0))
+    assert global_fibre_card(row, col, nonmatching) != local_product_card(row, col, nonmatching)
+
+    print("ERDOS 625 MATCHING-DEMAND PARTIAL-FIBRE REGRESSION: PASS")
+    print(f"  exact cardinality cases: {cases}")
+    print(f"  exact weighted cases: {weighted_cases}")
+    print("  nonmatching control: correctly fails cellwise factorization")
+
+
+if __name__ == "__main__":
+    run()
diff --git a/625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean b/625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean
new file mode 100644
index 00000000..37b6d7fc
--- /dev/null
+++ b/625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean
@@ -0,0 +1,536 @@
+import Erdos625.Section8ProfileSkeletonWeight
+import Erdos625.Section8EndpointSingleCellStubs
+import Mathlib.Tactic
+
+/-!
+# Section VIII: exact local-cell fibre of a matching-supported demand
+
+Let `demand : A → B → Nat` be a finite demand table whose positive support is a
+bipartite matching. A physical skeleton with this type table is exactly a
+product of independent one-cell partial stub matchings, one for every positive
+cell. This module proves that statement as a literal finite equivalence.
+
+This is the aggregate physical-fibre theorem needed in place of an objectwise
+"complete every cell and delete deficits" construction. It introduces no
+full-cell completion and no probability or asymptotic estimate.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- One independent literal partial stub matching in every positive demand
+cell. -/
+abbrev MatchingDemandCellDecoration
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat) :=
+  ∀ e : ↥(positiveDemandSupport demand),
+    SingleCellStubMatching (row e.1.1) (col e.1.2)
+      (demand e.1.1 e.1.2)
+
+/-- Embed one local one-cell edge in the global typed stub spaces. -/
+def matchingDemandPhysicalEdgeOfLocalEdge
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (e : ↥(positiveDemandSupport demand))
+    (p : RowStub (fun _ : Unit => row e.1.1) ×
+      ColumnStub (fun _ : Unit => col e.1.2)) :
+    RowStub row × ColumnStub col :=
+  (⟨e.1.1, p.1.2⟩, ⟨e.1.2, p.2.2⟩)
+
+/-- The local-to-global edge map is injective. -/
+theorem matchingDemandPhysicalEdgeOfLocalEdge_injective
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (e : ↥(positiveDemandSupport demand)) :
+    Function.Injective
+      (matchingDemandPhysicalEdgeOfLocalEdge
+        (demand := demand) (row := row) (col := col) e) := by
+  intro p q hpq
+  apply Prod.ext
+  · apply Sigma.ext (x := p.1) (y := q.1) rfl
+    apply heq_of_eq
+    apply Fin.ext
+    simpa only [matchingDemandPhysicalEdgeOfLocalEdge] using
+      congrArg (fun z => z.1.2.val) hpq
+  · apply Sigma.ext (x := p.2) (y := q.2) rfl
+    apply heq_of_eq
+    apply Fin.ext
+    simpa only [matchingDemandPhysicalEdgeOfLocalEdge] using
+      congrArg (fun z => z.2.2.val) hpq
+
+/-- Union of the physical edges supplied by all positive demand cells. -/
+def matchingDemandDecoratedPhysicalEdges
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (D : MatchingDemandCellDecoration demand row col) :
+    Finset (RowStub row × ColumnStub col) :=
+  (positiveDemandSupport demand).attach.biUnion fun e =>
+    (D e).1.edges.image fun p => matchingDemandPhysicalEdgeOfLocalEdge e p
+
+/-- A matching-supported cell decoration gives one global physical skeleton. -/
+def matchingDemandDecoratedPhysicalSkeleton
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand))
+    (D : MatchingDemandCellDecoration demand row col) :
+    UnlabelledTypedSkeleton row col where
+  edges := matchingDemandDecoratedPhysicalEdges D
+  leftUnique := by
+    intro x hx y hy hxy
+    simp only [matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and, Finset.mem_image] at hx hy
+    obtain ⟨ex, px, hpx, rfl⟩ := hx
+    obtain ⟨ey, py, hpy, rfl⟩ := hy
+    have ha : ex.1.1 = ey.1.1 := (Sigma.mk.inj_iff.mp hxy).1
+    have hb : ex.1.2 = ey.1.2 :=
+      hmatching.1 ex.1.1 ex.1.2 ey.1.2 ex.2 (by
+        rw [ha]
+        exact ey.2)
+    have he : ex = ey := Subtype.ext (Prod.ext ha hb)
+    subst ey
+    have hpl : px.1 = py.1 := by
+      apply Sigma.ext (x := px.1) (y := py.1) rfl
+      exact (Sigma.mk.inj_iff.mp hxy).2
+    have hp : px = py := (D ex).1.leftUnique px hpx py hpy hpl
+    subst py
+    rfl
+  rightUnique := by
+    intro x hx y hy hxy
+    simp only [matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and, Finset.mem_image] at hx hy
+    obtain ⟨ex, px, hpx, rfl⟩ := hx
+    obtain ⟨ey, py, hpy, rfl⟩ := hy
+    have hb : ex.1.2 = ey.1.2 := (Sigma.mk.inj_iff.mp hxy).1
+    have ha : ex.1.1 = ey.1.1 :=
+      hmatching.2 ex.1.2 ex.1.1 ey.1.1 ex.2 (by
+        rw [hb]
+        exact ey.2)
+    have he : ex = ey := Subtype.ext (Prod.ext ha hb)
+    subst ey
+    have hpr : px.2 = py.2 := by
+      apply Sigma.ext (x := px.2) (y := py.2) rfl
+      exact (Sigma.mk.inj_iff.mp hxy).2
+    have hp : px = py := (D ex).1.rightUnique px hpx py hpy hpr
+    subst py
+    rfl
+
+/-- In one selected positive cell, the global physical edge filter is exactly
+the image of the corresponding local cell matching. -/
+theorem matchingDemandDecoratedPhysicalSkeleton_cellEdges_selected
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand))
+    (D : MatchingDemandCellDecoration demand row col)
+    (e : ↥(positiveDemandSupport demand)) :
+    (matchingDemandDecoratedPhysicalSkeleton hmatching D).edges.filter
+        (fun z => z.1.1 = e.1.1 ∧ z.2.1 = e.1.2) =
+      (D e).1.edges.image fun p => matchingDemandPhysicalEdgeOfLocalEdge e p := by
+  ext z
+  constructor
+  · intro hz
+    rw [Finset.mem_filter] at hz
+    rcases hz with ⟨hz, hztype⟩
+    simp only [matchingDemandDecoratedPhysicalSkeleton,
+      matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and, Finset.mem_image] at hz
+    obtain ⟨e', p, hp, rfl⟩ := hz
+    have he : e' = e := Subtype.ext (Prod.ext hztype.1 hztype.2)
+    subst e'
+    exact Finset.mem_image.mpr ⟨p, hp, rfl⟩
+  · intro hz
+    rw [Finset.mem_image] at hz
+    obtain ⟨p, hp, rfl⟩ := hz
+    rw [Finset.mem_filter]
+    constructor
+    · simp only [matchingDemandDecoratedPhysicalSkeleton,
+        matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+        Finset.mem_attach, true_and]
+      exact ⟨e, Finset.mem_image.mpr ⟨p, hp, rfl⟩⟩
+    · simp [matchingDemandPhysicalEdgeOfLocalEdge]
+
+/-- The global skeleton has the prescribed multiplicity in every selected
+positive cell. -/
+theorem matchingDemandDecoratedPhysicalSkeleton_typeTable_selected
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand))
+    (D : MatchingDemandCellDecoration demand row col)
+    (e : ↥(positiveDemandSupport demand)) :
+    (matchingDemandDecoratedPhysicalSkeleton hmatching D).typeTable
+        e.1.1 e.1.2 = demand e.1.1 e.1.2 := by
+  unfold UnlabelledTypedSkeleton.typeTable
+  rw [matchingDemandDecoratedPhysicalSkeleton_cellEdges_selected hmatching D e]
+  rw [Finset.card_image_of_injective]
+  · simpa [UnlabelledTypedSkeleton.typeTable] using (D e).2
+  · exact matchingDemandPhysicalEdgeOfLocalEdge_injective e
+
+/-- No edge of the constructed skeleton lies in a zero demand cell. -/
+theorem matchingDemandDecoratedPhysicalSkeleton_typeTable_zero
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand))
+    (D : MatchingDemandCellDecoration demand row col)
+    (a : A) (b : B) (hzero : demand a b = 0) :
+    (matchingDemandDecoratedPhysicalSkeleton hmatching D).typeTable a b = 0 := by
+  unfold UnlabelledTypedSkeleton.typeTable
+  have hfilter :
+      (matchingDemandDecoratedPhysicalSkeleton hmatching D).edges.filter
+          (fun z => z.1.1 = a ∧ z.2.1 = b) = ∅ := by
+    ext z
+    constructor
+    · intro hz
+      rw [Finset.mem_filter] at hz
+      rcases hz with ⟨hz, ha, hb⟩
+      simp only [matchingDemandDecoratedPhysicalSkeleton,
+        matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+        Finset.mem_attach, true_and, Finset.mem_image] at hz
+      obtain ⟨e, p, hp, hzp⟩ := hz
+      have hea : e.1.1 = a :=
+        (congrArg (fun x => x.1.1) hzp).trans ha
+      have heb : e.1.2 = b :=
+        (congrArg (fun x => x.2.1) hzp).trans hb
+      have hepos : demand e.1.1 e.1.2 ≠ 0 := by
+        simpa only [positiveDemandSupport, Finset.mem_filter,
+          Finset.mem_univ, true_and] using e.2
+      have habpos : demand a b ≠ 0 := by
+        simpa [hea, heb] using hepos
+      exact (habpos hzero).elim
+    · simp
+  rw [hfilter]
+  simp
+
+/-- The physical skeleton assembled from local cell decorations has exactly the
+original demand table. -/
+theorem matchingDemandDecoratedPhysicalSkeleton_typeTable
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand))
+    (D : MatchingDemandCellDecoration demand row col) :
+    (matchingDemandDecoratedPhysicalSkeleton hmatching D).typeTable = demand := by
+  funext a b
+  by_cases hzero : demand a b = 0
+  · simpa [hzero] using
+      matchingDemandDecoratedPhysicalSkeleton_typeTable_zero
+        hmatching D a b hzero
+  · let e : ↥(positiveDemandSupport demand) :=
+      ⟨(a, b), by simp [positiveDemandSupport, hzero]⟩
+    simpa [e] using
+      matchingDemandDecoratedPhysicalSkeleton_typeTable_selected hmatching D e
+
+/-- Forward map from local cell decorations to the exact global physical
+skeleton fibre. -/
+def matchingDemandCellDecorationToPhysicalFibre
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand)) :
+    MatchingDemandCellDecoration demand row col →
+      {S : UnlabelledTypedSkeleton row col // S.typeTable = demand} := fun D =>
+  ⟨matchingDemandDecoratedPhysicalSkeleton hmatching D,
+    matchingDemandDecoratedPhysicalSkeleton_typeTable hmatching D⟩
+
+/-- The global physical skeleton determines every local one-cell decoration. -/
+theorem matchingDemandCellDecorationToPhysicalFibre_injective
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand)) :
+    Function.Injective
+      (matchingDemandCellDecorationToPhysicalFibre demand row col hmatching) := by
+  intro D₁ D₂ hPhysical
+  have hSkeleton :
+      matchingDemandDecoratedPhysicalSkeleton hmatching D₁ =
+        matchingDemandDecoratedPhysicalSkeleton hmatching D₂ :=
+    congrArg Subtype.val hPhysical
+  funext e
+  have hImage :
+      (D₁ e).1.edges.image (fun p => matchingDemandPhysicalEdgeOfLocalEdge e p) =
+        (D₂ e).1.edges.image (fun p => matchingDemandPhysicalEdgeOfLocalEdge e p) := by
+    rw [← matchingDemandDecoratedPhysicalSkeleton_cellEdges_selected
+      hmatching D₁ e]
+    rw [← matchingDemandDecoratedPhysicalSkeleton_cellEdges_selected
+      hmatching D₂ e]
+    rw [hSkeleton]
+  have hLocalEdges : (D₁ e).1.edges = (D₂ e).1.edges := by
+    ext p
+    constructor
+    · intro hp
+      have hpImage : matchingDemandPhysicalEdgeOfLocalEdge e p ∈
+          (D₁ e).1.edges.image (fun q =>
+            matchingDemandPhysicalEdgeOfLocalEdge e q) :=
+        Finset.mem_image.mpr ⟨p, hp, rfl⟩
+      rw [hImage] at hpImage
+      obtain ⟨q, hq, hpq⟩ := Finset.mem_image.mp hpImage
+      have hpq' : p = q :=
+        matchingDemandPhysicalEdgeOfLocalEdge_injective e hpq.symm
+      simpa [hpq'] using hq
+    · intro hp
+      have hpImage : matchingDemandPhysicalEdgeOfLocalEdge e p ∈
+          (D₂ e).1.edges.image (fun q =>
+            matchingDemandPhysicalEdgeOfLocalEdge e q) :=
+        Finset.mem_image.mpr ⟨p, hp, rfl⟩
+      rw [← hImage] at hpImage
+      obtain ⟨q, hq, hpq⟩ := Finset.mem_image.mp hpImage
+      have hpq' : p = q :=
+        matchingDemandPhysicalEdgeOfLocalEdge_injective e hpq.symm
+      simpa [hpq'] using hq
+  exact Subtype.ext (UnlabelledTypedSkeleton.ext hLocalEdges)
+
+/-- Pull one global physical cell edge into the corresponding unit-typed local
+coordinates. -/
+def matchingDemandPhysicalCellEdgeToLocal
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (e : ↥(positiveDemandSupport demand)) :
+    Fin (row e.1.1) × Fin (col e.1.2) →
+      RowStub (fun _ : Unit => row e.1.1) ×
+        ColumnStub (fun _ : Unit => col e.1.2) := fun p =>
+  (⟨(), p.1⟩, ⟨(), p.2⟩)
+
+/-- The pulled-back local edge map is injective. -/
+theorem matchingDemandPhysicalCellEdgeToLocal_injective
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (e : ↥(positiveDemandSupport demand)) :
+    Function.Injective
+      (matchingDemandPhysicalCellEdgeToLocal
+        (demand := demand) (row := row) (col := col) e) := by
+  intro p q hpq
+  apply Prod.ext
+  · exact eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.fst hpq)).2
+  · exact eq_of_heq (Sigma.mk.inj_iff.mp (congrArg Prod.snd hpq)).2
+
+/-- Local one-cell skeleton pulled back from a global physical skeleton fibre. -/
+def matchingDemandPhysicalCellLocalSkeleton
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (S : {S : UnlabelledTypedSkeleton row col // S.typeTable = demand})
+    (e : ↥(positiveDemandSupport demand)) :
+    UnlabelledTypedSkeleton (fun _ : Unit => row e.1.1)
+      (fun _ : Unit => col e.1.2) where
+  edges := (S.1.cellEdges e.1.1 e.1.2).image
+    (matchingDemandPhysicalCellEdgeToLocal e)
+  leftUnique := by
+    intro x hx y hy hxy
+    rw [Finset.mem_image] at hx hy
+    obtain ⟨p, hp, rfl⟩ := hx
+    obtain ⟨q, hq, rfl⟩ := hy
+    have hpFirst : p.1 = q.1 :=
+      eq_of_heq (Sigma.mk.inj_iff.mp hxy).2
+    have hpEdge :
+        ((⟨e.1.1, p.1⟩, ⟨e.1.2, p.2⟩) : RowStub row × ColumnStub col) ∈
+          S.1.edges := by
+      simpa [UnlabelledTypedSkeleton.cellEdges] using hp
+    have hqEdge :
+        ((⟨e.1.1, q.1⟩, ⟨e.1.2, q.2⟩) : RowStub row × ColumnStub col) ∈
+          S.1.edges := by
+      simpa [UnlabelledTypedSkeleton.cellEdges] using hq
+    have hrow : (⟨e.1.1, p.1⟩ : RowStub row) = ⟨e.1.1, q.1⟩ :=
+      Sigma.ext rfl (heq_of_eq hpFirst)
+    have hglobal := S.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 (matchingDemandPhysicalCellEdgeToLocal e)
+      (Prod.ext hpFirst hpSecond)
+  rightUnique := by
+    intro x hx y hy hxy
+    rw [Finset.mem_image] at hx hy
+    obtain ⟨p, hp, rfl⟩ := hx
+    obtain ⟨q, hq, rfl⟩ := hy
+    have hpSecond : p.2 = q.2 :=
+      eq_of_heq (Sigma.mk.inj_iff.mp hxy).2
+    have hpEdge :
+        ((⟨e.1.1, p.1⟩, ⟨e.1.2, p.2⟩) : RowStub row × ColumnStub col) ∈
+          S.1.edges := by
+      simpa [UnlabelledTypedSkeleton.cellEdges] using hp
+    have hqEdge :
+        ((⟨e.1.1, q.1⟩, ⟨e.1.2, q.2⟩) : RowStub row × ColumnStub col) ∈
+          S.1.edges := by
+      simpa [UnlabelledTypedSkeleton.cellEdges] using hq
+    have hcol : (⟨e.1.2, p.2⟩ : ColumnStub col) = ⟨e.1.2, q.2⟩ :=
+      Sigma.ext rfl (heq_of_eq hpSecond)
+    have hglobal := S.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 (matchingDemandPhysicalCellEdgeToLocal e)
+      (Prod.ext hpFirst hpSecond)
+
+/-- The pulled-back local skeleton has exactly the prescribed cell
+multiplicity. -/
+theorem matchingDemandPhysicalCellLocalSkeleton_typeTable
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (S : {S : UnlabelledTypedSkeleton row col // S.typeTable = demand})
+    (e : ↥(positiveDemandSupport demand)) :
+    (matchingDemandPhysicalCellLocalSkeleton S e).typeTable () () =
+      demand e.1.1 e.1.2 := by
+  unfold UnlabelledTypedSkeleton.typeTable
+  have hAll :
+      (matchingDemandPhysicalCellLocalSkeleton S e).edges.filter
+          (fun z => z.1.1 = () ∧ z.2.1 = ()) =
+        (matchingDemandPhysicalCellLocalSkeleton S e).edges := by
+    ext z
+    simp
+  rw [hAll]
+  change ((S.1.cellEdges e.1.1 e.1.2).image
+    (matchingDemandPhysicalCellEdgeToLocal e)).card = _
+  rw [Finset.card_image_of_injective]
+  · have hcell : (S.1.cellEdges e.1.1 e.1.2).card =
+        S.1.typeTable e.1.1 e.1.2 := by
+      unfold UnlabelledTypedSkeleton.cellEdges UnlabelledTypedSkeleton.typeTable
+      refine Finset.card_bij
+        (fun p _ => ((⟨e.1.1, p.1⟩, ⟨e.1.2, 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, hA, hB⟩ := hedge
+        obtain ⟨⟨a, r⟩, ⟨b, c⟩⟩ := edge
+        simp only at hA hB
+        subst a
+        subst b
+        exact ⟨(r, c), by simp [hEdge], rfl⟩
+    rw [hcell]
+    exact congrFun (congrFun S.2 e.1.1) e.1.2
+  · exact matchingDemandPhysicalCellEdgeToLocal_injective e
+
+/-- Reverse map from the exact physical fibre to the product of local one-cell
+matchings. -/
+def matchingDemandPhysicalFibreToCellDecoration
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat) :
+    {S : UnlabelledTypedSkeleton row col // S.typeTable = demand} →
+      MatchingDemandCellDecoration demand row col := fun S e =>
+  ⟨matchingDemandPhysicalCellLocalSkeleton S e,
+    matchingDemandPhysicalCellLocalSkeleton_typeTable S e⟩
+
+/-- Mapping a pulled-back local edge forward recovers the original physical
+edge. -/
+theorem matchingDemandPhysicalEdge_local_roundtrip
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    {demand : A → B → Nat} {row : A → Nat} {col : B → Nat}
+    (e : ↥(positiveDemandSupport demand))
+    (p : Fin (row e.1.1) × Fin (col e.1.2)) :
+    matchingDemandPhysicalEdgeOfLocalEdge e
+        (matchingDemandPhysicalCellEdgeToLocal e p) =
+      ((⟨e.1.1, p.1⟩, ⟨e.1.2, p.2⟩) :
+        RowStub row × ColumnStub col) := by
+  rfl
+
+/-- Forward after reverse is the identity on the global physical skeleton
+fibre. -/
+theorem matchingDemandCellDecorationToPhysicalFibre_rightInverse
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand)) :
+    Function.RightInverse
+      (matchingDemandPhysicalFibreToCellDecoration demand row col)
+      (matchingDemandCellDecorationToPhysicalFibre demand row col hmatching) := by
+  intro S
+  apply Subtype.ext
+  apply UnlabelledTypedSkeleton.ext
+  ext z
+  constructor
+  · intro hz
+    simp only [matchingDemandCellDecorationToPhysicalFibre,
+      matchingDemandDecoratedPhysicalSkeleton,
+      matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and, Finset.mem_image] at hz
+    obtain ⟨e, p, hp, rfl⟩ := hz
+    change p ∈ (matchingDemandPhysicalCellLocalSkeleton S e).edges at hp
+    rw [matchingDemandPhysicalCellLocalSkeleton, Finset.mem_image] at hp
+    obtain ⟨q, hq, rfl⟩ := hp
+    rw [matchingDemandPhysicalEdge_local_roundtrip]
+    simpa [UnlabelledTypedSkeleton.cellEdges] using hq
+  · intro hz
+    rcases z with ⟨⟨a, r⟩, ⟨b, c⟩⟩
+    have hcellpos : demand a b ≠ 0 := by
+      have htypepos : S.1.typeTable a b ≠ 0 :=
+        (S.1.typeTable_ne_zero_iff_exists_physical_edge a b).2
+          ⟨((⟨a, r⟩, ⟨b, c⟩) : RowStub row × ColumnStub col), hz, rfl, rfl⟩
+      have hcell := congrFun (congrFun S.2 a) b
+      simpa only [hcell] using htypepos
+    let e : ↥(positiveDemandSupport demand) :=
+      ⟨(a, b), by simp [positiveDemandSupport, hcellpos]⟩
+    let q : Fin (row a) × Fin (col b) := (r, c)
+    have hq : q ∈ S.1.cellEdges a b := by
+      simp [q, UnlabelledTypedSkeleton.cellEdges, hz]
+    let p := matchingDemandPhysicalCellEdgeToLocal e q
+    have hp : p ∈ (matchingDemandPhysicalCellLocalSkeleton S e).edges := by
+      rw [matchingDemandPhysicalCellLocalSkeleton, Finset.mem_image]
+      exact ⟨q, hq, rfl⟩
+    simp only [matchingDemandCellDecorationToPhysicalFibre,
+      matchingDemandDecoratedPhysicalSkeleton,
+      matchingDemandDecoratedPhysicalEdges, Finset.mem_biUnion,
+      Finset.mem_attach, true_and]
+    refine ⟨e, Finset.mem_image.mpr ⟨p, hp, ?_⟩⟩
+    rfl
+
+/-- Reverse after forward is the identity on local cell decorations. -/
+theorem matchingDemandCellDecorationToPhysicalFibre_leftInverse
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand)) :
+    Function.LeftInverse
+      (matchingDemandPhysicalFibreToCellDecoration demand row col)
+      (matchingDemandCellDecorationToPhysicalFibre demand row col hmatching) := by
+  intro D
+  apply matchingDemandCellDecorationToPhysicalFibre_injective
+    demand row col hmatching
+  exact matchingDemandCellDecorationToPhysicalFibre_rightInverse
+    demand row col hmatching
+      (matchingDemandCellDecorationToPhysicalFibre demand row col hmatching D)
+
+/-- Exact finite equivalence between the global physical skeleton fibre and the
+product of its positive-cell partial matching fibres. -/
+def matchingDemandCellDecorationEquivPhysicalFibre
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand)) :
+    MatchingDemandCellDecoration demand row col ≃
+      {S : UnlabelledTypedSkeleton row col // S.typeTable = demand} where
+  toFun := matchingDemandCellDecorationToPhysicalFibre demand row col hmatching
+  invFun := matchingDemandPhysicalFibreToCellDecoration demand row col
+  left_inv := matchingDemandCellDecorationToPhysicalFibre_leftInverse
+    demand row col hmatching
+  right_inv := matchingDemandCellDecorationToPhysicalFibre_rightInverse
+    demand row col hmatching
+
+#print axioms matchingDemandDecoratedPhysicalSkeleton_typeTable
+#print axioms matchingDemandCellDecorationToPhysicalFibre_injective
+#print axioms matchingDemandPhysicalCellLocalSkeleton_typeTable
+#print axioms matchingDemandCellDecorationToPhysicalFibre_rightInverse
+#print axioms matchingDemandCellDecorationToPhysicalFibre_leftInverse
+
+end
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean b/625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean
new file mode 100644
index 00000000..a304dd32
--- /dev/null
+++ b/625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean
@@ -0,0 +1,165 @@
+import Erdos625.Section8MatchingDemandCellFibre
+import Mathlib.Tactic
+
+/-!
+# Section VIII: pointwise attained partial-cell aggregate weight
+
+The preceding matching-demand equivalence removes the completion ambiguity:
+for a matching-supported demand table, the global physical skeleton fibre is
+exactly a product of independent one-cell partial matching fibres.
+
+This module computes the cardinality of that product and applies it to the exact
+profile high-skeleton weight. The final theorem is pointwise in one attained
+canonical demand and introduces no endpoint completion, probability estimate,
+or asymptotic bound.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Product of the unique local cell-factorial denominators. -/
+def matchingDemandCellFactorialProduct
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) : Nat :=
+  ∏ e : ↥(positiveDemandSupport demand),
+    (demand e.1.1 e.1.2).factorial
+
+/-- Product of the two local descending-factorial stub selections in every
+positive demand cell. -/
+def matchingDemandCellSelectionProduct
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat) : Nat :=
+  ∏ e : ↥(positiveDemandSupport demand),
+    (row e.1.1).descFactorial (demand e.1.1 e.1.2) *
+      (col e.1.2).descFactorial (demand e.1.1 e.1.2)
+
+/-- Exact cross-multiplied cardinality of the product of positive-cell partial
+matching fibres. -/
+theorem card_matchingDemandCellDecoration_mul_factorials
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat) :
+    Fintype.card (MatchingDemandCellDecoration demand row col) *
+        matchingDemandCellFactorialProduct demand =
+      matchingDemandCellSelectionProduct demand row col := by
+  classical
+  rw [Fintype.card_pi]
+  unfold matchingDemandCellFactorialProduct
+    matchingDemandCellSelectionProduct
+  rw [← Finset.prod_mul_distrib]
+  apply Finset.prod_congr rfl
+  intro e _he
+  exact card_singleCellStubMatching_mul_factorial
+    (row e.1.1) (col e.1.2) (demand e.1.1 e.1.2)
+
+/-- The product of local factorials is positive. -/
+theorem matchingDemandCellFactorialProduct_ne_zero
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) :
+    matchingDemandCellFactorialProduct demand ≠ 0 := by
+  unfold matchingDemandCellFactorialProduct
+  exact Finset.prod_ne_zero_iff.mpr fun _ _ => Nat.factorial_ne_zero _
+
+/-- Division form of the exact local-cell product cardinality in `ENNReal`. -/
+theorem ennreal_card_matchingDemandCellDecoration_eq_quotient
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat) :
+    (Fintype.card (MatchingDemandCellDecoration demand row col) : ENNReal) =
+      (matchingDemandCellSelectionProduct demand row col : ENNReal) /
+        (matchingDemandCellFactorialProduct demand : ENNReal) := by
+  apply (ENNReal.eq_div_iff
+    (Nat.cast_ne_zero.mpr
+      (matchingDemandCellFactorialProduct_ne_zero demand))
+    (ENNReal.natCast_ne_top _)).2
+  simpa only [Nat.cast_mul, mul_comm] using
+    congrArg (fun x : Nat => (x : ENNReal))
+      (card_matchingDemandCellDecoration_mul_factorials demand row col)
+
+/-- The exact aggregate obtained by summing any weight constant on the local
+cell-decoration fibre. -/
+def matchingDemandCellAggregateWeight
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (atomWeight : ENNReal) : ENNReal :=
+  ((matchingDemandCellSelectionProduct demand row col : Nat) : ENNReal) /
+      ((matchingDemandCellFactorialProduct demand : Nat) : ENNReal) *
+    atomWeight
+
+/-- Summing a common atom over all independent positive-cell partial matchings
+is exactly the aggregate quotient weight. -/
+theorem sum_matchingDemandCellDecoration_const_eq_aggregateWeight
+    {A B : Type*}
+    [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B]
+    (demand : A → B → Nat) (row : A → Nat) (col : B → Nat)
+    (atomWeight : ENNReal) :
+    (∑ _ : MatchingDemandCellDecoration demand row col, atomWeight) =
+      matchingDemandCellAggregateWeight demand row col atomWeight := by
+  rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
+  rw [ennreal_card_matchingDemandCellDecoration_eq_quotient]
+  rfl
+
+/-- Pointwise completion-free identity for one attained profile high skeleton.
+The exact physical fibre is replaced by the equivalent product of local
+positive-cell partial matching fibres, and its common atom is the existing
+`profileHighSkeletonWitnessWeight`. -/
+theorem profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight
+    {b : Nat} (k : ColoringProfile b) (U : Nat)
+    (demand : ProfileCanonicalHighSkeleton k U)
+    (hmatching : IsBipartiteMatching (positiveDemandSupport demand.1)) :
+    profileHighSkeletonWeight k U demand =
+      matchingDemandCellAggregateWeight demand.1
+        (profileBlockMargin k) (profileBlockMargin k)
+        (profileHighSkeletonWitnessWeight k U demand) := by
+  calc
+    profileHighSkeletonWeight k U demand =
+        ∑ _ : {S : UnlabelledTypedSkeleton (profileBlockMargin k)
+          (profileBlockMargin k) // S.typeTable = demand.1},
+            profileHighSkeletonWitnessWeight k U demand :=
+      profileHighSkeletonWeight_eq_sum_unlabelledSkeletonFibre k U demand
+    _ = ∑ _ : MatchingDemandCellDecoration demand.1
+          (profileBlockMargin k) (profileBlockMargin k),
+            profileHighSkeletonWitnessWeight k U demand := by
+      rw [Finset.sum_const, Finset.sum_const,
+        Finset.card_univ, Finset.card_univ]
+      rw [← Fintype.card_congr
+        (matchingDemandCellDecorationEquivPhysicalFibre demand.1
+          (profileBlockMargin k) (profileBlockMargin k) hmatching)]
+    _ = matchingDemandCellAggregateWeight demand.1
+          (profileBlockMargin k) (profileBlockMargin k)
+          (profileHighSkeletonWitnessWeight k U demand) :=
+      sum_matchingDemandCellDecoration_const_eq_aggregateWeight
+        demand.1 (profileBlockMargin k) (profileBlockMargin k)
+          (profileHighSkeletonWitnessWeight k U demand)
+
+/-- Structural specialization: every attained canonical profile high demand
+with the usual degree cap satisfies the pointwise aggregate identity. -/
+theorem profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight_of_cap
+    {b : Nat} (k : ColoringProfile b) (U : Nat)
+    (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+    (demand : ProfileCanonicalHighSkeleton k U) :
+    profileHighSkeletonWeight k U demand =
+      matchingDemandCellAggregateWeight demand.1
+        (profileBlockMargin k) (profileBlockMargin k)
+        (profileHighSkeletonWitnessWeight k U demand) := by
+  apply profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight
+  exact profileHighSkeleton_positiveSupport_isBipartiteMatching k U hcap demand
+
+#print axioms card_matchingDemandCellDecoration_mul_factorials
+#print axioms ennreal_card_matchingDemandCellDecoration_eq_quotient
+#print axioms sum_matchingDemandCellDecoration_const_eq_aggregateWeight
+#print axioms profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight
+#print axioms profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight_of_cap
+
+end
+
+end Erdos625
diff --git a/625/proofs/SECTION8_ATTAINED_PARTIAL_WEIGHT_IDENTIFICATION.md b/625/proofs/SECTION8_ATTAINED_PARTIAL_WEIGHT_IDENTIFICATION.md
new file mode 100644
index 00000000..9f53d51f
--- /dev/null
+++ b/625/proofs/SECTION8_ATTAINED_PARTIAL_WEIGHT_IDENTIFICATION.md
@@ -0,0 +1,187 @@
+# Section VIII attained partial-fibre and weight identification
+
+## Purpose
+
+The line-by-line audit isolates one exact finite seam in the canonical proof:
+the passage from an attained physical high skeleton to a block support with one
+deficit and one partial stub matching in every selected cell.
+
+The unsafe mental picture is:
+
+> choose a full-cell completion and delete the deficit edges.
+
+A partial physical matching usually has many full completions, and its unused
+stubs may participate in residual cells.  No proof should depend on choosing one
+of those completions.
+
+The replacement is an aggregate finite theorem.
+
+## Generic matching-demand theorem
+
+Let
+
+```text
+demand : A -> B -> Nat
+```
+
+have positive support
+
+```text
+M = {(a,b) : demand(a,b) != 0}
+```
+
+which is a bipartite matching.  Let `row(a)` and `col(b)` be the ambient stub
+degrees.  Define
+
+```text
+MatchingDemandCellDecoration demand row col
+```
+
+to be one literal one-cell partial matching of size `demand(a,b)` for every
+`(a,b) in M`.
+
+The new Lean module constructs and proves the equivalence
+
+```text
+MatchingDemandCellDecoration demand row col
+  ≃
+{S : UnlabelledTypedSkeleton row col // S.typeTable = demand}.
+```
+
+The forward map unions the local physical edges.  Matchingness of `M` gives
+global row- and column-stub uniqueness.  The reverse map restricts a physical
+skeleton to each positive type cell.  The two round trips use no full-cell
+completion and no ordering of edges within a cell.
+
+## Exact cardinality identity
+
+For one positive cell \(e=(a,b)\), put
+
+\[
+ j_e=\operatorname{demand}(a,b).
+\]
+
+The local fibre has cardinality
+
+\[
+ rac{(\operatorname{row}(a))_{j_e}
+       (\operatorname{col}(b))_{j_e}}{j_e!}.
+\]
+
+The finite equivalence therefore gives
+
+\[
+ \left|\{S:S.\operatorname{typeTable}=\operatorname{demand}\}
ight|
+ =
+ \prod_{e\in M}
+ rac{(\operatorname{row}(e_1))_{j_e}
+       (\operatorname{col}(e_2))_{j_e}}{j_e!}.
+\]
+
+This is the matching-supported specialization of the global prescribed-demand
+quotient.  It has one and only one factorial denominator per positive cell.
+
+The support-matching hypothesis is essential.  If two positive cells share a
+row, their row-stub selections are not independent, and the product of the
+single-cell cardinalities overcounts.
+
+## Pointwise bare-weight identity
+
+For an attained canonical high demand \(L\), define
+
+\[
+ J(L)=\sum_{e\in\operatorname{supp}_+(L)}L_e,
+ \qquad
+ G(L)=\prod_{e\in\operatorname{supp}_+(L)}g(L_e).
+\]
+
+Every physical realization has common atom weight
+
+\[
+ \frac{G(L)}{(n)_{J(L)}}.
+\]
+
+Summing that atom over the exact fibre gives
+
+\[
+ w_{\mathrm{hi}}(L)
+ =
+ \frac{G(L)}{(n)_{J(L)}}
+ \prod_{e\in\operatorname{supp}_+(L)}
+ \frac{(s_e)_{L_e}(t_e)_{L_e}}{L_e!}.
+\]
+
+This is precisely the aggregate partial-cell weight.  The equality is a finite
+cardinality theorem, not a heuristic completion argument.
+
+## Four-endpoint specialization
+
+For the four-size midpoint profile, the support/deficit encoding supplies:
+
+```text
+P       = fourEndpointDemandBlockPairing ... demand
+h(e)    = fourEndpointDemandDeficit ... demand e
+m(e)    = fourEndpointCellFullMultiplicity ... P e
+j(e)    = m(e) - h(e).
+```
+
+The already checked reconstruction theorem gives
+
+```text
+j(e) = demand(actualRow(e), actualColumn(e)),
+```
+
+and the high condition gives
+
+```text
+2*h(e) < m(e).
+```
+
+Consequently the generic aggregate weight specializes to
+
+```text
+fourEndpointPartialAggregateWeight
+  totalMass alpha hAlpha P h.
+```
+
+The next theorem after the generic equivalence is therefore the pointwise
+identity
+
+```text
+profileHighSkeletonWeight k U demand
+  =
+fourEndpointPartialAggregateWeight
+      totalMass alpha hAlpha P h.
+```
+
+Once this is green, the injective attained-demand reindexing in PR #48 and the
+cellwise geometric partition function in PR #49 may be applied without an
+unproved multiplicity assertion.
+
+## Exact regression
+
+`625/experiments/section8_attained_partial_weight_identity.py` enumerates small
+matching-supported demand tables and verifies with exact integer/Fraction
+arithmetic that:
+
+1. the global prescribed-demand fibre cardinality equals the product of the
+   local one-cell cardinalities;
+2. the corresponding reward/incidence weights agree;
+3. a deliberately nonmatching support fails the independent-cell product,
+   confirming the necessity of the matching hypothesis.
+
+The script is a regression check, not a substitute for the Lean equivalence.
+
+## Remaining boundary
+
+This work closes the aggregate physical-fibre ambiguity once both the generic
+equivalence and the pointwise profile specialization are warning-fatally green.
+It does not by itself sum all support/deficit data or prove the phase asymptotic.
+The remaining order is:
+
+1. apply the pointwise identity inside the injective support/deficit sum;
+2. use the sharp complete-deficit partition function;
+3. group zero-deficit references by full endpoint table;
+4. apply endpoint transportation and Lemma 7.1;
+5. compose with the q-only literal attachment theorem;
+6. export Proposition 9.2.