`Hyperfields/Finite.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

10 declarations, 0 contain sorry, 0 axioms

Finite sets over an explicit carrier

The five candidate field modules all need the same small vocabulary: a finite set of points drawn from a carrier of known size, membership, union, intersection, and difference.

The representation is a list of carrier elements with duplicates removed. That is a deliberate choice rather than an accident of what Lean 4 core happens to provide:

Lean 4 core has no Finset. Its Set is an unbounded predicate, which cannot be decided and therefore cannot support by decide proofs.
Std.HashSet exists, but its contains does not reduce for decide: the hash lookup is opaque to the kernel's evaluator. A port whose whole point is machine-checked finite consistency cannot rest on a predicate the compiler will not reduce.

A list does reduce. Membership is List.any with a decidable equality, union is a fold that appends only new elements, and intersection is a filter. Every one of those reduces, so by decide works over them.

The carrier is Fin n, so the number of points is fixed by the type and a structure over it is decidable without any further work.

Imports (1)

Imported by 6 files

def Hyperfields.Finite.mem Membership in a finite set line 43 source
Whether an element belongs to a finite set.
The carrier's equality is decidable, so membership is decidable and the compiler can reduce it.

A finite set is a list without duplicates, so membership is a decidable scan rather than an unbounded predicate.

no axioms what this means
Statement uses: BEq, List, Bool
Proof uses: List.any, BEq.beq
```
def mem {α : Type} [BEq α] (x : α) (xs : List α) : Bool :=
…
```
def Hyperfields.Finite.toSet Every member of a finite set is distinct line 55 source
Remove duplicates from a list, keeping the first occurrence of each element.
This is what makes a finite set a set: List.eraseDups guarantees that two equal lists describe the same collection, so a list of opens is compared by content rather than by how it was written.

A set that listed the same point twice would have a different size than its content, so duplicates are removed.

no axioms what this means
Statement uses: BEq, List
Proof uses: List.eraseDups
```
def toSet {α : Type} [BEq α] (xs : List α) : List α :=
…
```
def Hyperfields.Finite.insertOrdered Inserting an element into a sorted list line 80 source
Insert an element into an ordered list, keeping the list ordered.
This is insertion sort rather than List.mergeSort on purpose. The carrier is always tiny, but mergeSort allocates and recurses in a way that makes the kernel's evaluator give up before it can reduce a decision procedure over a topology's axioms. Insertion sort reduces in a fraction of the depth, which is what makes by decide usable here.

Insertion keeps the list ordered, so a sorted list is the canonical form of a finite set.

no axioms what this means
Statement uses: BEq, Bool, List
2 instances, coercions and auxiliary constants left out.
```
def insertOrdered {α : Type} [BEq α] (le : α → α → Bool) (x : α) (xs : List α) : List α :=
…
```
def Hyperfields.Finite.canonical Canonical ordering of a finite set line 93 source
Order a list so that equal contents give equal lists.
The ordering is an explicit argument rather than a typeclass instance, so the ordering in force is visible at every call site.

A set has one order, and canonicalising is what lets two descriptions of the same set be compared.

no axioms what this means
Statement uses: BEq, Bool, List
2 instances, coercions and auxiliary constants left out.
```
def canonical {α : Type} [BEq α] (le : α → α → Bool) : List α → List α
  | [] => []
  | x :: xs => insertOrdered le x (canonical le xs)

/-!
## The lattice operations
-/

-- L4DEL: title: Union of two finite sets
-- L4DEL: intuition: Union adds what the other set has and keeps what both already share, so no point is counted twice.
/--
The union of two finite sets.
```
Mentions: Hyperfields.Finite.insertOrdered, Hyperfields.Finite.union
def Hyperfields.Finite.union Union of two finite sets line 117 source
The union of two finite sets.
The result is sorted so that the union does not depend on which operand was named first. A union that returned ys's elements before xs's would still have the right membership but the wrong list, and a topology that is closed under union has to be closed under the operation the frame actually uses.
The ordering is an explicit argument rather than a typeclass instance. That keeps the operation total for any carrier the caller can order, and it keeps the caller's ordering visible at the call site, which matters because a different order would give a different list.

Union adds what the other set has and keeps what both already share, so no point is counted twice.

no axioms what this means
Statement uses: BEq, Bool, List
Proof uses: List.eraseDups, Hyperfields.Finite.canonical, HAppend.hAppend
2 instances, coercions and auxiliary constants left out.
```
def union {α : Type} [BEq α] (le : α → α → Bool) (xs ys : List α) : List α :=
…
```
def Hyperfields.Finite.inter Intersection of two finite sets line 128 source
The intersection of two finite sets.
Like union, the result is sorted, so the intersection does not depend on which operand was named first.

Intersection keeps exactly the points both sets name, so it is the filter of one by the other.

no axioms what this means
Statement uses: BEq, Bool, List
Proof uses: Hyperfields.Finite.canonical, List.filter, Hyperfields.Finite.mem
```
def inter {α : Type} [BEq α] (le : α → α → Bool) (xs ys : List α) : List α :=
…
```
def Hyperfields.Finite.diff Difference of two finite sets line 138 source
The difference of two finite sets: the elements of xs that are not in ys.
The result is sorted, so it does not depend on how xs was written.

Difference keeps what the first set names and the second does not, so it is the complement of the intersection inside the first.

no axioms what this means
Statement uses: BEq, Bool, List
Proof uses: Hyperfields.Finite.canonical, List.filter, Bool.not, Hyperfields.Finite.mem
```
def diff {α : Type} [BEq α] (le : α → α → Bool) (xs ys : List α) : List α :=
…
```
def Hyperfields.Finite.subset Containment of one finite set in another line 146 source
Whether every element of xs is also in ys.

A set is contained in another when every point of it is named by the other, and that is a filter over the points.

no axioms what this means
Statement uses: BEq, List, Bool
Proof uses: List.all, Hyperfields.Finite.mem
```
def subset {α : Type} [BEq α] (xs ys : List α) : Bool :=
…
```
def Hyperfields.Finite.carrier The carrier of a finite set line 161 source
The full carrier of n points.
Fin n is core Lean, so the carrier's size is part of its type and no separate bound has to be checked.

A finite set is a list of distinct elements, and the carrier is that list with its duplicates removed.

no axioms what this means
Statement uses: Nat, List, Fin
Proof uses: List.ofFn
```
def carrier (n : Nat) : List (Fin n) :=
…
```
def Hyperfields.Finite.finLe The natural ordering on a finite carrier line 174 source
The natural ordering on Fin n, as a Bool-valued comparison.
Fin n has a decidable order, and the natural one is the order the indices are written in. Every finite set operation in this module takes its ordering as an argument so that the ordering is visible at the call site; this is the one the candidate field ports use.

A carrier of indexed points has a canonical order, and using it keeps every set operation independent of how the set was written.

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: Hyperfields.Finite.finLe.match_1, Decidable.decide, LT.lt
2 instances, coercions and auxiliary constants left out.
```
def finLe : (n : Nat) → Fin n → Fin n → Bool
  | _, a, b => decide (a < b)
```