eightTick_value_finite
plain-language theorem explainer
For any eight-tick cadence window and any real-valued state scoring function, the undiscounted total value over the eight ticks exists as a real number. Verification and RL-bridge authors cite this to certify that eight-tick returns are well-defined before attaching policies or critics. The proof is a one-line existence witness: the sum itself, with reflexivity.
Claim. For every eight-tick cadence $c$ (a window of eight moral states together with the actions taken at each tick) and every scoring map $v$ from moral states to $\mathbb{R}$, there exists a real number equal to the undiscounted sum $\sum_{t=0}^{7} v(c_t)$.
background
The RS→RL bridge treats Recognition Science as control theory: moral states carry skew $\sigma$, energy budget, value $V$, max harm, and spectral gap; actions are coefficient vectors on the fourteen virtue generators; hard feasibility is $\sigma=0$ via LACompletion. Temporal aggregation is forced by the eight-tick octave (T6/T7): no arbitrary discount factor.
EightTickCadence packages an eight-state window and the corresponding virtue actions. Its total value is the finite undiscounted sum $\sum_{t:\mathrm{Fin},8} \mathrm{valueAt}(\mathrm{window},t)$. The module design principle is that policy and critic operate on these eight-tick blocks as atomic steps, matching the unique aggregator from T6 minimality.
proof idea
Term-mode existence proof. The witness is exactly c.totalValue valueAt (the Fin-8 sum of the scoring function on the window). The equality obligation is discharged by rfl. No lemmas beyond the definition of total value are required; finiteness is immediate because the index type is finite.
why it matters
Closes a basic well-definedness obligation in the RS→RL verification layer: eight-tick returns are ordinary reals, not partial or infinite objects. Downstream, goal_eightTick_value_finite in the RL audit module is a one-line re-export of this fact, so audit goals can name a stable interface without depending on the bridge internals.
Framework landmark: the eight-tick octave (T7 / T6 minimality) forces undiscounted block evaluation rather than exponential discounting. This lemma is the trivial but necessary certificate that the block return exists before lexicographic selectors, Gibbs policies, or harm-minimax objectives consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.