PhiAdmissible
plain-language theorem explainer
A real scale ratio is phi-admissible when it is strictly positive and obeys the golden algebraic constraint r² = r + 1. This is the gate predicate for the T6 phi-layer realization in maximal forcing. Anyone citing the tightened class of positive golden ratios, or the independence of r = φ over mere positivity, uses this predicate. The body is a two-conjunct Prop definition, not a proof.
Claim. A real number $r$ is phi-admissible when $0 < r$ and $r^2 = r + 1$.
background
This module is the Phase-2 (T6) instantiation of maximal forcing: the carrier is a candidate scale ratio $r : \mathbb{R}$, and the claim under closure is that $r$ equals the golden ratio $\varphi$. The loose class is just the positive reals; the gate class adds the golden constraint.
Self-similarity in a discrete ledger forces the algebraic relation $x^2 = x + 1$: scaling by $r$ must be composable so that the next scale $r^2$ equals current-plus-base $r + 1$ (Fibonacci-like structure). That relation is packaged as satisfies_golden_constraint.
Positivity here is ordinary strict positivity on $\mathbb{R}$ (the loose class), not the PRC-native ratio-orbit positivity used elsewhere. The predicate simply conjoins the two conditions that define the gate.
proof idea
Definitional, not a theorem. The predicate is the conjunction of $0 < r$ and $r^2 = r + 1$ (via the golden-constraint abbreviation). No lemmas are applied; the body is the Prop that later admissibility classes and forcing statements quantify over.
why it matters
Feeds the gate-tightened class whose admissible set is exactly the phi-admissible reals, labeled as positive ratios with golden constraint $r^2 = r + 1$. That class is the T6 counterpart of the cost-layer gate: over it, $r = \varphi$ is forced (wrapping uniqueness of the self-similar fixed point); over mere positivity the same claim is independent ($r = 1$ is a positive counter-model).
In the forcing chain this is the T6 landmark: $\varphi$ forced as the self-similar fixed point. The definition is the legitimacy evidence that the golden-constraint tightening does real work, parallel to the cost-layer gate conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.