arithmetic_before_time
plain-language theorem explainer
arithmetic_before_time asserts that the arithmeticObject stage precedes the timeTick stage under the Before relation on pre-temporal stages. Researchers tracing the forcing chain in Recognition Science would cite this link to confirm arithmetic structure is available prior to time. The proof is a one-line decision procedure that invokes the decidable instance of Before.
Claim. In the pre-temporal forcing order, arithmeticObject precedes timeTick: rank(arithmeticObject) < rank(timeTick).
background
The module records the dependency order that exists before time in Recognition Science. Stage is the inductive type listing the pre-temporal stages from distinction through recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject to timeTick. Before is the predicate rank a < rank b, equipped with a decidable instance via Nat.decLt.
proof idea
One-line wrapper that applies the decidable instance of Before, reducing directly to the natural-number comparison of ranks.
why it matters
This theorem supplies one link in the pre-temporal forcing chain that places arithmetic before time ticks. It follows jCost_before_arithmetic and precedes time_before_spacetime, supporting the overall structure that forces time as a derived object after recognition-light and J-cost. The result contributes to the foundation section of the unified forcing chain without invoking physical constants or spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.