Identify attained high-skeleton weights with exact partial-cell fibres

[SamPetkov]

Purpose

This PR attacks the unique independent blocker isolated by the literal TeX audit in PR #52. It replaces the noncanonical “complete each cell and delete deficits” picture by a literal finite equivalence and then proves the missing pointwise bare-weight identity.

It is stacked on PR #49 and therefore already contains:

• the attained-demand support/deficit injection from PR Reindex attained high demands by block support and bounded deficits #48;
• the endpoint physical equivalence and exact partial-cell cardinalities from PR Close the Section 8 physical-fibre and all-deficit seam #45;
• the sharp cellwise all-deficit product and three-quarter exponent budget from PR Sharpen and simplify the Section 8 all-deficit partition function #49.

1. Completion-free physical-fibre equivalence

625/formalization/Erdos625/Section8MatchingDemandCellFibre.lean defines

MatchingDemandCellDecoration demand row col

as one literal SingleCellStubMatching for every positive cell of a demand table. Under the sole structural hypothesis

IsBipartiteMatching (positiveDemandSupport demand),

it proves the exact finite equivalence

matchingDemandCellDecorationEquivPhysicalFibre :
  MatchingDemandCellDecoration demand row col
    ≃
  {S : UnlabelledTypedSkeleton row col // S.typeTable = demand}.

The forward map unions the local physical edges. The reverse map filters a global physical skeleton into its positive type cells. The two round trips are proved directly.

No full-cell completion is selected or counted. This is the aggregate theorem missing from the canonical “complete, distinguish, and forget” prose.

Main declarations

matchingDemandPhysicalEdgeOfLocalEdge_injective
matchingDemandDecoratedPhysicalSkeleton_typeTable
matchingDemandCellDecorationToPhysicalFibre_injective
matchingDemandPhysicalCellLocalSkeleton_typeTable
matchingDemandCellDecorationToPhysicalFibre_rightInverse
matchingDemandCellDecorationToPhysicalFibre_leftInverse
matchingDemandCellDecorationEquivPhysicalFibre

2. Exact local-cell product cardinality

625/formalization/Erdos625/Section8ProfilePartialAggregateWeight.lean proves the cross-multiplied formula

card_matchingDemandCellDecoration_mul_factorials

which says

card(local cell-decoration product)
  * product_e demand(e)!
=
product_e (row(e.1))_{demand(e)} (col(e.2))_{demand(e)}.

The denominator is proved nonzero before division, yielding

ennreal_card_matchingDemandCellDecoration_eq_quotient.

Thus there is exactly one local factorial denominator for every positive cell and no additional completion multiplicity.

3. Pointwise profile high-skeleton weight identity

The central theorem is now kernel-checked:

profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight

For one matching-supported attained canonical high demand, it proves

profileHighSkeletonWeight k U demand
  =
matchingDemandCellAggregateWeight
  demand.1
  (profileBlockMargin k)
  (profileBlockMargin k)
  (profileHighSkeletonWitnessWeight k U demand).

Equivalently, if j_e = demand(e) and J = sum_e j_e, then the exact bare weight is

[product_e (s_e)_{j_e}(t_e)_{j_e}/j_e!]
  * [canonical local reward/(n)_J].

The cap-specialized theorem

profileHighSkeletonWeight_eq_matchingDemandCellAggregateWeight_of_cap

automatically obtains matchingness from the canonical high-cell condition and the profile degree cap.

This closes the pointwise aggregate physical-fibre ambiguity identified in Lemma 8.3 of the TeX audit.

4. Exact finite regression

625/experiments/section8_attained_partial_weight_identity.py checks with integer and Fraction arithmetic that, for a large family of small matching-supported demands:

1. the global prescribed-demand physical-fibre cardinality equals the product of the one-cell cardinalities;
2. the corresponding reward/incidence aggregate weights agree exactly;
3. a deliberately nonmatching support fails the independent-cell product, confirming that matchingness is essential.

The script passes under ordinary Python and python -O.

5. Reader-facing audit note

625/proofs/SECTION8_ATTAINED_PARTIAL_WEIGHT_IDENTIFICATION.md explains:

• why objectwise full completion is the wrong proof object;
• the completion-free finite equivalence;
• the exact cardinality and weight formulas;
• the four-endpoint specialization still needed to connect directly to the support/deficit partition function.

Validation

The dedicated workflow is fully green on

0badcf2d63e8b21b7b4400024189b5aa44fa947a

with workflow run

30257733509.

Passed gates:

• placeholder/project-axiom/unsafe rejection;
• complete Lean 4.31 dependency build of Section8ProfilePartialAggregateWeight under --wfail;
• both physical-fibre round trips;
• exact local cardinality quotient;
• pointwise profile high-skeleton weight identity;
• exact regression under ordinary and optimized Python.

The new public theorems report only the standard logical foundations already used throughout the project (propext, Classical.choice, and Quot.sound); there is no sorryAx.

Remaining Section VIII boundary

This PR closes the aggregate physical-fibre and pointwise profile-weight seam. It does not yet prove the global bare-skeleton estimate.

The remaining composition is now narrower:

1. specialize the generic aggregate to PR Reindex attained high demands by block support and bounded deficits #48’s four-endpoint block support and deficit vector;
2. rewrite each selected multiplicity as m_e - h_e;
3. apply the single global (n-J)_H ≤ n^H comparison;
4. use PR Sharpen and simplify the Section 8 all-deficit partition function #49’s complete cellwise deficit partition function;
5. group the zero-deficit references by endpoint table and apply endpoint transportation;
6. compose with the q-only Section IX frontier to export Proposition 9.2.

PR #53 remains draft because those global summation steps, Proposition 9.2, and Erdos625Statement are not yet proved.