time_before_spacetime
plain-language theorem explainer
The theorem places the timeTick stage before the spacetime stage in the pre-temporal forcing order. Researchers tracing Recognition Science dependencies from primitive distinction to emergent spacetime would cite this step. The proof is a one-line wrapper that invokes the decidable Nat.lt instance on the ranks.
Claim. Let rank denote the dependency rank on the pre-temporal stages. Then rank(timeTick) < rank(spacetime).
background
The module records a forcing order among stages that must precede physical time. Stage is the inductive type of these stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, spacetime. Before(a, b) is the proposition rank a < rank b, equipped with a Decidable instance via Nat.decLt.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic uses the Decidable instance for Before, which reduces directly to a decidable comparison of the two Nat ranks.
why it matters
The result fills the final link in the pre-temporal forcing chain of the module, confirming that spacetime appears after timeTick. It supports the distinction drawn in the module documentation between recognition-light (prior to time) and physical light (downstream of J-cost and spacetime). No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.