phi_bounds_stub
plain-language theorem explainer
Coarse bounds 1.6 < phi < 1.7 are asserted for the self-similar fixed point phi drawn from the CPM constants bundle. Numerics modules in the Recognition derivations cite the result to license interval arithmetic without full precision. The proof is a one-line term that pairs the two supporting lemmas phi_gt_1_6 and phi_lt_1_7.
Claim. Let $phi$ be the self-similar fixed point constant from the CPM constants bundle. Then $1.6 < phi < 1.7$.
background
The Support.PhiApprox module supplies approximate numerical bounds on phi for use in downstream calculations. The constant phi is the self-similar fixed point satisfying the equation that forces it at step T6 of the unified forcing chain. The Constants structure from LawOfExistence bundles phi together with other CPM parameters such as Knet and Cproj.
proof idea
The proof is a term-mode pair constructor that directly returns the conjunction of the two private lemmas phi_gt_1_6 and phi_lt_1_7 defined in the same module. Each lemma unfolds Constants.phi, rewrites the target bound using the arithmetic expression (1 + sqrt(5))/2, and closes via linarith on the corresponding rational bound for sqrt(5).
why it matters
This theorem packages the directional inequalities into a single statement that downstream numerics modules are expected to import, as noted in the module doc-comment. It aligns with the forcing of phi as the self-similar fixed point at T6. No open questions are directly addressed; the result remains a lightweight support interface with zero downstream uses recorded so far.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.