predicate_before_symmetry
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not assign concrete numerical ranks to any stage.
- Does not address physical time or spacetime structure.
- Does not derive J-cost, RCL, or mass formulas.
- Does not interact with post-temporal physical constants.
formal statement (Lean)
77theorem predicate_before_symmetry :
78 Before Stage.singleValuedPredicate Stage.symmetricComparison := by
proof body
Decided by rfl or decide.
79 decide
80