Reindex attained high demands by block support and bounded deficits

[SamPetkov]

Purpose

This is the next closure-focused PR stacked on PR #45. It formalizes the exact finite statement that an attained canonical high-demand table is determined without multiplicity by:

block-level matching support + one admissible high deficit per selected cell.

The base branch already contains the endpoint decorated/physical equivalence, the literal partial-cell fibre, the attained-demand block support, and the four-deficit profile-cover adapter.

Main finite data type

For one four-endpoint profile, the PR defines the finite sigma type

FourEndpointSupportDeficitData

whose elements consist of:

1. an abstract block-level UnlabelledTypedSkeleton between the four endpoint slot families;
2. for every selected edge e, a bounded deficit h_e satisfying

   2 h_e < m_e,
   m_e = min(s_e,t_e).
   

Zero deficit is included and represents full containment.

Exact encoding and decoding

The PR defines:

fourEndpointDemandSupportDeficitEncoding
fourEndpointSupportDeficitTable
fourEndpointAbstractDemandTable

and proves the target equality

decode (encode demand) = abstractDemandTable demand.

The proof uses the checked reconstruction

m_e - (m_e - j_e) = j_e

on support cells and the exact positive-support equivalence to prove that all off-support cells decode to zero.

Injectivity and finite sum domination

The main declarations are intended to prove:

fourEndpointAbstractDemandTable_injective
fourEndpointDemandSupportDeficitEncoding_injective
sum_profileCanonicalHighSkeleton_le_sum_supportDeficitData

The final theorem says that any pointwise bound on the encoded demand weights may be summed over the full finite support/deficit family with no additional fibre multiplicity. This is the exact combinatorial seam required before inserting the aggregate local weight and geometric all-deficit estimate.

Files

• 625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean

The focused workflow is inherited from PR #45 and automatically builds this module warning-fatally, rejects placeholders/project axioms, and reruns the exact finite regression.

Scope boundary

This PR is draft until the exact target is green. It does not yet prove the pointwise equality between profileHighSkeletonWeight and the aggregate partial-cell weight, the full bare-skeleton estimate, Proposition 9.2, or Erdos625Statement.