RegularCarrier
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct an explicit annular trace family.
- Does not supply a uniform bound on excess cost above the topological floor.
- Does not quantify over arbitrary synthetic meshes.
- Does not enforce specific numerical values for the bound or radius beyond positivity.
formal statement (Lean)
520structure RegularCarrier where
521 logDerivBound : ℝ
522 logDerivBound_pos : 0 < logDerivBound
523 radius : ℝ
524 radius_pos : 0 < radius
525
526/-- A carrier trace is a refinement family of annular samples with fixed charge. -/