Before
plain-language theorem explainer
The forcing priority predicate supplies the strict order on pre-temporal stages by comparing their numerical ranks. Physicists tracing the forcing chain from distinction to time would cite this to establish priority without invoking chronology. It is introduced as a direct abbreviation of the rank inequality, with an automatic decidability instance.
Claim. For stages $a$ and $b$ in the pre-temporal forcing chain, $a$ precedes $b$ if and only if the rank of $a$ is strictly less than the rank of $b$.
background
Stage is the inductive type enumerating the dependency stages in the pre-temporal forcing chain, beginning with distinction and ending with timeTick. The rank function assigns a natural number to each stage, with distinction receiving rank zero and subsequent stages receiving higher values. This module establishes the dependency order that precedes physical time in Recognition Science. The order is not chronological but reflects which structures are required as prior dependencies. Upstream results include the definition of rank that maps each stage to its numerical priority.
proof idea
The definition directly sets the predicate to the strict inequality of ranks. A decidability instance follows immediately from the decidability of natural number comparison.
why it matters
This predicate supports the main order theorems such as distinction first and arithmetic before time. It fills the role of defining the forcing priority in the pre-temporal chain, linking to the Recognition Science landmarks of the forcing chain from T0 to T8. It enables the separation between recognition-light and physical light as described in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.