Foundation Pair Kernel Atomic Tick Countermodels Encoded Dist3 Triangle

The encoded distance

The triangle inequality is the rule that a direct path is never longer than a path that stops somewhere else along the way. On an ordinary three-dimensional grid, with distance measured by adding up the steps in each coordinate direction, the rule holds: the distance from point A to point C is at most the distance from A to point B plus the distance from B to point C. This is a classical fact about the L¹ metric, also called Manhattan distance, and it is what makes the grid a sensible space for measuring how far apart two locations are.

The declaration encodedDist3_triangle proves the same rule after a bookkeeping step: the three-dimensional grid is flattened into a single numbered list of sites, so that each site gets one index. The proof shows that the distance function defined on those indices still satisfies the triangle inequality. This matters because the flattening is not just a notational convenience; it is the form in which the framework's later arguments about locality and dependency are stated. Without this theorem, a step that reindexes the grid could silently break the metric structure that the rest of the framework relies on.

The theorem is a small, self-contained piece of the framework's machine-checked library of formal theorems. It does not by itself say anything about recognition, cost, or physical law. Its role is to guarantee that a technical encoding step preserves a basic geometric property. The proof works by pulling the encoded distance back to the original grid, applying the triangle inequality there, and pushing the result forward again. The statement is general: it holds for any grid size L and any three sites i, j, and k.

What the theorem does not claim is more interesting than what it does. It does not assert that the flattened grid is the physical space of three dimensions, nor that the encoding is unique or canonical. It does not say that the triangle inequality is the only property that matters for the framework's later arguments. It does not even say that the distance function is the one the framework will ultimately use for physics. It is a lemma, a supporting result, not a conclusion about the world. The framework's own documentation marks the operational locality premise as a hypothesis in production, not a theorem about nature.

The practical consequence is that the framework can safely move between the grid picture and the indexed list picture without losing the metric facts it needs. A reader who meets the flattened index in a later proof can trust that the distance notion still behaves as a distance should. The theorem is the kind of unglamorous but necessary result that lets a larger argument stand on solid ground.

/-- Triangle inequality after encoding the D=3 carrier into `Fin (L³)`. -/
theorem encodedDist3_triangle
    (L : ℕ) (i j k : Fin (L * L * L)) :
    encodedDist3 L i k ≤ encodedDist3 L i j + encodedDist3 L j k := by
  exact dist3_triangle ((enc3 L).symm i) ((enc3 L).symm j) ((enc3 L).symm k)

/-- Triangle inequality after encoding the D=3 carrier into `Fin (L³)`. -/
theorem encodedDist3_triangle
    (L : ℕ) (i j k : Fin (L * L * L)) :
    encodedDist3 L i k ≤ encodedDist3 L i j + encodedDist3 L j k := by
  exact dist3_triangle ((enc3 L).symm i) ((enc3 L).symm j) ((enc3 L).symm k)

/-- Triangle inequality after encoding the D=3 carrier into `Fin (L³)`. -/
theorem encodedDist3_triangle
    (L : ℕ) (i j k : Fin (L * L * L)) :
    encodedDist3 L i k ≤ encodedDist3 L i j + encodedDist3 L j k := by
  exact dist3_triangle ((enc3 L).symm i) ((enc3 L).symm j) ((enc3 L).symm k)

What this page does not claim

The flattened grid is not asserted to be the physical space of three dimensions. The encoding is not claimed to be unique or canonical. The triangle inequality is not claimed to be the only property that matters for the framework's later arguments.

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/Foundation/PairKernelAtomicTickCountermodels.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: