Simplify Section 8 through a direct half-deficit product assembly

[SamPetkov]

Purpose

This PR replaces the remaining near/middle bookkeeping in Section VIII by a direct, completion-free support/deficit product. It is stacked on PR #53, which identifies every attained matching-supported high-skeleton weight with its exact product of local partial-cell fibres.

The central simplification is to enlarge the exact high-deficit set to the local envelope

0 < h,  2h < m.

Every attained high cell already satisfies this condition. Since all summands are nonnegative, the enlargement is valid for an upper bound and removes the global cutoff U/2 from the finite analytic assembly.

1. Direct optional-choice encoding

Zero deficit is represented by none; a positive deficit satisfying 2h<m is represented by some h. Attained demands are encoded directly into the same NearSkeletonChoice type used by the finite product theorem.

Main declarations:

fourEndpointHalfDeficitAllowed
FourEndpointSupportChoiceData
fourEndpointSupportChoiceTable
fourEndpointDemandSupportChoiceEncoding
fourEndpointDemandSupportChoiceEncoding_injective
sum_fourEndpointSupportChoiceChargedWeight_eq
sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct

The decoder recovers the exact attained demand table. The encoding is injective and introduces no extra deficit-vector multiplicity.

2. Exact one-cell physical ratio

Section8ExactLocalDeficitRatio.lean proves the division-free identity for endpoint sizes m and m+d:

weightedCount(m,m+d,m-h)
  * product_(t=1)^h (d+t)
  * 2^(h*m-h*(h+1)/2)
=
weightedCount(m,m+d,m) * choose(m,h).

The proof separates the physical matching-count quotient from the exact local signed-reward quotient. No probability or asymptotic estimate enters.

Section8ExactLocalDeficitENNReal.lean performs only cancellation by explicitly positive finite factors and identifies

nearCellTerm(n,m,d,h)
  = n^h * exactLocalDeficitRatio(m,d,h).

Thus the charged cell identity is exact, before the later three-quarter majorant is applied.

3. Symmetric endpoint bridge

Section8SymmetricLocalDeficitRatio.lean removes orientation choices. For arbitrary endpoint sizes u,v, it uses

m = min(u,v),
d = Nat.dist(u,v),

and proves the same exact charged identity. The global proof therefore does not require sixteen endpoint-orientation cases.

4. One global falling-factorial loss

Section8PointwiseChargeProduct.lean isolates the two independent inputs:

1. one exact partial/full local ratio per selected cell;
2. one ambient falling-factorial comparison, paid once.

It proves

1/(n)_(J-H) <= n^H/(n)_J

and packages the resulting product comparison without redistributing this global loss cell by cell.

5. Coarse three-quarter charge

For one endpoint cell define

rho(n,m) = n*m / 2^floor((3m-1)/4).

The checked arithmetic gives

nearCellTerm(n,m,d,h) <= rho(n,m)^h

under 2h<m, independently of endpoint distance d.

The coarse public finite wrapper deliberately permits the harmless bound

(1 + (alpha+1)*rho)^|P|.

A sharper table-preserving geometric sum can be added separately without changing this finite infrastructure.

6. Support products and exact references

Section8SupportProductGrouping.lean proves the generic identities

product_(edge in P) f(type(edge))
  = product_(i,j) f(i,j)^(P.typeTable i j),

sum_(edge in P) f(type(edge))
  = sum_(i,j) P.typeTable i j • f(i,j).

It also identifies the support full multiplicity with fourEndpointJ of the support table and rewrites the literal zero-deficit reference as

product_(edge in P) fullWeightedCell(edge)
  / (n)_(full support multiplicity).

No additional physical completion or factorial enumeration is introduced.

7. Finite realized-table grouping

The type of all natural-valued four-by-four tables is infinite and is not used as a finite summation index. The PR defines the finite image of actually realized support tables and proves

sum_P fullSupportReference(P)
  = sum_(realized L) W(L).

The final coarse endpoint is

sum_D weight(D)
  <= [sum_(realized L) W(L)]
       * [1 + (alpha+1)*rho_16]^K,

conditional on one pointwise charged comparison. Support-cardinality control, local deficit summation, common-base domination, and finite reference regrouping are discharged internally.

8. Exact regression

625/experiments/section8_direct_half_deficit_assembly.py checks with exact integer and Fraction arithmetic:

• inclusion of the exact high window in 2h<m;
• injectivity of deficit decoding;
• the optional-choice product identity;
• exact one-cell partial/full ratios;
• exact multi-cell aggregate ratios;
• the single global (n)_J/(n)_(J-H) <= n^H loss;
• complete charged comparisons on small supports;
• the three-quarter local majorant.

The regression passes under ordinary and optimized Python, including 1,664 exact one-cell ratios and 500 aggregate charged comparisons.

Validation

Current head:

094dfcc6168378c0807557f76268021cc2a5d283

Successful dedicated runs:

Erdős 625 direct half-deficit assembly: 30563233183
Erdős 625 Section 8 physical-fibre closure: 30563233170

Both exact-regression jobs pass. The dedicated warning-fatal Lean build passes for:

Section8PointwiseChargeProduct
Section8ExactLocalDeficitRatio
Section8ExactLocalDeficitENNReal
Section8SymmetricLocalDeficitRatio
Section8SupportProductGrouping
Section8CanonicalThreeQuarterRho
Section8CoarsePhaseCorridor
Section8FiniteBareSkeletonReduction

The changed-source scan rejects sorry, admit, sorryAx, project-defined axioms, unsafe, and related placeholders. The repository-wide self-contained Lean workflow is also running on this head; its generated-source freshness check has passed.

Scope boundary

This PR does not assert Lemma 8.3, Proposition 9.2, or Erdos625Statement.

The exact remaining public seam is to instantiate the finite wrappers with a fully proved pointwise attained-demand charge and then prove the table-preserving support sum and endpoint transportation/asymptotic estimates. The present PR supplies the local exact algebra, the one-global-loss interface, support-product grouping, and both exact and coarse finite summation infrastructure.

[SamPetkov]

Validation update on head 094dfcc6168378c0807557f76268021cc2a5d283: all three relevant workflows are now green.

• repository-wide Lean run 30563233185: success, including self-contained freshness and warning-fatal replay;
• Erdős 625 Section 8 physical-fibre closure run 30563233170: success;
• Erdős 625 direct half-deficit assembly run 30563233183: success.

The exact finite regression, placeholder/project-axiom scans, focused modules, physical-fibre chain, and repository-wide generated standalone all pass. This validates the public PR #55 modules as candidate inputs; it does not by itself prove Lemma 8.3, Proposition 9.2, or Erdos625Statement.