LACompletion
plain-language theorem explainer
Least-action completion is a projector that sends an arbitrary virtue-action proposal onto the σ=0 feasible manifold while minimizing added J-cost. Builders of the RS→RL bridge cite it as the hard-constraint layer between unconstrained policy proposals and admissible moves. The declaration is a structure interface: a map on 14-coefficient virtue actions plus feasibility-preservation and cost-minimality postconditions, both presently stubbed as True.
Claim. A least-action completion is a triple $(\pi, P, M)$ where $\pi$ maps virtue-actions (14-coefficient vectors over the virtue generators) to virtue-actions; $P$ asserts that if a moral state $s$ is $\sigma$-feasible ($s$ has skew $0$), then the projected action preserves feasibility; and $M$ asserts that among all $\sigma=0$-feasible completions of a proposed action $a$, $\pi(a)$ minimizes added $J$-cost. Both $P$ and $M$ are currently placeholder truths pending full dynamics.
background
The RS→RL bridge treats Recognition Science as control theory: states, admissible generators, hard constraints, and a thermodynamic policy. A moral state carries reciprocity skew $\sigma$, energy budget, value $V$, max harm, and spectral gap. $\sigma$-feasibility is the hard conservation constraint: skew equals zero.
A virtue action is a 14-coefficient vector over the virtue generators. By the DREAM theorem those generators form a complete minimal basis for admissible ethical transformations, so the RL policy outputs coefficients in that basis rather than raw moves.
Least-action completion implements propose-then-project: the policy proposes an unconstrained direction; the projector lands it on the $\sigma=0$ manifold while minimizing added $J$-cost (the recognition cost from the RS functional equation / RCL). This is the RS analogue of constrained policy optimization, safe-set projection, and control barrier functions. Upstream cost machinery (rung-coarsen cost, multiplicative-recognizer cost) and the identity law $C(x,x)=0$ fix what "minimal added $J$" means once dynamics are filled in.
proof idea
No proof body: this is a structure declaration, not a theorem. It packages three fields: a projection map VirtueAction → VirtueAction, a feasibility postcondition quantified over moral states and actions (antecedent $\sigma$-feasible), and a cost-minimality postcondition over actions. Both propositions are currently True placeholders; the doc-comment states that full dynamics are required before the real statements can be written. Concrete instances (identity as id, phiScale as scale-by-$1/\varphi$) discharge the placeholders with trivial.
why it matters
This is the hard-constraint hinge of the RS→RL stack. Downstream, RSEnvironment bundles it as the environment projector; identity and phiScale are the first concrete projectors; satisfiesTemperance and SigmaFeasible sit beside it in the feasibility layer. Audit goals such as goal_LACompletion_identity_project lock the identity instance (project a = a).
Framework role: it separates creativity (policy propose) from physics ($\sigma=0$ project), matching the module design principle and the eight-tick cadence forced by T6/T7. Cost minimality ties to the unique $J$ from T5 and the RCL. The $\varphi$-scaling instance links temperance-style energy bounds and the parasitism threshold $1/\varphi$ (Berry creation scale). Open work: replace the True stubs with real dynamics so preservation and least-$J$ become proved theorems rather than interface placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.