rcl_before_jCost
plain-language theorem explainer
The pre-temporal forcing order places the recognition composition law stage before the J-cost stage. Foundation researchers cite this to fix the dependency sequence among early structures that later force time and spacetime. The proof is a one-line decision that confirms the rank inequality via the built-in decidable instance for natural-number comparison.
Claim. In the pre-temporal forcing order, the stage for the recognition composition law precedes the J-cost stage: $rank(rcl) < rank(jCost)$.
background
The module records a forcing order among dependency stages that exist prior to physical time. Stage is the inductive type listing these stages in sequence: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before a b is the proposition rank a < rank b, equipped with a Decidable instance that reduces to Nat.decLt.
proof idea
The proof is a one-line wrapper that applies the decidable instance for Before. Because Before expands to rank a < rank b and the instance is Nat.decLt, the decide tactic directly resolves the comparison between the ranks assigned to Stage.rcl and Stage.jCost.
why it matters
This result inserts the recognition composition law immediately before J-cost in the pre-temporal chain, supplying one link in the sequence that forces arithmetic objects and time ticks. It supports the overall forcing chain (T0-T8) by fixing order among the early stages that precede spacetime. No downstream theorems are listed yet, but sibling results such as arithmetic_before_time rely on the completed order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.