spacetime_before_lightCone
plain-language theorem explainer
The declaration asserts that the spacetime stage precedes the light-cone stage in the pre-temporal forcing order. Researchers deriving electromagnetic structure from recognition primitives would cite this ordering to fix the dependency hierarchy before physical time. The proof succeeds by invoking the decidable instance on the rank comparison, which reduces to a direct numerical check.
Claim. In the forcing order of pre-temporal stages, spacetime precedes the light cone: $rank(spacetime) < rank(lightCone)$.
background
The Pre-Temporal Forcing Order module records the dependency stages that exist before physical time is forced. Stage is the inductive type enumerating these stages, from distinction and recognitionInterface through symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, and onward to spacetime and lightCone. Before a b holds exactly when rank a is strictly smaller than rank b, equipped with a Decidable instance via Nat.decLt. The module documentation distinguishes recognition-light as the primitive act prior to time from physical light as the null-cone that appears only after spacetime.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This uses the Decidable instance for Before to compare the ranks of spacetime and lightCone directly.
why it matters
This result fixes spacetime before the light cone inside the pre-temporal forcing chain. It supports the module's separation of primitive recognition-light from physical light as the first boundary of spacetime. No downstream theorems depend on it yet, so it functions as a foundational ordering fact within the sequence leading to time and spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.