totalAccessCost
plain-language theorem explainer
The total access cost definition supplies the baseline aggregate cost for n items as the sum of each item's access frequency multiplied by its distance. Cache-optimality proofs in the Local Cache Theorem would reference this as the uncached reference point when establishing strict cost reduction under caching. The definition expands directly to a finite sum without additional lemmas or reductions.
Claim. The total access cost without caching is defined by the weighted sum $∑_{i ∈ Fin n} freq(i) ⋅ dist(i)$.
background
This definition appears in the Information.LocalCache module, which develops the machine-verified core of the Inevitability of Local Minds paper. The module establishes that caching strictly reduces total access cost under assumptions A1–A3, with optimal partitions forcing the golden ratio φ via Fibonacci-like recurrences.
proof idea
The definition is a direct one-line summation that multiplies each frequency by its corresponding distance and sums the products over the finite index set Fin n.
why it matters
This baseline cost definition underpins the local_cache_benefit theorem in the same module, which shows caching reduces total access cost. It connects to the Recognition Science framework through the J-cost primitives imported from MultiplicativeRecognizerL4.cost (derived cost of a multiplicative recognizer's comparator on positive ratios) and ObserverForcing.cost (J-cost of a recognition event).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.