IndisputableMonolith.Foundation.MaximalForcing.RSPhiUniverse
Defines the phi layer of Maximal Forcing: positive ratios obeying the golden equation, the associated claim class, and a universe certificate that classifies "is phi" as Forced. Anyone wiring Forced/Independent/Selected drainage into RealityClosure cites this. The module packages PhiForcing into the closure interface via admissibility predicates, classifiers, and a short independence check over a weaker class.
claimA ratio $r>0$ is phi-admissible when $r^2=r+1$. The phi universe is the forcing layer whose claims assert that the unique positive solution is $\varphi=(1+\sqrt{5})/2$, with a classifier and certificate placing that claim in the Forced branch of reality closure; over the weaker non-positive golden class the same claim is independent.
background
Maximal Forcing aims at a Reality Closure certificate: every claim in the closure of a universe is classified Forced, Independent, or Selected. RealityClosure states that interface without asserting the final theorem. PhiForcing supplies the upstream physics: self-similarity of a discrete ledger with J-cost forces the golden ratio $\varphi$ as the unique positive fixed point of the scale equation (framework landmark T6).
This module is the phi slice of that program. It introduces phi-admissibility (positive $r$ with $r^2=r+1$), two nested classes $L_{\phi 0}$ and $L_{\phi}^{\mathrm{gold}}$, the claim "is phi", and a small universe object carrying a classifier and certificate. The golden constraint is the algebraic content of self-similarity; positivity selects the physical root $\varphi>1$ rather than $1-\varphi$.
proof idea
Not a single theorem: a layer module. Admissibility and the two $L_\phi$ classes are definitions. Tightening $L_{\phi 0}\subseteq L_{\phi}^{\mathrm{gold}}$ is a short inclusion. The claim predicate, universe bundle, Forced classification, closure membership, and Forced-invariance are wrappers that plug PhiForcing into the RealityClosure certificate shape. A separate lemma records independence of "is phi" over the weaker non-positive golden class, matching the Selected-branch contrast used downstream.
why it matters in Recognition Science
Feeds RSSelectionExample, which drains a genuine Selected claim on the golden class without positivity and contrasts it with Forced layers (cost, phi, dimension, alpha). Without this module the phi branch of Maximal Forcing has no universe object or classifier to hand to the crown certificate. It is the T6 (phi forced) face of the forcing chain inside the closure program, parallel to cost and dimension layers. Downstream selection work relies on the Forced certificate here so that Selected can be exercised honestly on a nearby but weaker class.
scope and limits
- Does not prove the global Reality Closure crown theorem; only the phi-layer certificate interface.
- Does not re-derive phi from J-cost self-similarity; that lives in PhiForcing.
- Does not treat dimension, alpha, or mass-yardstick layers.
- Does not claim uniqueness without positivity; independence over the weaker golden class is explicit.
- Does not assert numerical bounds on alpha or mass rungs.
used by (1)
depends on (2)
declarations in this module (13)
-
def
PhiAdmissible -
def
Lphi0 -
def
LphiGold -
def
tighten_Lphi0_LphiGold -
def
isPhiClaim -
def
phiUniverse -
theorem
forced_isPhi -
theorem
isPhiClaim_in_closure -
def
isPhiForcedInvariant -
theorem
phiUniverse_classifier -
def
phiUniverseCert -
theorem
isPhi_independent_over_Lphi0 -
theorem
tightening_Lphi0_LphiGold_effective