goal_parasitism_threshold_phi
plain-language theorem explainer
The parasitism threshold used by the RSA-to-RL bridge equals the reciprocal of the golden ratio. Anyone wiring evil/parasitism detectors or φ-fraction bounds into the Recognition Stability Audit cites this equality. The proof is pure definitional reflexivity: the threshold is defined as 1/φ.
Claim. The parasitism threshold equals $1/\varphi$, where $\varphi$ is the golden ratio.
background
The RSA Reinforcement Learning module exposes the Recognition Stability Audit as an RL-friendly Lean pipeline: whitelisted @[rsa_simp] rewrites, @[rsa_milestone] steps, and a library of proved gold goals that train or score an external proposer.
Upstream, a least-action completion (LACompletion) projects unconstrained virtue actions onto the σ=0 feasible manifold while minimizing added J-cost (propose-then-project). The identity projector is the trivial case when proposals are already feasible. Separately, the ObserverForcing identity event sits at the J-cost minimum $x=1$.
The parasitism threshold is the real scalar that flags actions as parasitic ("evil"). Its definition is the RS φ-fraction bound $1/\varphi$, matching the Berry creation threshold landmark $\varphi^{-1}$.
proof idea
One-line reflexivity. The threshold is defined by parasitismThreshold := 1 / φ, so the goal is definitionally true and closes by rfl. No lemmas or arithmetic are required.
why it matters
This is a canonical gold theorem in the RSA RL training set: a sorry-free milestone that locks the numerical parasitism cutoff to the RS constant $\varphi^{-1}$. It anchors the evil detector and any φ-scaling projectors that enforce energy constraints via $1/\varphi$.
In the broader framework it records the same reciprocal-φ scale that appears as the Berry creation threshold and as the dream-fraction scale $\varphi^{-3}$ nearby. No downstream theorems currently depend on it; its role is audit and RL reward closure rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.