PhiPositivityCert
plain-language theorem explainer
Empty audit certificate whose verification predicate asserts that the golden ratio satisfies both 0 < φ and 1 < φ. Anyone building on the φ-ladder, mass rungs, or scale hierarchy cites this to lock the two elementary bounds. The companion theorem discharges the predicate by pairing the library lemmas phi_pos and one_lt_phi.
Claim. There is a certificate type whose verification predicate holds precisely when $0 < \varphi$ and $1 < \varphi$, where $\varphi = (1 + \sqrt{5})/2$. For every such certificate the predicate is true.
background
In Recognition Science the golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. It is the base of the $\varphi$-ladder that grades masses, couplings, and recognition scales. Two elementary inequalities are required before any ladder argument can run: strict positivity ($\varphi > 0$), so $\varphi$ is a legitimate ratio/scale factor, and supercriticality ($\varphi > 1$), so powers $\varphi^n$ grow unboundedly and $\varphi^{-n}$ decay to zero.
This module packages those two bounds as a verification certificate. The structure itself carries no data; the content lives in the predicate verified, which is the conjunction $(0 < \varphi) \wedge (1 < \varphi)$. Upstream, Constants.one_lt_phi proves $1 < \varphi$ from $\sqrt{5} > 1$, and the companion positivity lemma supplies $0 < \varphi$. Without $\varphi > 1$ the ladder would collapse ($\varphi = 1$) or invert ($\varphi < 1$).
proof idea
The structure is an empty marker (only Repr). The predicate is definitionally the conjunction $(0 < \mathrm{phi}) \wedge (1 < \mathrm{phi})$. The discharge theorem is a two-line constructor: the left conjunct is phi_pos, the right is one_lt_phi from Constants (proved by comparing $\sqrt{5}$ against $1$ and rearranging $(1+\sqrt{5})/2 > 1$). Both sides are marked @[simp], so downstream goals of the form verified c simplify away.
why it matters
Positivity and supercriticality of $\varphi$ are load-bearing for the entire RS certificate chain. Every mass formula of the form yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, the Berry threshold $\varphi^{-1}$, $Z_{\mathrm{cf}} = \varphi^5$, and the dream fraction $\varphi^{-3}$ presuppose a genuine hierarchical ladder. The module doc states the stakes directly: without $\varphi > 1$ the ladder collapses or inverts. This certificate is the audit-facing packaging of those two bounds, sitting in the Verification domain so later certificates can assume them by a single simp rather than replaying the $\sqrt{5}$ arithmetic. No downstream consumers are wired yet (used_by is empty); the intended role is a leaf fact in larger positivity or hierarchy audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.