Jcost_phi_pow_strictMono
plain-language theorem explainer
The theorem states that the J-cost function satisfies J(φ^m) < J(φ^n) for natural numbers m < n. Researchers deriving local cache forcing or closing the brain holography chain cite it to establish that access cost strictly increases with distance on the phi-ladder. The proof is a direct term application of strict monotonicity of Jcost on [1, ∞) to the facts that φ^m ≥ 1 and φ^m < φ^n.
Claim. For natural numbers $m < n$, let $J$ denote the J-cost function and let $φ$ denote the golden ratio. Then $J(φ^m) < J(φ^n)$.
background
The module Local Cache Forcing from J-Cost Minimization shows that J-cost minimization on connected graphs forces hierarchical local caching, closing Gap G1 in the brain holography derivation. Jcost is the cost function (abbrev Cost from RSNative.Core) whose strict increase on [1, ∞) is given by the sibling theorem Jcost_strictMono_on_Ici_one: for 1 ≤ a < b one has Jcost a < Jcost b. The phi-ladder supplies the auxiliary facts phi_pow_ge_one (φ^n ≥ 1 for all n) and phi_pow_strictMono (φ^m < φ^n when m < n), both proved by induction or by the property one_lt_phi.
proof idea
The proof is a one-line term wrapper that applies Jcost_strictMono_on_Ici_one to the pair (phi_pow_ge_one m, phi_pow_strictMono hmn). No additional tactics or rewrites are required; the two upstream lemmas directly supply the hypotheses 1 ≤ φ^m and φ^m < φ^n.
why it matters
This result is invoked by access_cost_increases_with_distance, access_cost_pos_of_nonzero, collocation_minimizes_cost and the master local_cache_forcing_certificate inside the same module; it also appears in the conjunction that defines brain_holography_fully_forced. It supplies the concrete step “J(φ^d) increasing: farther = costlier” that follows T5 (J-uniqueness) and precedes the eight-tick octave and D = 3 in the forcing chain. The declaration closes the local-cache half of the Recognition Science argument that any remote allocation carries strictly higher total weighted cost than the collocated pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.