recognition_before_predicate
plain-language theorem explainer
The result places the recognition interface stage ahead of the single-valued predicate stage in the pre-temporal forcing order. Workers on the Recognition Science chain from distinction to time would cite it to fix one link in the dependency sequence. The proof is a one-line decision that confirms the rank inequality via the decidable instance of the Before relation.
Claim. In the pre-temporal forcing chain, the recognition interface stage precedes the single-valued predicate stage, meaning its dependency rank is strictly smaller: $rank(recognitionInterface) < rank(singleValuedPredicate)$.
background
The module records a forcing order among dependency stages that must be in place before physical time appears. Stage is the inductive enumeration of these stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before is the relation that holds when the rank of the first stage is less than the rank of the second; an instance makes the relation decidable by reduction to Nat.lt. The module doc states that A is before B precisely when B requires A as prior structure, and distinguishes recognition-light (pre-temporal) from physical light (post-spacetime).
proof idea
One-line wrapper that applies the decidable instance of Before, which reduces the claim to a direct comparison of the natural-number ranks assigned to the two stages.
why it matters
The theorem is one of the main order theorems that populate the pre-temporal sequence listed in the module. It contributes the second link after distinction, supporting the overall claim that recognition-light is the first item in the forcing chain. No downstream uses are recorded in the current graph, but the result is required for the subsequent theorems predicate_before_symmetry through time_before_spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.