PhysicalLight
plain-language theorem explainer
PhysicalLight aliases the lightCone constructor inside the Stage inductive type that encodes the pre-temporal forcing chain. Researchers tracing the dependency order before time cite it to separate the electromagnetic carrier from the earlier recognition-light stage. The definition is a direct one-line alias to Stage.lightCone.
Claim. Let $PhysicalLight$ denote the light-cone stage $Stage.lightCone$ in the pre-temporal forcing order.
background
The module records the forcing order that exists before time in Recognition Science. Because physical time is itself a forced object, the ordering is not chronological: A precedes B when B requires A as prior structure. The central distinction drawn is between recognition-light (the primitive revealing act of distinction) and physical light (the null-cone electromagnetic carrier downstream of J-cost, ticks, and spacetime). Stage is the inductive type whose constructors mark successive dependency stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, spacetime, lightCone, photonEM, and embodiedObserver.
proof idea
One-line definition that directly aliases Stage.lightCone.
why it matters
The definition supplies the concrete stage used by six downstream results, including physical_light_after_spacetime (Before Stage.spacetime PhysicalLight), recognition_light_before_physical_light, and the PreTemporalOrderCert structure. It fills the slot for the first boundary of spacetime in the forcing chain, consistent with the module's separation of pre-temporal recognition-light from physical light. The placement aligns with the T0-T8 landmarks in which spacetime (D=3) precedes the light cone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.