tc_growth_holds
plain-language theorem explainer
Monotonicity of the PhiPow scaling function holds for real arguments under the ordering x ≤ y. Researchers modeling phi-ladder growth in nucleosynthesis tiers or spectral emergence would cite the result to justify tier ordering. The proof reduces the claim to positivity of log phi together with monotonicity of the exponential via a short chain of inequalities.
Claim. $x,y : ℝ, x ≤ y → Φ^{Pow}(x) ≤ Φ^{Pow}(y)$ where $Φ^{Pow}(z) := exp(log φ · z)$ and φ denotes the golden ratio with 1 < φ.
background
The module URCAdapters.TcGrowth supplies a minimal interface for computation growth. It exports the proposition tc_growth_prop, which asserts monotonicity of PhiPow. PhiPow is defined in RecogSpec.Scales as the map z ↦ exp(log φ · z). The constant φ satisfies 1 < φ by the upstream lemma one_lt_phi. Related upstream structures include the nuclear-density tiers in Astrophysics.NucleosynthesisTiers, which place physical quantities on discrete φ-ladders, and the J-cost structures in PhiForcingDerived.
proof idea
The tactic proof opens with intro x y hxy. It obtains 0 < φ from Constants.phi_pos and 0 < log φ from one_lt_phi together with Real.log_pos_iff. After dsimp on PhiPow it applies mul_le_mul_of_nonneg_left to the hypothesis hxy, then finishes with Real.exp_le_exp.mpr.
why it matters
The lemma supplies the concrete monotonicity fact required by URC adapters that rely on phi-based scaling. It sits downstream of one_lt_phi and the phi-forcing structures, and is consistent with the self-similar fixed point T6 and the phi-ladder mass formula. No parent theorem in the supplied used_by list consumes it yet; the result therefore closes a local interface requirement without resolving any larger open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.