phi_exponential_growth
plain-language theorem explainer
Records that the golden ratio satisfies φ > 1, hence φ^N diverges as N → ∞. Cited by the cubic Regge convergence certificate as the growth ingredient that keeps curvature from concentrating faster than the lattice resolves. Proof is a one-line term wrapper of the standard Constants lemma one_lt_phi.
Claim. The golden ratio satisfies $1 < \varphi$. Consequently $\varphi^N \to \infty$ as $N \to \infty$.
background
In the RS cubic-lattice gravity module, Regge convergence is proved without the full CMS regularity package. The lattice is perfectly shaped (identical cubes), carries an 8-tick UV cutoff at the fundamental voxel length, and inherits energy control from J-cost convexity. A fourth ingredient is exponential growth of φ: the bound φ^N > C·N³ (proved in GrowthBounds) ensures curvature cannot outrun lattice resolution.
The constant φ is the unique positive root of x² = x + 1 greater than 1; the framework forces it as the self-similar fixed point (T6). The elementary comparison 1 < φ is already established in Constants (via √5 > 1) and re-exported through PhiSupport. This declaration simply names that fact inside the cubic-convergence file so the certificate can point at a local hypothesis.
proof idea
One-line term proof: the goal 1 < phi is discharged by applying the existing lemma one_lt_phi from Constants (equivalently PhiSupport.one_lt_phi). No local arithmetic is repeated.
why it matters
Feeds the field phi_growth of cubic_convergence_cert, the package that asserts unconditional O(a²) weak-field Regge convergence on the RS Z³ lattice. The module strategy lists the φ-exponential growth bound as item 4 of the reasons CMS is unnecessary: φ^N beats any fixed polynomial in N, so discrete curvature mass cannot concentrate faster than the mesh can resolve. Landmark link: T6 (φ forced) plus the GrowthBounds hierarchy. Does not itself close the strong-field case; that remains conditional on bounded curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.