PhysicsLogic / Minkowski 1908

The Same Interval Is Not the Same Event

A fixed Lorentz boost tests law covariance separately from physical interpretation.

Definitions and assumptions

Scope and physical limitations

Events are reference-chart (ct,x) pairs in common length units. Two inertial charts share an origin; true selects the chart with beta=3/5 and gamma=5/4, false the reference chart. The inverse boost decodes each description into that reference chart. The comparison uses the identical numerical boost either with the chart changed or with the chart fixed. It preserves every selected squared-interval constraint, not a full dynamical theory. The actual timelike example is (1,0) mapped to (5/4,-3/4), both in the future cone. Reference coordinates fix the interpretation; they are not a preferred frame of nature. This does not establish empirical event identification, general covariance, curved-spacetime gauge equivalence, or a full theory of observers.

Other arguments
Examples and distinctions

Constructed examples of this model; each answer includes the Lean statement.

Exact root statement

∀ (targetChart : Bool), (eventInterpretation targetChart).InterpretationBridge ↔ targetChart = true
Compare two arguments

Compare their definitions and hypotheses. Shared declarations may be instantiated differently; differences do not establish equivalence or implication.

No comparison argument selected.

Compare an earlier extraction

Compare the displayed specifications with an earlier JSON export. This compares text, not mathematical equivalence. Files stay in this browser.

No earlier extraction selected.

Notes and questions

Note for

Unsubmitted text stays in this tab when navigating declarations, but is not saved across reloads.

Import merges local entries without overwriting them.

All declarations in the selected argument

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structure
  • structure
  • structure
  • structure
  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

Checked statements: parameters, hypotheses, and interpretation

  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor

External mathematical declarations

  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary