pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Information.LocalCache

show as:
view Lean formalization →

This module defines total access cost without cache as the weighted sum of frequencies times distances, plus cached variants and local cache benefit using J-cost. Researchers modeling information hierarchies cite these primitives to analyze cache optimization. The module supplies only definitions, importing J-cost from Cost and the time quantum from Constants.

claimTotal access cost is defined as $C = f_i d_i$ (summed), with cachedAccessCost and local_cache_benefit obtained by subtracting J-cost savings at the cache boundary.

background

Recognition Science models information flow via J-cost, the functional J(x) = (x + x^{-1})/2 - 1 drawn from the Cost module. Constants supplies the RS time quantum τ₀ = 1 tick. This module introduces local cache structures to quantify access penalties in hierarchies of positive reals.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed IndisputableMonolith.Information.PhiHierarchyGrowth, whose doc-comment states that J-cost gradient descent on cache hierarchies necessarily converges to the Fibonacci/φ partition. The module supplies the cost functions required for that convergence argument.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)