composition_before_rcl
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.
claimIn 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 in Recognition Science
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.
scope and limits
- Does not prove the content of the Recognition Composition Law.
- Does not address J-cost, arithmetic objects, or time ticks.
- Does not connect to physical spacetime or the phi-ladder mass formula.
- Does not establish uniqueness of J or the phi fixed point.
formal statement (Lean)
85theorem composition_before_rcl :
86 Before Stage.compositionConsistency Stage.rcl := by
proof body
Decided by rfl or decide.
87 decide
88