Jcost_phi_pow_strictMono
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim monotonicity of Jcost for arguments outside [1, ∞).
- Does not compute explicit numerical values of Jcost(φ^k).
- Does not address graphs that are not phi-ladder structured.
- Does not derive the functional equation satisfied by J itself.
Lean usage
theorem access_cost_increases_with_distance (d₁ d₂ : ℕ) (h : d₁ < d₂) : Jcost (phi ^ d₁) < Jcost (phi ^ d₂) := Jcost_phi_pow_strictMono hformal statement (Lean)
70theorem Jcost_phi_pow_strictMono {m n : ℕ} (hmn : m < n) :
71 Jcost (phi ^ m) < Jcost (phi ^ n) :=
proof body
Term-mode proof.
72 Jcost_strictMono_on_Ici_one (phi_pow_ge_one m) (phi_pow_strictMono hmn)
73
74/-! ## Part 3: Access Cost Properties -/
75
76/-- Farther access costs more. -/