RegularCarrier
plain-language theorem explainer
RegularCarrier packages a positive bound on the logarithmic derivative together with a positive radius to certify a holomorphic nonvanishing function on a disk inside the annular J-cost setting. Researchers on Euler product instantiations and cost-covering bridges cite the structure to interface analytic carriers with topological cost bounds. The declaration is a plain structure definition with four fields and no computational content.
Claim. A regular carrier on a disk consists of a real number $b > 0$ (bound on the logarithmic derivative) and a real number $r > 0$ (radius of the disk).
background
In the Annular J-Cost Framework the weighted cost is phiCost u := cosh((log φ)·u) − 1, which equals J(φ^u) with J the Recognition Science cost function. Annular samples record phase increments on concentric rings; Jensen coercivity shows nonzero winding forces Θ(m² log N) cost. Holomorphic nonvanishing carriers then imply O(R²) annular cost, supplying the budget interface for the topological cost-covering bridge.
proof idea
Structure definition that directly encodes the two real parameters with their positivity conditions. No lemmas are applied; the declaration serves as the interface type for budgeted carriers and Euler instantiations.
why it matters
BudgetedCarrier extends RegularCarrier by adding an explicit excess-budget witness along a zero-charge annular trace, yielding the realizable interface for mesh-independent claims. The structure feeds eulerCarrierInstance and EulerInstantiationCert, which close the chain from Euler product through nonvanishing and bounded derivative to the abstract EulerCarrier interface. It realizes the carrier-budget step of the annular cost-covering bridge, linking holomorphic data to the phi-ladder and J-cost properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.