totalValue
plain-language theorem explainer
Undiscounted total value of a real functional over an eight-tick cadence window: sum of the functional at each of the eight moral states. RL bridge and stability-audit code cite it as the atomic return for windowed critics and policies. The body is the finite sum over Fin 8; no discount factor appears.
Claim. Given an eight-tick cadence $c$ (states $c_t$ for $t\in\{0,\ldots,7\}$) and a real-valued map $v$ on moral states, the total value is $\sum_{t=0}^{7} v(c_t)$. The sum is undiscounted.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry skew σ, energy budget, value $V$, max harm, and spectral gap; admissible moves are 14 virtue generators; hard feasibility is σ=0 via LACompletion. Temporal aggregation is forced by T6 minimality: no arbitrary discount factor. The unique aggregator is the undiscounted sum over an eight-tick block (the octave period $2^3$ from the forcing chain).
EightTickCadence packages that block: a window map Fin 8 → MoralState and the virtue actions taken at each tick. MoralState is the lightweight RL state (skew, energy, value, maxHarm, robustness). The fundamental time quantum is one tick ($\tau_0=1$ in RS-native units); one octave is eight ticks.
Design rule from the module: policy and critic operate on 8-tick windows as atomic steps, matching T6 and the DREAM theorem references in the module doc.
proof idea
Pure definition, not a proof. The value is the Mathlib finite sum $\sum_{t:\mathrm{Fin},8} \mathrm{valueAt}(c.\mathrm{window}, t)$. No lemmas are applied; noncomputable only because the codomain is $\mathbb{R}$.
why it matters
Supplies the window return that the bridge uses instead of discounted infinite-horizon value. Downstream, eightTick_value_finite and the audit goal goal_eightTick_value_finite assert that this total is a well-defined real (witnessed by the sum itself). That closes the "value is finite on the cadence" obligation in the Recognition stability audit.
Framework landmark: T6/T7 eight-tick octave. The module explicitly rejects exponential discounting in favor of this undiscounted 8-sum, so lexicographic selectors and Gibbs policies can score trajectories on the forced period. Without this aggregator, the multi-objective stack (feasible → harm-minimax → value → robustness) would lack a canonical scalar for the value tier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.