totalAccessCost
plain-language theorem explainer
totalAccessCost defines the baseline total access cost for n items as the sum of each frequency multiplied by its distance. Cache theorists working on the Local Cache Theorem cite it to establish the uncached reference point before comparing benefits. The definition is a direct summation with no lemmas or reductions applied.
Claim. For $n$ items with frequencies $f : [n] → ℝ$ and distances $d : [n] → ℝ$, the total access cost is $∑_{i=1}^n f_i d_i$.
background
The LocalCache module supplies the machine-verified core of the Inevitability of Local Minds paper. Its main results include local_cache_benefit (caching reduces cost under A1–A3), fibonacci_partition_forces_phi, and hebb_is_Jcost_gradient. totalAccessCost supplies the uncached baseline used by those results. Upstream, cost from MultiplicativeRecognizerL4 is the derived cost of a comparator on positive ratios, while cost from ObserverForcing equals the J-cost of a recognition event.
proof idea
One-line definition that directly implements the weighted sum over Fin n.
why it matters
This definition supplies the uncached reference required by local_cache_benefit and the phi-optimal hierarchy results in the module. It anchors comparisons to the J-cost framework imported from ObserverForcing and MultiplicativeRecognizerL4. The declaration closes the baseline side of the cache-benefit argument in the paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.