AnnularTrace
plain-language theorem explainer
AnnularTrace packages a fixed integer charge with a refinement family of annular meshes indexed by natural number N such that every mesh carries exactly that charge. Researchers formalizing carrier budget bounds in the Recognition Science annular J-cost layer cite this structure to state mesh-independent excess claims without quantifying over arbitrary meshes. The definition is a direct packaging of the charge field, the mesh map, and the uniformity condition with no lemmas applied.
Claim. An AnnularTrace consists of an integer charge $q$ together with a family of annular meshes $M(N)$ indexed by $N : ℕ$ such that the charge of each mesh $M(N)$ equals $q$.
background
The Annular J-Cost Framework defines phiCost u := cosh((log φ)·u) − 1 = J(φ^u) and uses annular sampling to obtain Jensen-based coercivity: nonzero winding forces Θ(m² log N) cost while holomorphic nonvanishing yields O(R²) annular cost. AnnularMesh is the structure of N concentric rings whose rings map to AnnularRingSample, equipped with a single charge and the uniform_charge axiom ensuring every ring winding equals that charge. The local setting is the constructive formalization of the RS topological cost-covering bridge, where trace families supply the realizable interface for budget claims once the analytic carrier is equipped with a concrete zero-charge refinement family.
proof idea
This is a structure definition that directly assembles the three fields: the integer charge, the map from N to AnnularMesh, and the charge_spec axiom enforcing uniformity. No upstream lemmas are invoked; the construction is purely data packaging.
why it matters
AnnularTrace supplies the concrete trace family required by BudgetedCarrier, which extends RegularCarrier with an explicit excess-budget witness along a specific zero-charge annular trace. It completes the realizable interface for mesh-independent budget claims in the RS topological cost-covering bridge and connects to the phi-ladder through the annular sampling machinery that supports the eight-tick octave and D = 3. The definition closes the gap between synthetic meshes and the concrete Euler zero-trace used in downstream carrier constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.