succ
plain-language theorem explainer
The succ definition cycles the three vantages inside to act, act to outside, and outside to inside. Researchers modeling 3-phase rhythms in RRF causality or kinematics constructions cite this for the cyclic structure on perspectives. It is realized by exhaustive pattern matching on the Vantage inductive type.
Claim. The cyclic successor on the set of vantages $V = $ {inside, act, outside} is the map $succ: V → V$ with $succ(inside) = act$, $succ(act) = outside$, $succ(outside) = inside$.
background
Vantage is the inductive type with three constructors: inside (subjective qualia), act (dynamic process), and outside (objective observation). The module states that these are three views of the same thing and that all three must be consistent for existence to be actual. The succ definition supplies the cyclic successor for the 3-phase rhythm.
proof idea
Direct pattern match on the three Vantage constructors with no lemmas or tactics applied.
why it matters
This definition supplies the successor operation used by ballP, ReachN, ballFS, and related causality constructions. It realizes the 3-phase rhythm required by the RRF core for consistency across perspectives and aligns with the eight-tick octave structure in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.