module module high

`IndisputableMonolith.Information.LocalCache`

The LocalCache module supplies the core cost definitions for cache hierarchies in the Information domain of Recognition Science. It introduces totalAccessCost as the weighted sum of access frequencies times distances, together with cachedAccessCost and local_cache_benefit. Researchers analyzing J-cost flows on hierarchies cite these objects when setting up the gradient-descent argument. The module consists entirely of definitions with no theorems or proofs.

claimTotal access cost without cache is the weighted sum $C = ∑ f_i d_i$ of access frequencies $f_i$ and distances $d_i$. Cached access cost and local cache benefit are defined as the corresponding reductions when a local cache is present.

background

The module imports Constants, which fixes the RS time quantum τ₀ = 1 tick, and the Cost module that supplies the J-cost framework. It operates inside the Information domain and precedes the hierarchy analysis. Sibling definitions include totalAccessCost, cachedAccessCost, local_cache_benefit, fibonacci_recurrence, constant_ratio, and Jcost_symmetry_forces_geometric_boundary.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

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

scope and limits

Does not prove any convergence or optimality result.
Does not specify numerical values or concrete hierarchies.
Does not define the full space of cache hierarchies.
Does not connect to the forcing chain T0-T8 or the Recognition Composition Law.

used by (1)

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

IndisputableMonolith.Information.PhiHierarchyGrowth module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

def totalAccessCost L26
def cachedAccessCost L31
theorem local_cache_benefit L46
def fibonacci_recurrence L63
def constant_ratio L67
theorem fibonacci_ratio_forces_golden L73
theorem fibonacci_partition_forces_phi L108
theorem Jcost_symmetry_forces_geometric_boundary L138
def synapse_cost L183
theorem Jcost_pos_away_from_one L192
theorem hebbian_sign_structure L210
theorem Jcost_min_at_one L228
theorem Jcost_pos_of_ne_one L231
def working_memory_capacity L245
theorem working_memory_approx L247
def localCacheStatus L264