recognition_before_predicate
plain-language theorem explainer
Recognition Science places the recognition interface stage before the single-valued predicate stage in its pre-temporal forcing order. Researchers tracing the dependency chain from distinction onward would cite this result. The proof reduces to a single decision on the rank comparison via the built-in decidability instance.
Claim. In the pre-temporal forcing order, the recognition interface stage precedes the single-valued predicate stage: $rank(recognitionInterface) < rank(singleValuedPredicate)$.
background
The module records a forcing order on dependency stages that must precede the emergence of time. Stage is the inductive enumeration of these stages beginning with distinction, followed by recognitionInterface and singleValuedPredicate. Before a b is defined as rank a < rank b, equipped with a Decidable instance from Nat.decLt.
proof idea
One-line wrapper that invokes the Decidable instance for Before, reducing the claim to a Nat.lt comparison that decide resolves directly.
why it matters
This theorem supplies an early link in the pre-temporal forcing chain inside the module. It sits between distinction_first and predicate_before_symmetry, supporting the sequence that later reaches the Recognition Composition Law and J-cost. The module distinguishes recognition-light (primitive) from physical light (downstream of spacetime).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.