Jcost_symmetry_forces_geometric_boundary
plain-language theorem explainer
J-cost symmetry under inversion forces the optimal cache boundary to satisfy d² = D_ℓ D_prev for positive reals d, D_ℓ, D_prev. Researchers deriving hierarchical memory models from Recognition Science cite this to obtain the Fibonacci recurrence for successive cache sizes. The proof substitutes the squared expression for Jcost, cross-multiplies to reach a factored polynomial equation, and splits cases via the zero-product property.
Claim. Let $d, D_ℓ, D_{prev} > 0$. If $J(d/D_ℓ) = J(D_{prev}/d)$, then $d/D_ℓ = D_{prev}/d$ or $d/D_ℓ = (D_{prev}/d)^{-1}$.
background
J-cost is the function J(x) = (x + x^{-1})/2 - 1, equivalently expressed as (x-1)²/(2x) for x ≠ 0 by the Jcost_eq_sq lemma. The Local Cache module develops the theorem that caching reduces total access cost under assumptions A1-A3 and that optimal partitions obey the Fibonacci recurrence K_{ℓ+1} = K_ℓ + K_{ℓ-1}, which forces the golden ratio φ as the self-similar fixed point. This lemma sits inside the Local Cache Theorem and φ-Optimal Hierarchy section, relying on the Jcost_eq_sq identity and the mul_eq_zero theorem from IntegersFromLogic that supplies the zero-product law for the ring isomorphism with integers.
proof idea
The tactic proof defines a := d/D_ℓ and b := D_prev/d, establishes positivity of both, substitutes Jcost_eq_sq on each side of the balance hypothesis, simplifies the resulting equation with field_simp and linarith to obtain the cross-multiplication identity, then applies nlinarith to factor as (a-b)(ab-1)=0. It invokes mul_eq_zero to split into cases, handling a=b by linarith and ab=1 by inversion.
why it matters
The lemma supplies the geometric-mean boundary required by the Optimal Partition statement in the Local Cache Theorem, which feeds directly into the localCacheStatus definition and the fibonacci_partition_forces_phi result that extracts φ from the recurrence. It closes the step from J-symmetry in the forcing chain (T5) to the self-similar fixed point (T6) and the eight-tick octave structure. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.