Verification Metric From Units Cert

The metric certificate

A metric is a rule that assigns a distance-like number to pairs of points, and in special relativity the relevant metric is the Minkowski metric, which separates spacetime into timelike, spacelike, and lightlike separations. The metric-from-units certificate is a small, machine-checked module in the Recognition Science library that shows the framework's internal units already determine such a metric, with no extra assumptions bolted on. The module defines a minimal four-dimensional vector, a symmetric bilinear evaluation as the metric interface, and instantiates it with the Minkowski signature (-c², +1, +1, +1) in coordinates (t, x, y, z).

The central fact it establishes is that the anchor vector (τ₀, ℓ₀, 0, 0), built from the framework's time and length units, is null under this metric: its squared norm is zero. This holds because the framework's units carry a built-in cone bound, the relation c · τ₀ = ℓ₀, which states that the speed parameter times the fundamental time unit equals the fundamental length unit. The proof is a short algebraic identity: substituting ℓ₀ = c · τ₀ into -c²τ₀² + ℓ₀² gives zero identically.

In Recognition Science, this certificate is the first non-scaffold milestone on a checklist for deriving the metric from the ledger, the framework's discrete record of recognition events. It does not derive the metric from first principles; it verifies consistency: if the units satisfy the cone bound, then the Minkowski metric they determine has the expected light-cone structure. The certificate is deliberately minimal, using no imports from any relativity geometry module, so it provides an independent check that the framework's units are compatible with a standard relativistic metric.

For a reader, the practical consequence is that the framework's foundational constants are not arbitrary: they are constrained so that a light-cone condition holds automatically. This means the framework's internal units already encode a speed parameter and a relation that matches the structure of special relativity, a necessary condition for any later claim that the framework reproduces spacetime geometry. The module does not yet prove the full bridge from recognition to metric; it proves a single, clean consistency fact that such a bridge must satisfy.

/-- Minimal symmetric “metric” interface: an evaluation pairing plus symmetry. -/
structure Metric4 where
  eval : Vec4 → Vec4 → ℝ
  symm : ∀ v w : Vec4, eval v w = eval w v

/-- Minkowski bilinear evaluation with signature `(-c^2, +1, +1, +1)` in coordinates
`(t, x, y, z)`. -/
def minkowskiEval (c : ℝ) (v w : Vec4) : ℝ :=
  -(c ^ 2) * v.t * w.t + v.x * w.x + v.y * w.y + v.z * w.z

/-- The anchor vector is null for every RSUnits pack (by the built-in cone bound). -/
lemma anchorsVec_null (U : RSUnits) :
    normSq (minkowskiMetric U.c) (anchorsVec U) = 0 := by
  -- RSUnits contains the cone bound `c * τ0 = ℓ0` as a field.
  simpa [anchorsVec] using anchorsVec_null_of_cone U.c U.tau0 U.ell0 U.c_ell0_tau0

lemma anchorsVec_null_of_cone (c τ ℓ : ℝ) (h : c * τ = ℓ) :
    normSq (minkowskiMetric c) { t := τ, x := ℓ, y := 0, z := 0 } = 0 := by
  unfold normSq minkowskiMetric minkowskiEval
  -- reduce to `-(c^2)*τ^2 + ℓ^2 = 0` and rewrite `ℓ = c*τ`
  simp [pow_two, h.symm]
  ring

What this page does not claim

This certificate does not derive the Minkowski metric from first principles; it verifies consistency given the cone bound. This module does not prove the full bridge from the recognition ledger to spacetime geometry. The certificate does not establish that the speed parameter c equals the physical speed of light.

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/Verification/MetricFromUnitsCert.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: