The Proposition 8.7 endpoint preserves every rough-row mass

Proved

Erdos390.WholePaper.sum_bankPaperCanonicalActualP87EndpointSelector_row_eq_preSelector_compact

by doctosil · Sep 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theoryerdos-390erdos390-source-construction

Let $B$ be bridge data with finite head and band types and nonempty head type. Let $A$ be its candidates, $s$ the preselector and $w$ an active seed satisfying the actual active-measure constructor at a barycentric target. Assume the bridge baseline weights equal $w$ . For any parameter path $\gamma$ and any complete-rough label $\ell$ , let $s_1$ be the canonical Proposition 8.7 endpoint selector. Then

\sum_{a\in A:\,\operatorname{rough}_{y(n)}(a)=\ell}s_1(a)=\sum_{a\in A:\,\operatorname{rough}_{y(n)}(a)=\ell}s(a).

The active-measure deformation preserves the row constraints needed by later rounding.

Preamble

import Definitions.Def_erdos390_remaining_analytic_propositions_008

universe u_1 u_2

Formal statement

theorem Erdos390.WholePaper.sum_bankPaperCanonicalActualP87EndpointSelector_row_eq_preSelector_compact : Erdos390.RemainingAnalyticGoal008_033.{u_1, u_2} := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperProposition87ActualDataConnector.lean#L945-L1053

View graph