recognition_light_before_time
plain-language theorem explainer
Recognition-light precedes the time tick in the pre-temporal forcing order. Researchers deriving time from prior structure in Recognition Science cite this to fix the dependency hierarchy before spacetime. The proof is a one-line decision that evaluates the rank comparison via the decidable instance on natural numbers.
Claim. The forcing priority satisfies $rank(RecognitionLight) < rank(timeTick)$, where RecognitionLight is the recognition interface stage and timeTick is the arithmetic time stage.
background
The module records the forcing order among dependency stages before physical time. Stage is the inductive type with constructors distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before (a b) is the proposition rank a < rank b, equipped with a Decidable instance via Nat.decLt.
proof idea
One-line wrapper that applies the decidable instance for Before. The decide tactic evaluates the strict inequality on the natural-number ranks of RecognitionLight and timeTick.
why it matters
The result supplies one field of the PreTemporalOrderCert record. It anchors the pre-temporal segment of the chain that later forces timeTick, J-cost, and spacetime, separating the primitive recognition act from downstream physical light.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.