composition_before_rcl
plain-language theorem explainer
The theorem places the composition consistency stage before the recognition composition law in the pre-temporal forcing order. Researchers tracing the dependency sequence from distinction through symmetric comparison to the RCL functional equation would cite this ordering. The proof is a one-line decidability check on the rank comparison.
Claim. In the pre-temporal forcing order, the composition consistency stage precedes the recognition composition law: rank(composition consistency) < rank(recognition composition law).
background
The module records a forcing order on dependency stages that exist prior to time. Stage is the inductive type listing these stages in sequence: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before a b is the proposition rank a < rank b, equipped with a decidable instance via Nat.lt. The local setting distinguishes recognition-light (primitive distinction) from physical light (downstream of J-cost and spacetime).
proof idea
The proof is a one-line wrapper that applies the decidable instance for Before, reducing the claim to a direct Nat.lt comparison on the ranks of the two stages.
why it matters
This ordering result belongs to the main sequence of theorems that establish prerequisites for the Recognition Composition Law. It ensures composition consistency is available before the RCL equation J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) is introduced, fitting the pre-temporal chain that later reaches the eight-tick octave and D = 3. No downstream uses are recorded in the current module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.