From e9baeec402faf9c7eb91336738f0d407dc1d7935 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:05:04 +0300
Subject: [PATCH 1/3] Add exact physical-fibre ratio theorem

---
 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md | 264 +++++++++++++++++++++++
 1 file changed, 264 insertions(+)
 create mode 100644 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md

diff --git a/625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md b/625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md
new file mode 100644
index 00000000..55a6bf5a
--- /dev/null
+++ b/625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md
@@ -0,0 +1,264 @@
+# Exact physical-fibre ratio at fixed high support
+
+## Status and purpose
+
+This note proves the finite counting identity used by the corrected Section VIII
+route once the block support is fixed.  It strengthens the exposition by
+replacing a sequence of local comparisons with one exact formula.
+
+It does **not** close the remaining global theorem.  The unresolved step is
+still the disjoint reindexing of every attained canonical high skeleton by:
+
+```text
+block support + admissible deficits + local partial physical matchings,
+```
+
+with neither omission nor multiplicity and with exact aggregate weight
+preservation.  The theorem below begins after that support-and-multiplicity data
+has been fixed.
+
+## Setup
+
+Let \(P\) be a matching of selected block pairs.  For \(e\in P\), let the two
+endpoint blocks have sizes \(s_e,t_e\), and put
+
+\[
+  m_e:=\min\{s_e,t_e\},
+  \qquad
+  d_e:=|s_e-t_e|.
+\]
+
+Choose a deficit \(0\le h_e\le m_e\), and write
+
+\[
+  j_e:=m_e-h_e,
+  \qquad
+  J:=\sum_{e\in P}j_e,
+  \qquad
+  H:=\sum_{e\in P}h_e.
+\]
+
+Thus the full-containment reference has total multiplicity \(J+H\).
+
+A size-\(j\) physical fibre between labelled blocks of sizes \(s,t\) is a
+partial bijection between a \(j\)-subset of the first block and a \(j\)-subset
+of the second.  Let \(\mathcal M_{s,t}(j)\) denote this finite set.  The exact
+signed-overlap cell factor is
+
+\[
+  g(j):=2^{\binom j2-1}.
+\]
+
+For fixed \(P\) and \(j=(j_e)\), define the aggregate physical weight
+
+\[
+  w(P,j)
+  :=
+  \frac1{(n)_J}
+  \prod_{e\in P}
+    |\mathcal M_{s_e,t_e}(j_e)|g(j_e).
+\]
+
+This definition has one global falling-factorial denominator.  It does not
+replace that denominator by a product of independent ambient denominators.
+
+## Exact theorem
+
+### Theorem
+
+For every fixed support \(P\) and admissible multiplicity vector \(j=m-h\):
+
+1. the local fibre cardinality is
+   
+   \[
+     |\mathcal M_{s,t}(j)|
+     =\binom sj\binom tj j!
+     =\frac{(s)_j(t)_j}{j!};
+   \]
+
+2. for endpoint sizes \(m,m+d\), the exact local weighted deficit ratio is
+   
+   \[
+     \frac{
+       |\mathcal M_{m,m+d}(m-h)|g(m-h)
+     }{
+       |\mathcal M_{m,m+d}(m)|g(m)
+     }
+     =R_{m,d}(h),
+   \]
+   
+   where
+   
+   \[
+     R_{m,d}(h)
+     :=
+     \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}
+     2^{-hm+h(h+1)/2};
+   \]
+
+3. the full fixed-support ratio is the exact identity
+   
+   \[
+     \boxed{
+     \frac{w(P,m-h)}{w(P,m)}
+     =(n-J)_H\prod_{e\in P}R_{m_e,d_e}(h_e).}
+   \]
+
+Consequently,
+
+\[
+  \frac{w(P,m-h)}{w(P,m)}
+  \le
+  \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e).
+\]
+
+If the high-cell condition gives \(2h_e<m_e\) whenever \(h_e>0\), then
+
+\[
+  R_{m_e,d_e}(h_e)
+  \le
+  \left(
+    \frac{m_e}{2^{\lfloor2m_e/3\rfloor}}
+  \right)^{h_e}.
+\]
+
+Hence, with
+
+\[
+  \rho_n:=
+  \max_m\frac{nm}{2^{\lfloor2m/3\rfloor}},
+\]
+
+one has
+
+\[
+  \frac{w(P,m-h)}{w(P,m)}
+  \le
+  \rho_n^H.
+\]
+
+### Proof
+
+Choose the \(j\) left endpoints, choose the \(j\) right endpoints, and choose a
+bijection between them.  This gives
+
+\[
+  |\mathcal M_{s,t}(j)|
+  =\binom sj\binom tj j!
+  =\frac{(s)_j(t)_j}{j!}.
+\]
+
+Assume \(s=m\) and \(t=m+d\).  The unweighted local ratio is
+
+\[
+\begin{aligned}
+  \frac{|\mathcal M_{m,m+d}(m-h)|}
+       {|\mathcal M_{m,m+d}(m)|}
+  &=
+  \frac{
+    (m)_{m-h}(m+d)_{m-h}/(m-h)!
+  }{
+    (m)_m(m+d)_m/m!
+  }\\
+  &=
+  \binom mh\frac{d!}{(d+h)!}\\
+  &=
+  \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}.
+\end{aligned}
+\]
+
+The cell-factor ratio is
+
+\[
+  \frac{g(m-h)}{g(m)}
+  =
+  2^{\binom{m-h}{2}-\binom m2}
+  =
+  2^{-hm+h(h+1)/2}.
+\]
+
+Multiplying proves the exact local formula.
+
+For the global ratio, note that the full multiplicity is
+
+\[
+  \sum_{e\in P}m_e=J+H.
+\]
+
+Therefore
+
+\[
+\begin{aligned}
+  \frac{w(P,m-h)}{w(P,m)}
+  &=
+  \frac{(n)_{J+H}}{(n)_J}
+  \prod_{e\in P}R_{m_e,d_e}(h_e)\\
+  &=
+  (n-J)_H
+  \prod_{e\in P}R_{m_e,d_e}(h_e).
+\end{aligned}
+\]
+
+This is the exact one-global-denominator identity.  Since
+\((n-J)_H\le n^H=\prod_en^{h_e}\), the displayed upper bound follows.
+
+Finally suppose \(h>0\) and \(2h<m\).  Since
+
+\[
+  \frac{\binom mh}{(d+1)\cdots(d+h)}\le m^h,
+\]
+
+it remains to control the power of two.  The inequality \(2h<m\) implies
+\(h+1\le2m/3\) for \(m\ge3\), and hence
+
+\[
+  m-\frac{h+1}{2}
+  \ge\frac{2m}{3}
+  \ge\left\lfloor\frac{2m}{3}\right\rfloor.
+\]
+
+Thus
+
+\[
+  -hm+\frac{h(h+1)}2
+  \le
+  -h\left\lfloor\frac{2m}{3}\right\rfloor,
+\]
+
+which proves the geometric majorant.  Multiplying over \(e\in P\) and inserting
+the factor \(n^H\) gives the final claim.  \(\square\)
+
+## Why this improves the proof
+
+The corrected Section VIII argument can now be written in three clean steps.
+
+1. **Reindexing theorem:** identify every attained canonical high skeleton with
+   one fixed-support physical fibre.  This is the remaining open seam.
+2. **Exact ratio theorem:** apply the boxed identity above.
+3. **Aggregate summation:** sum the geometric deficit factors and then apply
+   the endpoint transport estimate.
+
+The local factorial algebra and the global finite-population denominator no
+longer need to be interleaved.  In particular, the proof cannot accidentally
+introduce one ambient denominator per high cell.
+
+## Executable finite audit
+
+`625/scripts/verify_physical_fibre_exact_ratio.py` uses only exact integers and
+`fractions.Fraction`.  It checks:
+
+- 140 literal partial-matching enumerations for block sizes at most six;
+- 1,296 exact local weighted-ratio identities;
+- 580 multi-cell exact global-ratio identities with one global denominator;
+- 14,160 instances of the high-deficit geometric bound;
+- the direction of the replacement \((n-J)_H\le n^H\).
+
+The script prints an explicit scope boundary:
+
+```text
+fixed-support physical-fibre identities checked;
+global attained-skeleton reindexing not claimed
+```
+
+This distinction must remain in the PR description and any manuscript status
+statement.
\ No newline at end of file

From bd976ca47b146ef85963f83f598bd60c9a5ed5f7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:05:30 +0300
Subject: [PATCH 2/3] Add exact physical-fibre ratio audit

---
 .../verify_physical_fibre_exact_ratio.py      | 225 ++++++++++++++++++
 1 file changed, 225 insertions(+)
 create mode 100644 625/scripts/verify_physical_fibre_exact_ratio.py

diff --git a/625/scripts/verify_physical_fibre_exact_ratio.py b/625/scripts/verify_physical_fibre_exact_ratio.py
new file mode 100644
index 00000000..c8b0eafa
--- /dev/null
+++ b/625/scripts/verify_physical_fibre_exact_ratio.py
@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+"""Exact finite audit of the Erdős 625 physical-fibre weight identities.
+
+This script checks the local partial-matching cardinality, the exact weighted
+deficit ratio, the one-global-denominator identity, and the finite geometric
+majorant used in the corrected Section VIII route.  It does not claim the
+remaining global reindexing of every attained canonical high skeleton.
+"""
+from __future__ import annotations
+
+from fractions import Fraction
+from itertools import combinations, permutations, product
+from math import comb, factorial, floor
+import json
+
+
+def falling(value: int, length: int) -> int:
+    if value < 0 or length < 0 or length > value:
+        raise ValueError("invalid falling factorial")
+    result = 1
+    for offset in range(length):
+        result *= value - offset
+    return result
+
+
+def rising(value: int, length: int) -> int:
+    if value <= 0 or length < 0:
+        raise ValueError("invalid rising factorial")
+    result = 1
+    for offset in range(length):
+        result *= value + offset
+    return result
+
+
+def power_two(exponent: int) -> Fraction:
+    if exponent >= 0:
+        return Fraction(2**exponent, 1)
+    return Fraction(1, 2 ** (-exponent))
+
+
+def cell_factor(size: int) -> Fraction:
+    """The exact signed-overlap cell factor g(size)=2^(C(size,2)-1)."""
+    if size < 0:
+        raise ValueError("negative cell size")
+    return power_two(size * (size - 1) // 2 - 1)
+
+
+def partial_matching_count(left_size: int, right_size: int, size: int) -> int:
+    if size < 0 or size > min(left_size, right_size):
+        return 0
+    return (
+        falling(left_size, size)
+        * falling(right_size, size)
+        // factorial(size)
+    )
+
+
+def brute_partial_matching_count(left_size: int, right_size: int, size: int) -> int:
+    """Enumerate literal partial bijections between two labelled blocks."""
+    if size < 0 or size > min(left_size, right_size):
+        return 0
+    count = 0
+    for left_subset in combinations(range(left_size), size):
+        for right_subset in combinations(range(right_size), size):
+            for right_order in permutations(right_subset):
+                # Pair the sorted left subset with an ordered right subset.
+                tuple(zip(left_subset, right_order))
+                count += 1
+    return count
+
+
+def weighted_local_fibre(left_size: int, right_size: int, size: int) -> Fraction:
+    return Fraction(
+        partial_matching_count(left_size, right_size, size), 1
+    ) * cell_factor(size)
+
+
+def local_deficit_ratio(m: int, d: int, h: int) -> Fraction:
+    if m < 0 or d < 0 or h < 0 or h > m:
+        raise ValueError("invalid deficit parameters")
+    denominator = rising(d + 1, h) if h else 1
+    exponent = -h * m + h * (h + 1) // 2
+    return Fraction(comb(m, h), denominator) * power_two(exponent)
+
+
+def support_weight(
+    n: int,
+    endpoint_sizes: tuple[tuple[int, int], ...],
+    multiplicities: tuple[int, ...],
+) -> Fraction:
+    if len(endpoint_sizes) != len(multiplicities):
+        raise ValueError("support and multiplicity lengths differ")
+    total = sum(multiplicities)
+    if total > n:
+        raise ValueError("global multiplicity exceeds n")
+    numerator = Fraction(1, 1)
+    for (left_size, right_size), size in zip(endpoint_sizes, multiplicities):
+        numerator *= weighted_local_fibre(left_size, right_size, size)
+    return numerator / falling(n, total)
+
+
+def verify_brute_local_counts(max_block_size: int = 6) -> int:
+    checks = 0
+    for left_size in range(max_block_size + 1):
+        for right_size in range(max_block_size + 1):
+            for size in range(min(left_size, right_size) + 1):
+                actual = brute_partial_matching_count(left_size, right_size, size)
+                expected = partial_matching_count(left_size, right_size, size)
+                if actual != expected:
+                    raise AssertionError(
+                        "partial matching count failed for "
+                        f"{(left_size, right_size, size)}"
+                    )
+                checks += 1
+    return checks
+
+
+def verify_local_ratio(max_m: int = 24, max_d: int = 3) -> int:
+    checks = 0
+    for m in range(1, max_m + 1):
+        for d in range(max_d + 1):
+            full = weighted_local_fibre(m, m + d, m)
+            for h in range(m + 1):
+                partial = weighted_local_fibre(m, m + d, m - h)
+                expected = local_deficit_ratio(m, d, h)
+                if partial / full != expected:
+                    raise AssertionError(
+                        f"local weighted ratio failed for {(m, d, h)}"
+                    )
+                checks += 1
+    return checks
+
+
+def verify_global_ratio() -> dict[str, int]:
+    """Check the exact one-global-denominator identity on support products."""
+    support_families = (
+        ((2, 2),),
+        ((3, 4),),
+        ((4, 6),),
+        ((2, 3), (3, 3)),
+        ((3, 5), (4, 4)),
+        ((2, 4), (3, 5), (5, 6)),
+    )
+    checks = equality_cases = 0
+    for endpoints in support_families:
+        full_multiplicities = tuple(min(left, right) for left, right in endpoints)
+        deficit_ranges = tuple(range(m + 1) for m in full_multiplicities)
+        full_total = sum(full_multiplicities)
+        for deficits in product(*deficit_ranges):
+            partial_multiplicities = tuple(
+                m - h for m, h in zip(full_multiplicities, deficits)
+            )
+            partial_total = sum(partial_multiplicities)
+            total_deficit = sum(deficits)
+            for slack in range(5):
+                n = full_total + slack
+                partial_weight = support_weight(
+                    n, endpoints, partial_multiplicities
+                )
+                full_weight = support_weight(n, endpoints, full_multiplicities)
+                exact_global = Fraction(
+                    falling(n - partial_total, total_deficit), 1
+                )
+                exact_local = Fraction(1, 1)
+                for (left, right), h in zip(endpoints, deficits):
+                    m = min(left, right)
+                    d = abs(left - right)
+                    exact_local *= local_deficit_ratio(m, d, h)
+                expected = exact_global * exact_local
+                if partial_weight / full_weight != expected:
+                    raise AssertionError(
+                        "global ratio failed for "
+                        f"{endpoints}, {deficits}, n={n}"
+                    )
+
+                upper = Fraction(n**total_deficit, 1) * exact_local
+                if partial_weight / full_weight > upper:
+                    raise AssertionError(
+                        "global denominator bound has wrong direction"
+                    )
+                if exact_global == n**total_deficit:
+                    equality_cases += 1
+                checks += 1
+    return {"checks": checks, "upper_bound_equality_cases": equality_cases}
+
+
+def verify_high_deficit_geometric_bound(
+    max_m: int = 120, max_d: int = 3
+) -> int:
+    checks = 0
+    for m in range(2, max_m + 1):
+        for d in range(max_d + 1):
+            for h in range(1, m + 1):
+                if 2 * h >= m:
+                    continue
+                exact = local_deficit_ratio(m, d, h)
+                geometric = Fraction(m, 2 ** floor(2 * m / 3)) ** h
+                if exact > geometric:
+                    raise AssertionError(
+                        f"geometric deficit bound failed for {(m, d, h)}"
+                    )
+                checks += 1
+    return checks
+
+
+def main() -> None:
+    if not __debug__:
+        raise RuntimeError("verification must not be run with python -O")
+
+    result = {
+        "brute_partial_matching_counts": verify_brute_local_counts(),
+        "exact_local_weighted_ratios": verify_local_ratio(),
+        "exact_global_ratio": verify_global_ratio(),
+        "high_deficit_geometric_bounds": verify_high_deficit_geometric_bound(),
+        "status_boundary": (
+            "fixed-support physical-fibre identities checked; "
+            "global attained-skeleton reindexing not claimed"
+        ),
+    }
+    print("Erdos 625 physical-fibre exact-ratio audit: PASS")
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()

From 2356fb2fa3dcc978b140215622751eb3f8663de4 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Mon, 27 Jul 2026 09:05:39 +0300
Subject: [PATCH 3/3] Add physical-fibre exact-ratio workflow

---
 .../erdos625-physical-fibre-exact-ratio.yml   | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 .github/workflows/erdos625-physical-fibre-exact-ratio.yml

diff --git a/.github/workflows/erdos625-physical-fibre-exact-ratio.yml b/.github/workflows/erdos625-physical-fibre-exact-ratio.yml
new file mode 100644
index 00000000..c630e0db
--- /dev/null
+++ b/.github/workflows/erdos625-physical-fibre-exact-ratio.yml
@@ -0,0 +1,31 @@
+name: Erdős 625 physical-fibre exact ratio
+
+on:
+  pull_request:
+    paths:
+      - "625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md"
+      - "625/scripts/verify_physical_fibre_exact_ratio.py"
+      - ".github/workflows/erdos625-physical-fibre-exact-ratio.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  exact-ratio:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Compile verifier
+        run: python -m py_compile 625/scripts/verify_physical_fibre_exact_ratio.py
+      - name: Run exact finite audit
+        run: python 625/scripts/verify_physical_fibre_exact_ratio.py
+      - name: Check theorem and status markers
+        run: |
+          grep -F '(n-J)_H' 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md >/dev/null
+          grep -F 'one-global-denominator' 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md >/dev/null
+          grep -F 'global attained-skeleton reindexing not claimed' 625/scripts/verify_physical_fibre_exact_ratio.py >/dev/null
+          grep -F 'does **not** close the remaining global theorem' 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md >/dev/null