Stage
plain-language theorem explainer
Stage enumerates the thirteen dependency stages in the pre-temporal forcing chain of Recognition Science. Researchers establishing logical priority before time would cite this inductive type to ground order theorems such as distinction_first. The definition is a direct inductive listing of constructors with no additional structure or proof obligations.
Claim. The pre-temporal forcing stages form an inductive type whose constructors are: distinction, recognition interface, single-valued predicate, symmetric comparison, composition consistency, recognition composition law, J-cost, arithmetic object, time tick, spacetime, light cone, photon electromagnetic, and embodied observer.
background
This module records the logical dependency order that exists before physical time in Recognition Science. The ordering is a forcing relation: later stages require earlier ones as prior structure. Recognition-light (the primitive act of distinction) is placed first, while physical light (null-cone and photon) appears later after J-cost and ticks. The rank function assigns natural numbers to these stages, with distinction at 0 and embodied observer at 12, so that Before a b holds precisely when rank a < rank b.
proof idea
This is an inductive definition that enumerates the stages. It supplies the constructors used by the sibling rank definition and by downstream theorems such as distinction_first and Before.
why it matters
Stage supplies the enumeration required by the sequence of order theorems in this module, including distinction_first, composition_before_rcl, jCost_before_arithmetic, and arithmetic_before_time. It occupies the initial position in the forcing chain that leads to the eight-tick octave and D = 3. The definition leaves open the explicit derivation of J-uniqueness and the phi-ladder from these stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.