Actual versus medium-only power correction under the same weights
ProvedErdos390.Full.PaperBridgeFit.BridgeData.sum_abs_actual_powerCorrection_sub_physicalMedium_le_compactanalytic-number-theoryerdos-390erdos390-source-construction
For a valuation law , put . Let have nonempty head set and , and fix a tilt parameter . Suppose positive cell densities obey . Let bound, respectively, every effective prime coefficient, the physical tilt coordinate, the absolute physical score, and each reciprocal-event constant
Assume . Then
The reference removes only the residual physical score, retaining the actual reweighted component probabilities.
This compact declaration is definitionally identical to the original fully quantified statement; the named proposition preserves every hypothesis.
Preamble
import Definitions.Def_erdos390_analytic_compact_goals_003 universe u_1 u_2
Formal statement
theorem Erdos390.Full.PaperBridgeFit.BridgeData.sum_abs_actual_powerCorrection_sub_physicalMedium_le_compact : Erdos390.AnalyticCompactBatch003Goal001.{u_1, u_2} := by sorrySource