sampledCost
plain-language theorem explainer
sampledCost sums the J-cost of radial step ratios over N discrete angular increments along a logarithmic spiral. Researchers modeling variational spiral wavefields under φ-scaling would reference this when discretizing paths for cost evaluation in Recognition Science calculations. The definition directly applies the stepRatio helper at each sampled angle θ + n Δθ and accumulates the results via Finset sum.
Claim. The sampled cost is defined as $S = (1/N) sum_{n=0}^{N-1} J(ratio_n)$ where ratio_n = r(θ_n + Δθ)/r(θ_n), θ_n = θ + n Δθ, and the log-spiral radius satisfies r(θ) = r_0 φ^{(κ θ)/(2π)} with κ drawn from the parameter record P.
background
The Spiral.SpiralField module introduces a scaffold for variational ansatz of logarithmic spiral fields under φ-scaling and eight-tick gating constraints. Only basic structures and helpers are defined here, with no proofs needed for compilation. The local Params structure holds an integer kappa that sets the spiral exponent in the radius formula r(θ) = r0 · φ^{(κ · θ)/(2π)}.
proof idea
This is a direct definition that sums Jcost of stepRatio over the range 0 to N-1. For each n it forms θn = θ + n · Δθ then feeds stepRatio(r0, θn, Δθ, P) into Jcost. The construction relies on the sibling stepRatio definition and standard Finset summation.
why it matters
This helper discretizes the continuous spiral path for cost sampling in the Spiral wavefields scaffold. It supports future calculations of neutrality scores and eight-gate predicates within the module, aligning with the φ-scaling and eight-tick octave (T7) in the Recognition Science forcing chain. The module remains scaffolding with no downstream usage yet, leaving open the integration with full variational theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.