Kernel-check the exact Section 8 decorated endpoint reference weight

[SamPetkov]

Purpose

This is the final closure-focused stacked PR above cumulative audit PR #39. It closes the exact full-endpoint normalization seam in Section VIII rather than adding a new proof direction.

The base is agent/625-full-proof-audit-frontier; review PR #39 first. The branch also synchronizes the green q-only normalized-second-moment frontier from that base.

Exact endpoint result

For one four-type full endpoint table L, the repository had already formalized separately:

1. selection and pairing of row and column blocks, with the single table-cell factorial quotient;
2. selection and bijective matching of the physical stubs inside every selected full endpoint cell.

This PR first combines their cross-multiplied cardinality identities:

card(decorated block pairings)
  * (cell-table factorials * cell-stub factorials)
=
(row block selections * column block selections)
  * cell-stub selections.

It then attaches the common full-cell signed reward and ambient falling-factorial normalization. Because unrestricted product-of-quotients cancellation is invalid in ENNReal, the local algebra is proved in cross-multiplied form and only positive finite natural-factorial casts are cancelled.

The final kernel-checked theorem is

sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW

which states that summing over every block pairing and every full-cell physical stub matching with table L gives exactly

fourEndpointW n alpha hAlpha k L.

Thus there is no missing symmetry factor and no duplicated factorial in the full-endpoint reference family.

Formal files

• 625/formalization/Erdos625/Section8EndpointDecoratedReferenceQuotient.lean
• 625/formalization/Erdos625/Section8EndpointDecoratedReferenceWeight.lean
• 625/formalization/Erdos625/Section8EndpointDecoratedReferenceIdentification.lean
• 625/formalization/SECTION8_DECORATED_REFERENCE_QUOTIENT_AUDIT.md
• .github/workflows/erdos625-section8-decorated-reference-quotient.yml

Public theorem chain

1. card_fourEndpointDecoratedBlockPairing_mul_denominator combines the block-pairing and local-stub cardinalities without division.
2. ennreal_card_fourEndpointDecoratedBlockPairing_eq_quotient divides only after proving the denominator nonzero and finite.
3. sum_fourEndpointDecoratedReferenceAtomWeight_eq_quotientWeight attaches the common reward and ambient factor.
4. fourEndpointLocalProduct_mul_stubFactorialProduct proves the local product identity in cross-multiplied form.
5. fourEndpointLocalProduct_eq_stubQuotient_mul_reward performs the justified cancellation.
6. sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW identifies the literal decorated sum with the manuscript reference weight.

Remaining Section VIII boundary

The endpoint factorial calculation is now closed. The repository already contains

fourEndpointDecoratedBlockPairingToPhysicalFibre

and proves that its output is endpoint-only, block-matching, and has the prescribed table. The remaining finite endpoint theorem is the reverse construction and the two round trips, or an equivalent weighted injectivity/surjectivity result identifying the decorated family with FourEndpointPhysicalFibre.

After that, the decisive nonendpoint theorem is the aggregate deficit reindexing: every attained canonical high physical skeleton must be summed over its endpoint block support, one allowed multiplicity deficit per selected cell, and the corresponding partial stub-matching fibre. The exact one-cell ratio and product majorant are already in the cumulative stack.

Literature update

The PR adds 625/audits/LITERATURE_UPDATE_2026-07-25.md and updates both bibliography files. The search found several relevant antecedents missing from the current background:

• Lesniak--Straight (1977), the origin paper for the cochromatic number;
• Erdős--Gimbel--Straight (1990) and Erdős--Gimbel--Kratsch (1991), foundational comparison/extremal papers;
• Scheinerman (1992), the Theta(n/log n) generalized-hereditary-coloring framework;
• Bollobás--Thomason (1995), the sharper exact first-order generalized chromatic asymptotic;
• Gimbel--Kündgen--Molloy (2022), fractional cocoloring as adjacent work;
• Steiner's final 2025 SIAM journal publication details.

The audit also records the informal two-independent-graph reduction on the Erdős Problems forum, but does not treat it as a published theorem, and cautions against a novelty claim for the elementary generic restriction-product lemma without a dedicated coding/matroid literature review.

Validation

The focused workflow on commit f5e72950800131f847d48953be2a8a4b134e47b4 passed all gates:

• placeholder/project-axiom rejection;
• bibliography key and brace checks;
• complete dependency build of Section8EndpointDecoratedReferenceIdentification under Lean 4.31 and --wfail.

PR #39's exact regression, focused Section VIII, focused Section IX frontier, and root Lean build are also green on its current head.

This PR remains draft because it does not yet prove the physical-fibre equivalence, the global deficit reindexing, Lemma 8.3, Proposition 9.2, or Erdos625Statement.