Hypergeometry.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

22 declarations, 0 contain sorry, 0 axioms

Hypergeometry

[FRAME] Exact finite chart geometry; no physical geometry is asserted.

This is the Lean port of the local hypergeometry candidate. It carries the finite metric-space frame and the properties that frame establishes.

Distances are exact. Lean 4 core has Rat, but Rat equality does not reduce for decide, so a decision procedure over rational distances never finishes. The port therefore holds every distance as an integer numerator over one shared positive denominator, exactly as Hyperfields.Exact describes. The cross-multiplication comparison is then decidable and the compiler checks the metric axioms.

What is proved here is finite and mechanical: that a concrete matrix is a metric, that a concrete permutation of points is an isometry, that transporting a point along a path lands where the path says, and that a cycle of transports returns a point to itself exactly when the cycle's composed mapping is the identity.

What is not proved here, and cannot be, is any claim that physical space has this structure. The frame is a finite carrier with a chosen distance matrix. It does not say that the universe is a manifold, that these are the right charts, or that the finite models here are the intended ones. The Python source carries the same [FRAME] classification and this port keeps it: a finite consistency result is not a foundation.

Imports (3)

Imported by 1 file

Hyperfields/AllFields.lean

structure Hyperfields.Fields.Hypergeometry.MetricSpace A finite metric space over a fixed carrier line 59 source
A finite metric space over a carrier of n points.
The matrix holds the distances as numerators over one shared scale, so the scale is part of the structure and every distance in one matrix is comparable with every other. wellShaped is where the metric axioms are checked.
The structure derives DecidableEq but not BEq, because BEq on a Value would need a LawfulBEq instance for the scale, and the scale is a parameter rather than a fixed type. Every comparison the port makes is an explicit numerator comparison, so no lawfulness obligation is smuggled in.

The carrier's size is part of its type and the distances are exact, so a metric space is a decidable object rather than a promise.

no axioms what this means
Statement uses: Nat
```
structure MetricSpace (n : Nat) where
…
```
def Hyperfields.Fields.Hypergeometry.MetricSpace.wellShaped The axioms a metric space must satisfy line 80 source
Whether the matrix satisfies the metric axioms.
The four axioms are checked here rather than assumed:
1. Separation: the distance is zero exactly on the diagonal.
2. Symmetry: d(i, j) = d(j, i).
3. The triangle inequality: d(i, j) ≤ d(i, k) + d(k, j).
4. A usable scale: the shared denominator is strictly positive.
The scale check is not decoration. Cross-multiplication over a non-positive denominator would reverse the order, and every comparison in the module would then be meaningless.
A metric is zero exactly on the diagonal, positive off it, symmetric, and satisfies the triangle inequality; a frame that drops any of these is not a metric.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypergeometry.MetricSpace, Bool
Proof uses: Bool.and, Hyperfields.Exact.Scale.usable, Hyperfields.Fields.Hypergeometry.MetricSpace.scale, Hyperfields.Exact.separation, Hyperfields.Fields.Hypergeometry.MetricSpace.matrix, Hyperfields.Exact.symmetric, Hyperfields.Exact.triangleInequality
```
def MetricSpace.wellShaped {n : Nat} (space : MetricSpace n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypergeometry.MetricSpace
def Hyperfields.Fields.Hypergeometry.sameDistance Two points at the same distance line 99 source
Whether two distances are the same.
The two distances may come from different metric spaces, and therefore from different scales. The comparison is on the numerators, which is exactly right when the two scales agree, and is the comparison the port makes: every isometry in this module is between spaces that share a scale, and the scale is part of the data so a mismatch is visible rather than silently absorbed.

Two pairs are the same distance when the stored numerators agree, which is a comparison over one shared scale.
Prerequisites: 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 sameDistance {leftScale rightScale : Scale}
    (left : Value leftScale) (right : Value rightScale) : Bool :=
…
```
structure Hyperfields.Fields.Hypergeometry.ChartTransition A chart transition between two metric spaces line 116 source
A chart transition: a bijection of points between two metric spaces that preserves every distance.
The mapping is a list of pairs. isIsometry is where the distance preservation is checked.

A chart transition is a point-for-point correspondence that preserves distance exactly, not approximately.

no axioms what this means
Statement uses: Nat
```
structure ChartTransition (m n : Nat) where
…
```
def Hyperfields.Fields.Hypergeometry.lookup Read one entry line 126 source
Look up the image of a point in a transition's mapping.

A coordinate outside the matrix has no entry, which is nothing rather than a default.
Prerequisites: Hyperfields.Exact.Value

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Fin, Option
Proof uses: Hyperfields.Fields.Hypergeometry.lookup.match_1, List.find?, BEq.beq, Prod.fst, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def lookup {m n : Nat} (mapping : List (Fin m × Fin n)) (point : Fin m) : Option (Fin n) :=
…
```
def Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry The distance a mapping preserves line 141 source
Whether the transition's mapping preserves every distance.
The mapping must be total and single valued on the source, bijective onto the target, and preserve the distance between every pair. The last condition is checked pair by pair over the whole carrier, because an isometry that preserved only some distances would not be one.

An isometry must preserve the distance between every pair of points, not merely carry points across.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hypergeometry.ChartTransition, Bool
Proof uses: List, Fin, Hyperfields.Finite.carrier, Prod, Hyperfields.Fields.Hypergeometry.ChartTransition.mapping, Bool.and, BEq.beq, List.length, List.all, Hyperfields.Finite.mem, Prod.fst, Prod.snd, List.eraseDups, List.map, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry.match_2, Option, Hyperfields.Fields.Hypergeometry.lookup, Unit, Bool.false, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry.match_1 and 7 more
7 instances, coercions and auxiliary constants left out.
```
def ChartTransition.isIsometry {m n : Nat} (transition : ChartTransition m n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hypergeometry.ChartTransition
def Hyperfields.Fields.Hypergeometry.transportPath Transporting a point along a path of transitions line 178 source
Transport a point along a path of chart transitions.
The path is a list of transitions over one carrier size. A path that crosses between spaces of different sizes has no meaning here, because there is no chart to carry the point into.

A path composes chart by chart, and each step must actually be defined for the point it carries.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, List, Hyperfields.Fields.Hypergeometry.ChartTransition, Option
Proof uses: List.foldl, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry.match_2, Unit, Option.none, Hyperfields.Fields.Hypergeometry.lookup, Hyperfields.Fields.Hypergeometry.ChartTransition.mapping, Option.some
```
def transportPath {n : Nat} (point : Fin n)
    (transitions : List (ChartTransition n n)) : Option (Fin n) :=
…
```
Mentions: Hyperfields.Fields.Hypergeometry.ChartTransition
def Hyperfields.Fields.Hypergeometry.twoPoint The two-point metric line 197 source
The two-point metric: two points at distance one.
The distances are numerators over a shared scale of one, so 1 means one unit of the matrix scale and 0 means zero.

A concrete metric lets the compiler check the axioms against something a reader can see.

no axioms what this means
Statement uses: Hyperfields.Fields.Hypergeometry.MetricSpace, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypergeometry.MetricSpace.mk, Hyperfields.Exact.Scale.mk, Int, List.cons, List, Hyperfields.Exact.Value, Hyperfields.Exact.Value.mk, List.nil
3 instances, coercions and auxiliary constants left out.
```
def twoPoint : MetricSpace 2 where
…
```
Mentions: Hyperfields.Fields.Hypergeometry.MetricSpace
def Hyperfields.Fields.Hypergeometry.threePoint The three-point chain metric line 213 source
The three-point metric: points a, b, c with distances 1, 2, and 1.
The triangle inequality is not automatic here. The distance from a to c is 2, and the two-step path through b is 1 + 1, so the inequality holds exactly at the boundary.

A three-point metric with unequal distances exercises the triangle inequality in a way the two-point case cannot.

no axioms what this means
Statement uses: Hyperfields.Fields.Hypergeometry.MetricSpace, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypergeometry.MetricSpace.mk, Hyperfields.Exact.Scale.mk, Int, List.cons, List, Hyperfields.Exact.Value, Hyperfields.Exact.Value.mk, List.nil
3 instances, coercions and auxiliary constants left out.
```
def threePoint : MetricSpace 3 where
…
```
Mentions: Hyperfields.Fields.Hypergeometry.MetricSpace
def Hyperfields.Fields.Hypergeometry.twoPointIdentity The identity transition line 224 source
The identity transition on the two-point metric.

The identity on a metric space is always an isometry, which is the baseline the other transitions are measured against.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypergeometry.ChartTransition, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypergeometry.ChartTransition.mk, Hyperfields.Fields.Hypergeometry.twoPoint, List.cons, Prod, Fin, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def twoPointIdentity : ChartTransition 2 2 where
…
```
Mentions: Hyperfields.Fields.Hypergeometry.ChartTransition
def Hyperfields.Fields.Hypergeometry.twoPointSwap The swap transition line 232 source
The transition that swaps the two points of the two-point metric.

Swapping two equidistant points preserves every distance, which is the smallest non-trivial isometry.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hypergeometry.ChartTransition, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hypergeometry.ChartTransition.mk, Hyperfields.Fields.Hypergeometry.twoPoint, List.cons, Prod, Fin, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def twoPointSwap : ChartTransition 2 2 where
…
```
Mentions: Hyperfields.Fields.Hypergeometry.ChartTransition
theorem Hyperfields.Fields.Hypergeometry.two_point_is_a_metric The two-point metric satisfies the axioms line 240 source
The two-point metric satisfies the metric axioms.

The concrete example must clear the axioms the frame demands, or the example proves nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.MetricSpace.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.twoPoint, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 241
  before
```
⊢ twoPoint.wellShaped = true
```
  after
  no goals remain
```
theorem two_point_is_a_metric : twoPoint.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypergeometry.three_point_is_a_metric The three-point metric satisfies the axioms line 246 source
The three-point metric satisfies the metric axioms.

The concrete example must clear the axioms the frame demands, or the example proves nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.MetricSpace.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.threePoint, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 247
  before
```
⊢ threePoint.wellShaped = true
```
  after
  no goals remain
```
theorem three_point_is_a_metric : threePoint.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hypergeometry.triangle_violation_is_rejected A matrix that violates the triangle inequality is rejected line 259 source
A matrix whose long edge exceeds the two-step path is not a metric.
This is the negative case. A checker that never rejects anything is not a check, and this theorem is what makes the positive cases meaningful. The distance from a to c is 3, while the path through b is 1 + 1, so the triangle inequality fails.

The metric check must be able to fail, or it certifies nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.MetricSpace.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.MetricSpace.mk, Hyperfields.Exact.Scale.mk, Int, List.cons, List, Hyperfields.Exact.Value, Hyperfields.Exact.Value.mk, List.nil, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
5 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 266
  before
```
⊢ { scale := { denominator := 1 },
        matrix :=
          [[{ numerator := 0 }, { numerator := 1 }, { numerator := 3 }],
            [{ numerator := 1 }, { numerator := 0 }, { numerator := 1 }],
            [{ numerator := 3 }, { numerator := 1 }, { numerator := 0 }]] }.wellShaped =
    false
```
  after
  no goals remain
```
theorem triangle_violation_is_rejected :
    ({ scale := { denominator := 1 },
…
```
theorem Hyperfields.Fields.Hypergeometry.two_point_identity_is_an_isometry The identity transition is an isometry line 271 source
The identity transition on the two-point metric is an isometry.

Carrying a point to itself preserves every distance, because the distance to itself was already that distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.twoPointIdentity, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 273
  before
```
⊢ twoPointIdentity.isIsometry = true
```
  after
  no goals remain
```
theorem two_point_identity_is_an_isometry :
    twoPointIdentity.isIsometry = true := by
…
```
theorem Hyperfields.Fields.Hypergeometry.two_point_swap_is_an_isometry The swap transition is an isometry line 278 source
The swap transition on the two-point metric is an isometry.

The two points are equidistant, so exchanging them preserves the one distance that exists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.twoPointSwap, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 280
  before
```
⊢ twoPointSwap.isIsometry = true
```
  after
  no goals remain
```
theorem two_point_swap_is_an_isometry :
    twoPointSwap.isIsometry = true := by
…
```
theorem Hyperfields.Fields.Hypergeometry.a_collapsing_transition_is_rejected A non-isometry is rejected line 291 source
A transition that collapses two distinct points is not an isometry.
The map sends both points to the same target point, so the distance between them, which was one, becomes zero. That is the negative case that gives the positive cases their force.

An isometry check must be able to fail, or it certifies nothing.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hypergeometry.ChartTransition.isIsometry, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.ChartTransition.mk, Hyperfields.Fields.Hypergeometry.twoPoint, List.cons, Prod, Fin, Prod.mk, List.nil, Bool.false
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 294
  before
```
⊢ { source := twoPoint, target := twoPoint, mapping := [(0, 0), (1, 0)] }.isIsometry = false
```
  after
  no goals remain
```
theorem a_collapsing_transition_is_rejected :
    ({ source := twoPoint, target := twoPoint, mapping := [(0, 0), (1, 0)] } :
…
```
Mentions: Hyperfields.Fields.Hypergeometry.twoPoint
theorem Hyperfields.Fields.Hypergeometry.transport_through_swap Transporting through the swap line 299 source
Transporting the first point through the swap lands it on the second.

Transport carries a point chart by chart, and the swap sends each point to the other.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.transportPath, List.cons, Hyperfields.Fields.Hypergeometry.ChartTransition, Hyperfields.Fields.Hypergeometry.twoPointSwap, List.nil, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 301
  before
```
⊢ transportPath 0 [twoPointSwap] = some 1
```
  after
  no goals remain
```
theorem transport_through_swap :
    transportPath 0 [twoPointSwap] = some 1 := by
…
```
Mentions: Hyperfields.Fields.Hypergeometry.transportPath, Hyperfields.Fields.Hypergeometry.twoPointSwap
theorem Hyperfields.Fields.Hypergeometry.transport_through_identity Transporting through the identity line 306 source
Transporting the first point through the identity leaves it in place.

The identity carries a point to itself, so transport returns where it started.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.transportPath, List.cons, Hyperfields.Fields.Hypergeometry.ChartTransition, Hyperfields.Fields.Hypergeometry.twoPointIdentity, List.nil, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 308
  before
```
⊢ transportPath 0 [twoPointIdentity] = some 0
```
  after
  no goals remain
```
theorem transport_through_identity :
    transportPath 0 [twoPointIdentity] = some 0 := by
…
```
Mentions: Hyperfields.Fields.Hypergeometry.transportPath, Hyperfields.Fields.Hypergeometry.twoPointIdentity
theorem Hyperfields.Fields.Hypergeometry.a_single_swap_is_not_the_identity A cycle of the swap is not the identity line 319 source
Transporting through a single swap does not return a point to itself.
This is the negative case for the cycle check. A single swap exchanges the two points rather than fixing them, so the path is a cycle that is not the identity.

Swapping twice returns the point, so the cycle closes; but a single swap is not the identity, and the distinction is what makes the cycle check meaningful.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.transportPath, List.cons, Hyperfields.Fields.Hypergeometry.ChartTransition, Hyperfields.Fields.Hypergeometry.twoPointSwap, List.nil, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 321
  before
```
⊢ transportPath 0 [twoPointSwap] = some 1
```
  after
  no goals remain
```
theorem a_single_swap_is_not_the_identity :
    transportPath 0 [twoPointSwap] = some 1 := by
…
```
Mentions: Hyperfields.Fields.Hypergeometry.transportPath, Hyperfields.Fields.Hypergeometry.twoPointSwap
theorem Hyperfields.Fields.Hypergeometry.two_swaps_are_the_identity Two swaps compose to the identity line 326 source
Transporting through two swaps returns the first point to itself.

Swapping twice returns each point to where it started, so the composed cycle is the identity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Option, Fin, OfNat.ofNat, Nat, Hyperfields.Fields.Hypergeometry.transportPath, List.cons, Hyperfields.Fields.Hypergeometry.ChartTransition, Hyperfields.Fields.Hypergeometry.twoPointSwap, List.nil, Option.some
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 328
  before
```
⊢ transportPath 0 [twoPointSwap, twoPointSwap] = some 0
```
  after
  no goals remain
```
theorem two_swaps_are_the_identity :
    transportPath 0 [twoPointSwap, twoPointSwap] = some 0 := by
…
```
Mentions: Hyperfields.Fields.Hypergeometry.transportPath, Hyperfields.Fields.Hypergeometry.twoPointSwap
def Hyperfields.Fields.Hypergeometry.entry Hypergeometry explainer entry line 338 source
The canonical Hypergeometry record used by the unified portal.

This declaration exposes the checked ecosystem record for Hypergeometry on its own stable explainer page.
See also: Hyperfields.hypergeometry

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.hypergeometry
```
def entry : Hyperfields.Entry := Hyperfields.hypergeometry
…
```
Mentions: Hyperfields.Entry, Hyperfields.hypergeometry