RecognitionLight
plain-language theorem explainer
RecognitionLight names the pre-temporal stage of the revealing act that makes distinction available. Researchers tracing the forcing order before time cite this definition to separate primitive recognition from later physical light and spacetime. The definition is a direct one-line alias to the recognitionInterface constructor of the Stage inductive type.
Claim. Let the recognition stage be the recognitionInterface constructor of the inductive type Stage that enumerates pre-temporal dependency stages.
background
The module records the forcing order that exists before time in Recognition Science. Recognition-light is the primitive revealing act of distinction, prior to time and spacetime, while physical light is the null-cone electromagnetic carrier downstream of J-cost, ticks, and spacetime. Stage is the inductive type of dependency stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick.
proof idea
One-line definition that aliases the recognitionInterface constructor of Stage.
why it matters
This definition anchors the pre-temporal forcing order and feeds the structure PreTemporalOrderCert together with the three before theorems that place recognition light prior to timeTick, spacetime, and physical light. It directly implements the module distinction between recognition-light as pre-temporal and physical light as the first boundary of spacetime. The placement aligns with the overall forcing chain in which time and D=3 emerge after recognition and J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.