`Hyperfields/Exact.lean`

Explanation legend

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

11 declarations, 0 contain sorry, 0 axioms

Exact rationals as scaled integers

A metric space needs exact distances. Lean 4 core has Rat, but Rat equality does not reduce for decide: the kernel's evaluator will not normalize a rational, so a decision procedure over rational values never finishes.

The representation that does reduce is a pair of integers over a shared positive denominator. A value a / d is compared with b / e by cross-multiplication:

a / d  ≤  b / e   ⟺   a * e  ≤  b * d

Int multiplication and comparison both reduce, so the comparison is decidable and by decide works over it.

The shared denominator matters. Two values with different denominators cannot be compared by cross-multiplication without a common denominator, so every value in one metric space is held over the same positive denominator. That is exactly what a finite matrix of distances needs: one scale for the whole matrix, and each entry is an integer numerator over that scale.

This is a representation, not a claim that rationals are integers. The denominator is part of the data, and a value is only meaningful relative to the scale it was declared with.

Imports (1)

Imported by 2 files

structure Hyperfields.Exact.Scale A shared denominator line 38 source
The scale of a rational: a strictly positive shared denominator.

Every value in one matrix is written over the same denominator, so comparing two of them is comparing two integers.

no axioms what this means
```
structure Scale where
…
```
def Hyperfields.Exact.Scale.usable A scale must be positive line 51 source
Whether a scale is usable: its denominator must be strictly positive.
A zero or negative denominator would make the cross-multiplication comparison meaningless, because it would reverse the order.

Dividing by a negative number reverses the order, so a non-positive denominator would make the comparison mean the opposite of what it says.
Prerequisites: Hyperfields.Exact.Scale

no axioms what this means
Statement uses: Hyperfields.Exact.Scale, Bool
Proof uses: Decidable.decide, LT.lt, Int, OfNat.ofNat, Hyperfields.Exact.Scale.denominator
3 instances, coercions and auxiliary constants left out.
```
def Scale.usable (scale : Scale) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale
structure Hyperfields.Exact.Value A numerator over a scale line 58 source
A rational value: a numerator over a shared scale.

The value is the numerator; the denominator lives in the scale, so two values over one scale are directly comparable.
Prerequisites: Hyperfields.Exact.Scale

no axioms what this means
Statement uses: Hyperfields.Exact.Scale
```
structure Value (scale : Scale) where
…
```
Mentions: Hyperfields.Exact.Scale
def Hyperfields.Exact.Value.le Compare two values line 72 source
Compare two values over the same scale.
a / d ≤ b / d is a ≤ b when d is positive, because dividing by a positive number preserves the order. The general cross-multiplication is written out below so the reason is visible.

Over one positive denominator, a over d is at most b over d exactly when a is at most b.
Prerequisites: Hyperfields.Exact.Scale, Hyperfields.Exact.Value

no axioms what this means
Statement uses: Hyperfields.Exact.Scale, Hyperfields.Exact.Value, Bool
Proof uses: Bool.and, Hyperfields.Exact.Scale.usable, Decidable.decide, LE.le, Int, Hyperfields.Exact.Value.numerator
2 instances, coercions and auxiliary constants left out.
```
def Value.le (scale : Scale) (left right : Value scale) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.Value.eq Equality over one scale line 79 source
Whether two values over the same scale are equal.

Two numerators over the same denominator are equal exactly when the numerators are equal.
Prerequisites: Hyperfields.Exact.Scale, Hyperfields.Exact.Value

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hyperfields.Exact.Scale, Hyperfields.Exact.Value, Bool
Proof uses: BEq.beq, Int, Hyperfields.Exact.Value.numerator
4 instances, coercions and auxiliary constants left out.
```
def Value.eq (scale : Scale) (left right : Value scale) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.Value.add Add two values line 86 source
The sum of two values over the same scale.

Adding numerators over a shared denominator adds the values, because the denominator is common.
Prerequisites: Hyperfields.Exact.Scale, Hyperfields.Exact.Value

no axioms what this means
Statement uses: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
Proof uses: Hyperfields.Exact.Value.mk, HAdd.hAdd, Int, Hyperfields.Exact.Value.numerator
2 instances, coercions and auxiliary constants left out.
```
def Value.add (scale : Scale) (left right : Value scale) : Value scale :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.distance Read one distance line 98 source
The distance between two points, as a numerator over the matrix scale.
The metric matrix stores numerators over one shared scale, so the distance is a lookup rather than a computation.

The matrix already stores the distances, so reading one is a lookup and an index outside the matrix is nothing rather than a guess.
Prerequisites: Hyperfields.Exact.Scale, Hyperfields.Exact.Value

standard axioms: propext what this means
Statement uses: Hyperfields.Exact.Scale, List, Hyperfields.Exact.Value, Nat, Option
Proof uses: Hyperfields.Exact.distance.match_1, GetElem?.getElem?, LT.lt, List.length, Unit, Option.none
2 instances, coercions and auxiliary constants left out.
```
def distance (scale : Scale) (matrix : List (List (Value scale))) (row column : Nat) : Option (Value scale) :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.positiveOffDiagonal Every entry is positive line 109 source
Whether every matrix entry is a strictly positive distance.

A distance is positive, so every stored numerator must be greater than zero.
Prerequisites: Hyperfields.Exact.Value

no axioms what this means
Statement uses: Hyperfields.Exact.Scale, List, Hyperfields.Exact.Value, Bool
Proof uses: List.all, Decidable.decide, LT.lt, Int, OfNat.ofNat, Hyperfields.Exact.Value.numerator
3 instances, coercions and auxiliary constants left out.
```
def positiveOffDiagonal {scale : Scale} (matrix : List (List (Value scale))) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.separation Separation line 120 source
Whether the matrix satisfies separation: zero exactly on the diagonal and strictly positive off it.

A point is at distance zero from itself and from nothing else, which is what separates distinct points.
Prerequisites: Hyperfields.Exact.Value

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hyperfields.Exact.Scale, Nat, List, Hyperfields.Exact.Value, Bool
Proof uses: List.all, List.range, ite, Eq, BEq.beq, Bool.true, Hyperfields.Exact.separation.match_1, Option, Option.bind, GetElem?.getElem?, LT.lt, List.length, Int, Hyperfields.Exact.Value.numerator, OfNat.ofNat, Unit, Bool.false, Decidable.decide
12 instances, coercions and auxiliary constants left out.
```
def separation {scale : Scale} (n : Nat) (matrix : List (List (Value scale))) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.symmetric Symmetry line 141 source
Whether the matrix is symmetric.
Symmetry is checked on the whole matrix, not just one triangle, because a one-triangle check would leave the other triangle unchecked.

The distance from i to j is the distance from j to i, and the check reads both triangles so neither is left unchecked.
Prerequisites: Hyperfields.Exact.Value

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hyperfields.Exact.Scale, Nat, List, Hyperfields.Exact.Value, Bool
Proof uses: List.all, List.range, Hyperfields.Exact.symmetric.match_1, Option, Option.bind, GetElem?.getElem?, LT.lt, List.length, BEq.beq, Int, Hyperfields.Exact.Value.numerator, Bool.false
6 instances, coercions and auxiliary constants left out.
```
def symmetric {scale : Scale} (n : Nat) (matrix : List (List (Value scale))) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value
def Hyperfields.Exact.triangleInequality The triangle inequality line 165 source
Whether the matrix satisfies the triangle inequality.
For every ordered triple i, j, k:
```
d(i, j)  ≤  d(i, k) + d(k, j)
```
This is the axiom that makes a distance a distance. Dropping it would leave a symmetric non-negative matrix that is not a metric, and every geometry that transports along paths depends on it.
Going through a third point is never shorter than going directly, and this is the axiom that makes a distance a distance.
Prerequisites: Hyperfields.Exact.Value, Hyperfields.Exact.distance

standard axioms: propext what this means
Statement uses: Hyperfields.Exact.Scale, Nat, List, Hyperfields.Exact.Value, Bool
Proof uses: List.all, List.range, Hyperfields.Exact.triangleInequality.match_1, Option, Hyperfields.Exact.distance, Decidable.decide, LE.le, Int, Hyperfields.Exact.Value.numerator, HAdd.hAdd, Bool.false
4 instances, coercions and auxiliary constants left out.
```
def triangleInequality {scale : Scale} (n : Nat) (matrix : List (List (Value scale))) : Bool :=
…
```
Mentions: Hyperfields.Exact.Scale, Hyperfields.Exact.Value