Physics Lorentz Invariance From Jcost

Lorentz invariance and its cost

The Lorentz factor is the quantity in special relativity that stretches time and shrinks lengths as an object's speed approaches the speed of light. It appears in the time dilation and length contraction formulas, and it grows without bound as speed nears the speed of light, which is why nothing with mass can reach that speed: the energy required would become infinite.

The factor was introduced by Hendrik Lorentz in 1895 to explain the null result of the Michelson-Morley experiment, and Albert Einstein derived it independently in 1905 from the two postulates of special relativity. In modern physics, the factor is not an empirical fit but a consequence of the symmetry that the speed of light is the same for all observers in uniform relative motion. That symmetry, Lorentz invariance, is the foundational principle of special relativity.

In Recognition Science, the framework models a ledger, a discrete record of events, and assigns a cost, a measure of how far a recorded value is from the true value. The framework's central cost function is J(x) = (x + 1/x)/2 − 1, which is zero when the recorded value equals the true value and positive otherwise. The module in question defines domainCost as J(measured / expected), so it measures the cost when a measured value differs from an expected one.

What the module actually proves is three general facts about this cost function. First, the cost is zero when the measured value equals the expected value: domainCost r r = 0. Second, the cost is never negative for positive inputs: 0 ≤ domainCost m e whenever m and e are both positive. Third, the quantity φ − 3/2 is positive, where φ is the golden ratio. These three facts are collected into a structure called LorentzInvCert, and the module proves that this structure is inhabited.

The module does not prove anything specific to Lorentz invariance, because domainCost is defined as J(m/e) without any reference to the Lorentz factor or to special relativity. The docstring states this plainly: the code proves general facts about the cost function, and what would make it a theorem about Lorentz invariance is a definition of m and e in the subject's own terms. The intended connection, that the Lorentz factor could be expressed as a J-cost on the v/c ratio, remains a research note, not a result.

theorem domainCost_at_equilibrium (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (measured expected : ℝ) : ℝ := Jcost (measured / expected)

What this page does not claim

The module does not prove that the Lorentz factor equals J(v/c) or any similar physical identity. The module does not establish Lorentz invariance as a physical principle; it only proves properties of a cost function. The golden ratio threshold φ − 3/2 is not shown to have any physical significance for Lorentz invariance.

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/LorentzInvarianceFromJCost.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: