predicate_before_symmetry
plain-language theorem explainer
The theorem places the single-valued predicate stage before the symmetric comparison stage in the pre-temporal forcing order. Foundation workers tracing Recognition Science dependencies cite this link when building the sequence from distinction through composition to time. The proof is a one-line decision that evaluates the rank inequality via the decidable instance on natural numbers.
Claim. In the pre-temporal forcing order, the single-valued predicate stage precedes the symmetric comparison stage: $rank(singleValuedPredicate) < rank(symmetricComparison)$.
background
The PreTemporalForcingOrder module records forcing dependencies that exist before physical time is constructed. Its Stage inductive type lists the layers: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. The Before relation is defined by rank a < rank b together with a decidable instance that reduces to Nat.decLt.
proof idea
The proof is a one-line wrapper that applies the decidable instance for Before. The instance is supplied directly by the definition of Before as a strict inequality on natural-number ranks, so decide evaluates the comparison and closes the goal.
why it matters
This result occupies the slot between recognition_before_predicate and symmetry_before_composition in the pre-temporal chain. It supplies the required ordering that later stages (rcl, jCost, arithmetic, timeTick) presuppose, consistent with the forcing sequence that ultimately yields the eight-tick octave and three spatial dimensions. No open questions are attached to this link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.