Vantage
plain-language theorem explainer
Vantage enumerates the three irreducible perspectives on any phenomenon in Recognition Science: subjective experience, dynamic process, and objective measurement. RRF core developers cite this when decomposing statements into vantage triples that must remain consistent. The declaration is an inductive enumeration whose Fintype instance is discharged by exhaustive case analysis on the three constructors.
Claim. Let $V$ be the type whose elements are the subjective perspective $I$, the dynamic perspective $A$, and the objective perspective $O$.
background
The RRF module treats every phenomenon as a single underlying reality viewed from three vantages. Inside captures qualia and subjective experience. Act captures recognition and becoming. Outside captures physics and measurement. The module doc states that all three views must be consistent for existence to be actual. The declaration depends on Fintype from Mathlib to record that exactly three elements exist.
proof idea
The inductive definition introduces three constructors. The Fintype instance lists the three elements explicitly and discharges completeness by case analysis on each constructor, using the decide tactic.
why it matters
This supplies the vantage type referenced by Glossary.V, card_vantage, complements, get, pred, succ, and the identity theorems pred_succ_id and succ_pred_id. It realizes the three-perspective requirement stated in the module doc. The complements definition downstream shows each vantage pairs with the remaining two, closing the finite structure needed for later RRF constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.