Fixed numerical rich sources have mesh-independent scalar data

Proved

Erdos390.WholePaper.BankPaperRealization.eventually_bankPaperCanonicalSectionNinePostHeight_fixedRichSource_crossMeshScalarTransport

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

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

Let $M_0,M_1$ be any two regular meshes with positive lower parameters. Suppose they carry fixed-rich-source witnesses for exactly the same numerical parameters $c,\delta_*,\beta_{\rm prot},\beta_{\rm act}$ , source-cell margin, depth, tail threshold, cutoff, rough level, exponent, and guarded tail family $F$ . At each source use its prescribed balanced alpha and the common extended guarded smooth base mass from $F$ . Eventually, for every proof that the ambient index exceeds the tail threshold,

m_{\rm frozen}^{(0)}=m_{\rm frozen}^{(1)},\qquad\mathrm{logY}^{(0)}=\mathrm{logY}^{(1)},\qquad\Lambda_{0,\rm rounded}^{(0)}=\Lambda_{0,\rm rounded}^{(1)}.

The theorem compares local formulas directly, enabling a scalar ledger chosen on one mesh to be reused on another.

Preamble

import Mathlib
import Definitions.Def_erdos390_source_bank_interface
import Definitions.Def_erdos390_dickman_step_function
import Theorems.Thm_MediumPNT
import Definitions.Def_erdos390_analytic_foundations_001
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_product_bound
import Theorems.Thm_Erdos390_Full_DickmanBasic_rho_pos_on_zero_five
import Theorems.Thm_Erdos390_Full_DickmanBasic_kernel_secondDerivative_first_bound
import Definitions.Def_erdos390_analytic_foundations_002
import Definitions.Def_erdos390_analytic_foundations_003
import Definitions.Def_erdos390_analytic_foundations_005
import Definitions.Def_erdos390_analytic_foundations_006
import Definitions.Def_erdos390_analytic_foundations_007
import Definitions.Def_erdos390_analytic_foundations_008
import Definitions.Def_erdos390_analytic_foundations_009
import Definitions.Def_erdos390_analytic_foundations_010

Formal statement

theorem Erdos390.WholePaper.BankPaperRealization.eventually_bankPaperCanonicalSectionNinePostHeight_fixedRichSource_crossMeshScalarTransport :
∀ {delta₀ eta₀ delta₁ eta₁ : Real} (M₀ : Erdos390.Full.RegularRelativeMesh.Mesh delta₀ eta₀) (M₁ : Erdos390.Full.RegularRelativeMesh.Mesh delta₁ eta₁) {c deltaStar betaProt betaAct sourceCellMargin : Real} {depth N W K0 E : Nat} (hdelta₀ : @LT.lt.{0} Real _ (@OfNat.ofNat.{0} Real (nat_lit 0) _) delta₀) (hdelta₁ : @LT.lt.{0} Real _ (@OfNat.ofNat.{0} Real (nat_lit 0) _) delta₁) (F : Erdos390.WholePaper.BankPaperCanonicalGuardedTailFamily c depth N) (X₀ : @Erdos390.WholePaper.BankPaperRealization.BankPaperCanonicalSectionNinePostHeightFixedRichSourceWitness delta₀ eta₀ M₀ c deltaStar betaProt betaAct sourceCellMargin depth N W K0 E hdelta₀ F) (X₁ : @Erdos390.WholePaper.BankPaperRealization.BankPaperCanonicalSectionNinePostHeightFixedRichSourceWitness delta₁ eta₁ M₁ c deltaStar betaProt betaAct sourceCellMargin depth N W K0 E hdelta₁ F),
  @Filter.Eventually.{0} Nat
    (fun (n : Nat) =>
      ∀ (hn : @LE.le.{0} Nat _ N n),
        let Y₀ := @Erdos390.WholePaper.BankPaperRealization.BankPaperCanonicalSectionNinePostHeightFixedRichSourceWitness.source delta₀ eta₀ M₀ c deltaStar betaProt betaAct sourceCellMargin depth N W K0 E hdelta₀ F X₀ n hn;
        let Y₁ := @Erdos390.WholePaper.BankPaperRealization.BankPaperCanonicalSectionNinePostHeightFixedRichSourceWitness.source delta₁ eta₁ M₁ c deltaStar betaProt betaAct sourceCellMargin depth N W K0 E hdelta₁ F X₁ n hn;
        let B₀ := @Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀;
        let B₁ := @Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁;
        let R₀ := @Sigma.fst.{0, 0} (Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))))) (fun (R : Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))))) => Erdos390.WholePaper.GuardedCentralAnchorCertificate c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardLeftCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardRightCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R) (@Erdos390.WholePaper.BankPaperRealization.centralChangedMarkers (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R depth)) (@Prod.fst.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀));
        let R₁ := @Sigma.fst.{0, 0} (Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))))) (fun (R : Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))))) => Erdos390.WholePaper.GuardedCentralAnchorCertificate c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardLeftCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardRightCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R) (@Erdos390.WholePaper.BankPaperRealization.centralChangedMarkers (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R depth)) (@Prod.fst.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁));
        let certificate₀ := @Sigma.snd.{0, 0} (Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))))) (fun (R : Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))))) => Erdos390.WholePaper.GuardedCentralAnchorCertificate c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardLeftCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardRightCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R) (@Erdos390.WholePaper.BankPaperRealization.centralChangedMarkers (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))))) R depth)) (@Prod.fst.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀));
        let certificate₁ := @Sigma.snd.{0, 0} (Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))))) (fun (R : Erdos390.WholePaper.BankPaperRealization (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))))) => Erdos390.WholePaper.GuardedCentralAnchorCertificate c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardLeftCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R) (@Erdos390.WholePaper.BankPaperRealization.anchorGuardRightCore (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R) (@Erdos390.WholePaper.BankPaperRealization.centralChangedMarkers (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperEndpoint (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (Erdos390.WholePaper.upperTailLength c (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))))) R depth)) (@Prod.fst.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁));
        let T₀ := @Prod.snd.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B))) Y₀);
        let T₁ := @Prod.snd.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁)))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ (@Sigma.fst.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁))) (@Sigma.snd.{0, 0} (@Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) (fun (B : @Erdos390.Full.PaperBridgeFit.BridgeData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _) => Prod.{0, 0} (Erdos390.WholePaper.BankPaperCanonicalGuardedTailFiber c depth (@Erdos390.Full.PaperBridgeFit.StructuredSampleData.n.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) (@Erdos390.Full.PaperGuardCensus.BarycentricTarget.{0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) _ (@Erdos390.Full.PaperBridgeFit.BridgeData.sampleData.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B))) Y₁);
        let alpha₀ := @Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalPostHfitBalancedAlpha.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ _ _ B₀ c K0 betaProt betaAct;
        let alpha₁ := @Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalPostHfitBalancedAlpha.{0, 0} (Erdos390.Full.PaperHeadSimplex.Tag (Erdos390.WholePaper.primesUpTo W)) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ _ _ B₁ c K0 betaProt betaAct;
        let qTilde := @Erdos390.WholePaper.BankPaperCanonicalGuardedTailFamily.extendedGuardedSmoothBaseMass c depth N F W (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat _ K0 (@OfNat.ofNat.{0} Nat (nat_lit 1) _)) betaAct deltaStar n;
        And (@Eq.{1} Real (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalTopFrozenSmoothFrozenMass.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ B₀ c depth (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat _ K0 (@OfNat.ofNat.{0} Nat (nat_lit 1) _)) R₀ certificate₀ deltaStar betaProt alpha₀) (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalTopFrozenSmoothFrozenMass.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ B₁ c depth (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat _ K0 (@OfNat.ofNat.{0} Nat (nat_lit 1) _)) R₁ certificate₁ deltaStar betaProt alpha₁)) (And (@Eq.{1} Real (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNinePostHeightLogY.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ B₀ c depth R₀ certificate₀) (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNinePostHeightLogY.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ B₁ c depth R₁ certificate₁)) (@Eq.{1} Real (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNinePostHeightRoundedLambda0.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₀ eta₀ M₀) _ _ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat _ K0 (@OfNat.ofNat.{0} Nat (nat_lit 1) _)) B₀ c depth R₀ certificate₀ T₀ deltaStar betaProt alpha₀ (@HAdd.hAdd.{0, 0, 0} Real Real Real _ betaProt betaAct) qTilde) (@Erdos390.WholePaper.BankPaperRealization.bankPaperCanonicalSectionNinePostHeightRoundedLambda0.{0} (Erdos390.WholePaper.primesUpTo W) (@Erdos390.WholePaper.BankPaperCanonicalExponentBand delta₁ eta₁ M₁) _ _ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat _ K0 (@OfNat.ofNat.{0} Nat (nat_lit 1) _)) B₁ c depth R₁ certificate₁ T₁ deltaStar betaProt alpha₁ (@HAdd.hAdd.{0, 0, 0} Real Real Real _ betaProt betaAct) qTilde))))
    (@Filter.atTop.{0} Nat _) := by sorry

Source

https://github.com/ShouqiaoW/erdos/blob/61325b10bbdc29f4fb5e0618b414b9f2189333ad/390/lean/Erdos390/WholePaper/BankPaperCanonicalSectionNinePostHeightSourceFirstCrossMeshScalarTransport.lean#L353-L678

View graph