totalEnergy
plain-language theorem explainer
Total energy of an eight-tick cadence is the undiscounted sum of per-tick virtue-action energy costs. Temperance and least-action checks in the RS→RL bridge cite it as the window scalar. The body is a plain Fin 8 sum; no lemmas are needed beyond the energy-cost map on virtue actions.
Claim. Given an eight-tick cadence $c$ (states and virtue actions indexed by $t\in\{0,\ldots,7\}$), the total energy is $$E(c)=\sum_{t=0}^{7}\mathrm{energyCost}(a_t),$$ where $a_t$ is the virtue action at tick $t$. The sum is undiscounted.
background
The RS→RL bridge treats Recognition Science as control theory: moral states, fourteen virtue generators as admissible actions, σ=0 feasibility via LACompletion, and evaluation on fixed eight-tick windows rather than discounted returns.
EightTickCadence packages one such window: a map Fin 8 → MoralState and a map Fin 8 → VirtueAction. Its doc-comment states the design rule from T6 minimality: "no arbitrary discount"; the unique aggregator is the undiscounted sum over the eight-tick cadence. Policy and critic therefore treat each 8-tick block as an atomic step.
Per-tick cost comes from VirtueAction.energyCost, the scalar cost of a coefficient vector in the virtue basis. This definition lifts that tick cost to the full window.
proof idea
Pure definition, not a theorem. The body is the Finset sum over Fin 8 of VirtueAction.energyCost applied to c.actions t. No rewriting, no upstream lemmas, no tactics.
why it matters
Gives the window-level energy scalar required by the bridge's temperance constraint. Downstream, satisfiesTemperanceWindow c budget is exactly totalEnergy c ≤ budget, so every temperance audit routes through this sum.
It also appears in the least-action certification surface and in energy-related Hamiltonian/Noether statements that share the total-energy vocabulary, tying the RL window cost to the mechanical conservation story.
Framework landmark: T6/T7 eight-tick octave. The module header insists on undiscounted 8-tick blocks as the unique temporal aggregator; this def is that aggregator for energy. Without it, temperance and multi-tick feasibility checks have no canonical scalar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.