tc_growth_prop
plain-language theorem explainer
tc_growth_prop packages the monotonicity of the phi-power map as a reusable proposition in the URC growth interface. Researchers working on scaling laws in Recognition Science cite it when chaining order-preserving arguments along the phi-ladder. The declaration is a direct forall statement over real pairs that encodes non-decreasing behavior without internal lemmas.
Claim. The proposition that for all real numbers $x$ and $y$, if $x ≤ y$ then $Φ(x) ≤ Φ(y)$, where $Φ(x) = exp(log φ ⋅ x)$ and $φ$ is the self-similar fixed point.
background
PhiPow is the upstream wrapper defined by PhiPow(x) := Real.exp(Real.log(Constants.phi) * x). The module URCAdapters.TcGrowth supplies a simple computation growth interface that exports this Prop, which holds because PhiPow is strictly increasing when φ > 1. This rests on the Scales module definition of PhiPow as the concrete exponential realization of phi-powers.
proof idea
The declaration is a definition whose body is exactly the forall statement. No tactics or lemmas are invoked inside the def; the content is the direct assertion of the order-preserving implication.
why it matters
This definition supplies the interface used by the downstream lemma tc_growth_holds, which discharges the Prop by proving log φ > 0. It supports Recognition Science scaling by formalizing monotonic growth on the phi-ladder, consistent with the self-similar fixed point from T6 and the eight-tick octave. It leaves open the explicit linkage to physical constants such as the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.