totalAccessCost
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.
claimThe 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 in Recognition Science
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).
scope and limits
- Does not incorporate any caching mechanism or maintenance overhead.
- Does not specify or assume particular values for frequencies or distances.
- Does not extend to infinite domains or continuous distributions.
- Does not compute benefits or compare to cached scenarios.
formal statement (Lean)
26noncomputable def totalAccessCost (n : ℕ) (freq : Fin n → ℝ) (dist : Fin n → ℝ) : ℝ :=
proof body
Definition body.
27 ∑ i : Fin n, freq i * dist i
28
29/-- Cached access cost: cached items accessed at distance ε, uncached at full distance,
30 plus maintenance overhead α per cached item. -/