phi_rpow_neg_antitone
plain-language theorem explainer
The lemma establishes that the map x ↦ φ^{-x} is antitone on the reals, where φ is the golden ratio. Numerics routines for interval bounds on negative powers of φ invoke it when the exponent interval must be reversed. The proof negates the input inequality and reduces directly to the known monotonicity of φ^x.
Claim. The function $x ↦ φ^{-x}$ is antitone on $ℝ$: if $x ≤ y$ then $φ^{-y} ≤ φ^{-x}$.
background
This lemma sits inside the module that supplies rigorous interval arithmetic for the power function via the identity $x^y = exp(y · log x)$ for $x > 0$. The golden ratio φ is the self-similar fixed point forced by the Recognition Science chain (T5–T6). The sole upstream dependency is the lemma that $x ↦ φ^x$ is monotone increasing.
proof idea
The term proof assumes y ≤ z, obtains -z ≤ -y by applying negation to both sides of the inequality, and feeds the reversed relation into the monotonicity lemma for φ^x to conclude φ^{-z} ≤ φ^{-y}.
why it matters
The result closes the negative-exponent case needed for interval propagation of the factors φ^{-5} and φ^{-3} that appear in the mass formula and Berry creation threshold. It supports the sibling declarations phi_pow_neg5_interval and phi_pow_neg3_interval inside the same module. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.