Physics Light Cone Causality From Rs

Causal relations in the light cone

In special relativity, the light cone around an event is the set of points reachable by light, and it organizes all possible cause and effect. The cone has an interior, an exterior, and a surface, and these give five canonical ways two events can be related. Two events are timelike separated if one lies inside the other's cone, meaning a signal could connect them. They are spacelike separated if neither lies in the other's cone, so no signal can connect them. They are lightlike (or null) separated if they lie exactly on each other's cone surface. Finally, an event can sit on the past boundary or the future boundary of another's cone, marking the two halves of that surface.

This fivefold classification is standard physics, taught in every relativity course. The Recognition Science framework's contribution is to make the count precise and machine-checked. Its library, a machine-checked collection of formal theorems, defines an inductive type called CausalRelation with exactly those five constructors: timelike, spacelike, lightlike, pastBoundary, futureBoundary. It then proves a theorem, causalRelation_count, that the cardinality of this type is 5. The proof is by decide, meaning the computer evaluates the finite case directly. The file reports 0 sorry and 0 axiom, so the count rests entirely on the kernel's standard rules.

The five relations are not arbitrary labels. They are the exhaustive answer to a single question: given two events, what causal connection is possible? The interior of the cone admits signals, the exterior forbids them, and the surface is the limiting case where light itself barely connects them. The past and future boundaries distinguish whether the connection runs forward or backward in time. This classification is what makes the light cone the backbone of relativistic causality, and the framework's theorem pins down that there are no hidden sixth or seventh cases.

In Recognition Science, this result sits inside a larger program that derives physical structure from a discrete ledger of recognition events. The five relations are a small but load-bearing piece: they give a finite, exact vocabulary for how events can influence one another. The theorem does not derive the light cone from first principles; it takes the standard relativistic picture and proves the count of its relation types. What the framework adds is certainty about the enumeration, not a new physics of the cone itself.

The practical payoff is that any later framework construction involving causality can rely on this closed set of five relations. When a builder needs to classify event pairs, the machine-checked theorem guarantees the list is complete and no case is missing. That is a modest but real foundation stone: the classification is not assumed, it is proved.

inductive CausalRelation where
  | timelike
  | spacelike
  | lightlike
  | pastBoundary
  | futureBoundary
  deriving DecidableEq, Repr, BEq, Fintype

theorem causalRelation_count : Fintype.card CausalRelation = 5 := by decide

theorem causalRelation_count : Fintype.card CausalRelation = 5 := by decide

theorem causalRelation_count : Fintype.card CausalRelation = 5 := by decide

What this page does not claim

The framework does not derive the light cone from recognition cost; it classifies relations within the standard relativistic picture. The five relations are not shown to be physically exhaustive beyond the mathematical definition of the inductive type. No claim is made about the physical bridge from recognition events to spacetime geometry.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/LightConeCausalityFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: