complements
plain-language theorem explainer
The complements definition assigns to each of the three vantages its ordered pair of the remaining two. Researchers formalizing consistency among subjective, dynamic, and objective perspectives in the RRF framework would cite it when establishing the cyclic three-phase structure. The definition is realized by exhaustive pattern matching on the three constructors of the Vantage inductive type.
Claim. Let the set of vantages consist of inside (subjective/qualia view), act (dynamic/process view), and outside (objective/physics view). The function complements maps each vantage to the ordered pair of the other two: complements(inside) = (act, outside), complements(act) = (inside, outside), complements(outside) = (inside, act).
background
The RRF.Core.Vantage module introduces the three fundamental perspectives on the One Thing. Vantage is the inductive type whose constructors are inside (subjective perspective: qualia, meaning, experience), act (dynamic perspective: recognition, process, becoming), and outside (objective perspective: physics, measurement, observation). The module states that these are not three different things but three views of the same thing, with the requirement that all three must be consistent for existence to be actual.
proof idea
The definition proceeds by pattern matching on the input vantage. The inside case returns the pair (act, outside), the act case returns (inside, outside), and the outside case returns (inside, act). This exhausts the three constructors of the Vantage type.
why it matters
This definition supplies the basic pairing that realizes the cyclic three-phase rhythm. It is used by the theorem passive_fraction_lt_one in Cosmology.VacuumUniformity, whose doc-comment notes that the active fraction complements the passive fraction to 1. The pairing therefore anchors the consistency condition among the three vantages and feeds the broader Recognition Science landmarks of the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.