rank
plain-language theorem explainer
The rank function assigns consecutive natural numbers to the stages of the pre-temporal forcing chain, with distinction at rank 0 and embodied observer at rank 12. Researchers tracing dependency priorities before the emergence of time cite it to compare forcing order. The definition is given by exhaustive pattern matching on the Stage inductive type.
Claim. Define the function $rank : Stage → ℕ$ by $rank(distinction) = 0$, $rank(recognitionInterface) = 1$, $rank(singleValuedPredicate) = 2$, $rank(symmetricComparison) = 3$, $rank(compositionConsistency) = 4$, $rank(rcl) = 5$, $rank(jCost) = 6$, $rank(arithmeticObject) = 7$, $rank(timeTick) = 8$, $rank(spacetime) = 9$, $rank(lightCone) = 10$, $rank(photonEM) = 11$, $rank(embodiedObserver) = 12$.
background
Stage is the inductive type enumerating dependency stages in the pre-temporal forcing chain: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, spacetime, lightCone, photonEM, embodiedObserver. The module records a forcing order, not a chronological one: later stages require earlier ones as prior structure. Recognition-light (the primitive distinction) is pre-temporal while physical light (null cone and photon) appears downstream after J-cost and ticks.
proof idea
The definition is given directly by pattern matching on each constructor of the Stage inductive type, assigning the integers 0 through 12 in sequence.
why it matters
This supplies the numerical labels used by downstream results on feasible witnesses in SAT complexity, Hessian entries in cost projections, and verified constants in CPM audits. It fills the pre-temporal segment of the forcing chain (T0–T8) that runs from distinction through J-uniqueness and the eight-tick octave to D = 3. The definition supports the separation between recognition-light and physical light stated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.