distinction_first
plain-language theorem explainer
The theorem shows that the distinction stage precedes every other stage in the pre-temporal forcing order by having the lowest rank. Researchers tracing the dependency chain from recognition to time would cite it to fix the initial position. The proof is a one-line wrapper that applies case analysis on the stage and simplifies the rank inequality.
Claim. For every stage $s$ in the pre-temporal forcing chain with $s$ not equal to the distinction stage, the rank of distinction is strictly less than the rank of $s$.
background
The Pre-Temporal Forcing Order module records the dependency order that exists before time in Recognition Science. The Stage inductive type enumerates the stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. The rank function maps distinction to 0 and each subsequent stage to the next integer. Before(a, b) is defined as rank(a) < rank(b), making the relation a forcing priority rather than chronological time.
proof idea
The proof is a one-line wrapper that applies case analysis on s. Simplification with the definitions of Before and rank then discharges the goal for every constructor other than distinction, using the hypothesis that s differs from distinction.
why it matters
This theorem anchors the start of the pre-temporal forcing chain by placing distinction first. It supports the distinction between recognition-light (the primitive revealing act) and physical light (downstream of J-cost and spacetime). The module doc-comment notes that physical light is the first boundary of spacetime, not the first item in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.