Prove and exhaustively audit the fixed-support physical-fibre ratio

[SamPetkov]

Purpose

This is a mathematical and executable follow-up stacked on reader-first PR #47. It isolates the exact finite identity used after the high block support and its multiplicities have been fixed.

It does not modify the frozen canonical manuscript, claim the remaining attained-skeleton reindexing, or promote Proposition 9.2 or Erdos625Statement.

Main mathematical improvement

For a fixed support matching P, write

m_e = min(s_e,t_e),
j_e = m_e-h_e,
J   = sum_e j_e,
H   = sum_e h_e.

Let w(P,j) be the aggregate physical partial-matching weight with one global denominator (n)_J. The PR proves the exact identity

w(P,m-h) / w(P,m)
  = (n-J)_H * product_e R_{m_e,d_e}(h_e),

where

R_{m,d}(h)
  = C(m,h)/((d+1)...(d+h))
    * 2^(-hm+h(h+1)/2).

The earlier comparison follows immediately:

w(P,m-h) / w(P,m)
  <= product_e n^(h_e) R_{m_e,d_e}(h_e).

This makes the single global finite-population denominator explicit rather than interleaving it with the local fibre algebra.

Local fibre theorem

A literal size-j partial matching between labelled blocks of sizes s,t has cardinality

C(s,j) C(t,j) j! = (s)_j (t)_j / j!.

Multiplying by the exact cell factor g(j)=2^(C(j,2)-1) gives the displayed R_{m,d}(h) ratio.

Under the canonical high condition 2h<m, the same proof gives

R_{m,d}(h)
  <= (m / 2^floor(2m/3))^h,

which is the finite input for the geometric all-deficit sum.

Files

• 625/proofs/PHYSICAL_FIBRE_EXACT_RATIO.md
• 625/scripts/verify_physical_fibre_exact_ratio.py
• .github/workflows/erdos625-physical-fibre-exact-ratio.yml

Exact finite audit

The standard-library verifier uses exact integers and fractions.Fraction. It checks:

• 140 brute-force enumerations of literal partial bijections 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 high-deficit geometric inequalities;
• the direction of (n-J)_H <= n^H.

The deterministic local run passed. The PR workflow compiles and reruns the audit.

What this closes

For every fixed support and fixed multiplicity vector, the PR gives:

1. the exact physical fibre cardinality;
2. the exact local weighted deficit ratio;
3. the exact global denominator ratio;
4. the product upper bound used in the all-deficit summation.

What remains open

The submission-blocking seam remains:

attained canonical high skeleton
  <-> block support + admissible deficits + local partial physical matchings

with a disjoint global reindexing and exact aggregate weight preservation. This PR starts after those data are fixed and deliberately prints:

fixed-support physical-fibre identities checked;
global attained-skeleton reindexing not claimed

Readability gain

The eventual Section VIII proof can be reduced to three steps:

1. global reindexing of attained skeletons;
2. the exact boxed ratio from this PR;
3. geometric deficit summation plus endpoint transport.

This removes repeated local factorial manipulations and makes it impossible to introduce one ambient denominator per cell.

Review focus

Please check:

• the partial-bijection count;
• the cancellation giving the local binomial/rising-factorial ratio;
• the cell-factor exponent -hm+h(h+1)/2;
• the exact identity (n)_(J+H)/(n)_J=(n-J)_H;
• the finite proof of the floor(2m/3) geometric majorant;
• the stated boundary between fixed-support counting and the unresolved global reindexing.

[SamPetkov]

Dedicated validation is green on head 2356fb2: Actions run 30241720613 compiled and executed the exact Fraction-based audit. It passed 140 brute partial-matching counts, 1,296 local weighted-ratio identities, 580 multi-cell one-global-denominator identities, and 14,160 high-deficit geometric bounds. The workflow also enforces the explicit statement that the global attained-skeleton reindexing is not claimed here.