phiScale
plain-language theorem explainer
Defines the golden-ratio scaling projector: every virtue-action is multiplied by 1/φ before use. It is a concrete least-action completion used in the RS-to-RL bridge to enforce Temperance-style energy bounds. Construction is direct: the project field is action scaling, and the two structure obligations are discharged by trivial placeholders.
Claim. The $\varphi$-scaling projector is the least-action completion whose projection map sends a virtue-action $a$ to $a$ scaled by $1/\varphi$. Feasibility preservation and cost-minimization fields are held as trivial placeholders pending full dynamics.
background
The surrounding module turns Recognition Science into reinforcement-learning control: states are moral ledgers (bonds, skew, energy), actions are 14-coefficient combinations of virtue generators, and hard physics is enforced by projecting proposals onto the $\sigma=0$ feasible set.
LACompletion is that projector. It separates creativity (the policy proposes any direction) from physics (the completion forces $\sigma=0$ while adding as little $J$-cost as possible). Sibling fields include virtue-action scaling and an energy-cost functional used for Temperance checks.
$\varphi$ is the self-similar fixed point forced at T6 in the RS chain. Scaling by $1/\varphi$ is the elementary energy-bounding move that keeps proposed actions inside the Temperance envelope before lexicographic selection or Gibbs sampling over eight-tick windows.
proof idea
Pure structure instance, not a derived theorem. The project field is the one-line map $a \mapsto a.\mathrm{scale}(1/\varphi)$. The two proof fields preserves_feasibility and minimizes_cost are currently True placeholders, so both obligations are closed by trivial. No upstream lemmas are invoked beyond the ambient VirtueAction.scale operation and the LACompletion structure type.
why it matters
Supplies the simplest concrete LACompletion in the RS→RL bridge: a Temperance-style energy clamp by the golden-ratio factor. Module design treats this as the physics half of propose-then-project, feeding later lexicographic selectors and Gibbs policies $p(a|s)\propto\exp(-J(s,a)/T_R)$ over forced eight-tick cadences (T6/T7).
No downstream consumers are wired yet (used_by empty), so the definition is infrastructure for the audit path rather than a cited lemma. It sits next to feasibility predicates and virtue generators, and will matter once dynamics replace the True placeholders with real $\sigma=0$ postconditions. Landmark link: $\varphi$ from the forcing chain and the eight-tick window discipline of the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.