module module

`IndisputableMonolith.Papers.GCIC.LocalCacheForcing`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

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

IndisputableMonolith.Papers.GCIC.BrainHolography module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Papers.GCIC.GraphRigidity module_import

declarations in this module (13)

theorem Jcost_strictMono_on_Ici_one L31
theorem Jcost_mono_on_Ici_one L45
lemma phi_pow_ge_one L54
lemma phi_pow_strictMono L65
theorem Jcost_phi_pow_strictMono L70
theorem access_cost_increases_with_distance L77
theorem access_cost_zero_at_origin L82
theorem access_cost_pos_of_nonzero L86
theorem collocation_minimizes_cost L94
theorem caching_is_forced L100
theorem phi_from_fibonacci_ratio L119
theorem optimal_at_minimum_is_holographic L138
theorem local_cache_forcing_certificate L153