pred
The definition pred supplies the cyclic predecessor on the three Vantage perspectives in the RRF framework. Researchers deriving physical predictions from vantage cycling in cosmology or particle physics cite it to rotate through subjective, dynamic, and objective views. The definition proceeds by exhaustive pattern matching on the three constructors of Vantage.
claimLet $V$ be the set of vantages with elements inside (subjective qualia), act (dynamic process), and outside (objective observation). The predecessor map pred : $V$ → $V$ is defined by pred(inside) = outside, pred(act) = inside, and pred(outside) = act.
background
In the RRF.Core.Vantage module the Vantage type is introduced as an inductive type whose three constructors capture the fundamental perspectives on the One Thing: inside for the subjective view (qualia, meaning, experience), act for the dynamic view (recognition, process, becoming), and outside for the objective view (physics, measurement, observation). The module states that every phenomenon admits these three consistent vantages and that consistency across them is required for actual existence. The predecessor definition rests directly on this inductive Vantage declaration.
proof idea
The definition is realized by a direct match expression on the three Vantage constructors, sending inside to outside, act to inside, and outside to act. No lemmas are invoked; the implementation is a pure case analysis on the inductive type.
why it matters in Recognition Science
This definition is invoked by eighteen downstream declarations, including H_late_pred_value in Cosmology.HubbleTension (which obtains the 73.016 Hubble prediction), muon_mass_pred_bounds and tau_mass_pred_bounds in LeptonGenerations, V_cb_from_cube_edges in CKMGeometry, and winding_surjective_single in WindingCharges. It supplies the cyclic structure required for vantage rotation inside the RRF core, enabling the consistency condition across the three perspectives that underpins the framework's physical derivations.
scope and limits
- Does not define or reference a successor operation.
- Does not prove any identities such as pred composed three times equals the identity.
- Does not apply outside the Vantage inductive type.
- Does not establish bijectivity or other algebraic properties.
formal statement (Lean)
58def pred (v : Vantage) : Vantage :=
proof body
Definition body.
59 match v with
60 | inside => outside
61 | act => inside
62 | outside => act
63
used by (18)
-
H_late_pred_value -
ratioInRange -
winding_surjective_single -
V_cb_from_cube_edges -
muon_mass_pred_bounds -
tau_mass_pred_bounds -
pmns_theta12_match -
nu2_match -
nu3_match -
squared_mass_ratio_structural_phi7 -
two_div_17_upper -
pred_succ_id -
succ_pred_id -
muon_mass_pred_bounds -
tau_mass_pred_bounds -
bottom_mass_match -
charm_mass_match -
top_mass_match