pith. machine review for the scientific record. sign in
def definition def or abbrev high

annularCost

show as:
view Lean formalization →

Annular cost aggregates the phi-weighted ring costs across N concentric rings sharing a uniform integer winding charge. Researchers on the RS topological cost-covering bridge cite it when deriving divergence bounds for nonzero-charge defects. The definition is realized by direct summation over the mesh rings, which immediately transfers convexity and nonnegativity from the underlying ringCost.

claimLet $N$ be a natural number and let $M$ be an annular mesh of $N$ rings with integer charge $m$. The annular cost is defined by $C(M) := {}_{n=0}^{N-1} r_n$, where $r_n$ denotes the ring cost of the $n$-th ring sample in $M$.

background

The Annular J-Cost Framework supplies the phi-weighted cost function phiCost u := cosh((log phi) u) - 1 = J(phi^u) together with annular sampling machinery for the RS topological cost-covering bridge. AnnularMesh is the structure consisting of N concentric rings, each an AnnularRingSample, a shared integer charge, and the uniform-winding axiom that every ring carries the same winding number m. Upstream results include PhiForcingDerived.of supplying the J-cost definition and PrimitiveDistinction.from reducing the seven axioms to four structural conditions plus three definitional facts.

proof idea

The declaration is a direct definition that sums ringCost over the Fin N rings of the mesh. No lemmas or tactics are applied; the body is the summation expression itself.

why it matters in Recognition Science

This definition supplies the central quantity for the annular coercivity theorem, which establishes annularCost mesh >= (pi^2 kappa / 4) m^2 sum_{n=1}^N 1/n for m != 0, and for the excess decomposition annularExcess. It feeds the carrier-budget comparison theorems that separate topological floor from excess cost. The object realizes the Jensen coercivity step in the annular layer, linking directly to the phi-ladder and the eight-tick octave in the T0-T8 forcing chain.

scope and limits

formal statement (Lean)

 315noncomputable def annularCost {N : ℕ} (mesh : AnnularMesh N) : ℝ :=

proof body

Definition body.

 316  ∑ n, ringCost (mesh.rings n)
 317
 318/-! ### §3. Jensen coercivity -/
 319
 320/-- Jensen bound for phiCost on a single ring:
 321    ∑ f(Δ_j) ≥ (8n) · f(∑Δ_j / (8n)).
 322    Follows from strict convexity of cosh. -/

used by (28)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.