Uniform raw reference inputs for non-step prime-power rows
ProvedErdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_nonstepPower_inputs_compactanalytic-number-theoryerdos-390erdos390-source-construction
Fix a finite nonempty head family, physical intervals with lower endpoints at least 1 and upper endpoints at most Cmax, and a guard ledger. The box-independent prime-power constant Cpow is positive. For W>1 containing all head primes and nonnegative coefficient and physical tilt bounds, there exists a nonnegative sequence ε₇₅ tending to zero, with ε₇₅ log L tending to zero. The canonical non-step correction ρ also satisfies ρ log L→0. Beyond one threshold, uniformly over finite band types, canonical guarded bridges and allowed tilts, the canonical raw medium reference law satisfies PrimePowerTransferBounds(Cpow,ε₇₅), and the actual/reference prime-power covariance differences satisfy the displayed weighted row estimate.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_001 universe u_1 u_2
Formal statement
theorem Erdos390.Full.PaperBridgeFit.BridgeData.boxIndependent_canonicalRaw_nonstepPower_inputs_compact : Erdos390.RemainingAnalyticGoal001_008.{u_1, u_2} := by sorrySource