composition_before_rcl
plain-language theorem explainer
The pre-temporal forcing order places the compositionConsistency stage before the rcl stage. Foundation researchers tracing Recognition Science dependencies cite this when sequencing the chain from distinction through to the recognition composition law. The proof is a one-line decision that compares the numerical ranks induced by the inductive definition of Stage.
Claim. $rank( compositionConsistency ) < rank( rcl )$, where Before(a,b) holds precisely when the dependency rank of a is strictly smaller than that of b.
background
The module records a forcing order on pre-temporal stages rather than a chronological sequence. Before(a,b) is defined as rank a < rank b, with an instance of Decidable supplied by Nat.decLt. The inductive type Stage enumerates the stages in dependency order: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick.
proof idea
The proof invokes the decide tactic. This uses the Decidable instance for Before, which reduces the claim to a Nat.lt comparison on the ranks implicitly assigned by the order of constructors in Stage. The inequality holds because compositionConsistency appears before rcl in that enumeration.
why it matters
The result supplies one directed edge in the pre-temporal forcing chain that begins with distinction and ends at timeTick. It ensures the recognition composition law is downstream of composition consistency and upstream of jCost. The module as a whole supports the claim that physical time is a forced object rather than primitive, consistent with the distinction between recognition-light and physical light drawn in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.