card_vantage
plain-language theorem explainer
The declaration proves that the Vantage type in the RRF core has exactly three elements. A researcher modeling the three perspectives on phenomena would reference this cardinality when verifying consistency across inside, act, and outside views. The proof reduces immediately by reflexivity once the Fintype instance for Vantage is in scope.
Claim. The finite type consisting of the three fundamental vantages on reality has cardinality three: $Fintype.card(Vantage) = 3$.
background
In the RRF.Core.Vantage module, Vantage is defined as an inductive type with three constructors: inside for the subjective perspective (qualia and experience), act for the dynamic process view (recognition and becoming), and outside for the objective physics view (measurement and observation). These are three consistent perspectives on the same phenomenon, not distinct entities. The module states that all three must align for existence to be actual. The upstream result is the inductive definition of Vantage, which supplies the Fintype instance used here.
proof idea
The proof is a one-line term that applies reflexivity to the Fintype.card computation on the Vantage inductive type with its three explicit constructors.
why it matters
This result anchors the RRF core by fixing the number of fundamental vantages at three, supporting the key insight that phenomena require consistent inside, act, and outside views. It fills the basic counting step before higher-level consistency theorems in the Recognition framework. No open questions are directly touched, as the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.