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

23 declarations, 0 contain sorry, 0 axioms

Hyperstructure

[FRAME] Independent class, containment, composition and recursive relations.

This is the Lean port of the local hyperstructure candidate. It carries the sempiternality view and the recursive structure, and the properties that frame establishes.

The frame keeps four relations apart rather than collapsing them into one "relation": an abstract member is an instance of a class, a contained item is contained by a whole, a component is component of a whole, and a recursive structure adds contains, represents, and connects. The port keeps that separation, because the whole point of the field is that these are independent.

The four designated kinds are the frame's own requirement, not a theorem about kinds in general: base-reality, surreality, preality, and areality must all be declared, must be pairwise distinct, and a composition must contain a representative of each.

What is not proved here, and cannot be, is any claim that these four kinds are the right kinds, that they are exhaustive, or that composition follows from kind distinction. The Python source carries the same [FRAME] classification and this port keeps it.

Imports (2)

Imported by 1 file

Hyperfields/AllFields.lean

def Hyperfields.Fields.Hyperstructure.requiredKinds The four designated kinds line 48 source
The four designated kinds.
These are the kinds the frame requires. They are named, not derived: the field declares that a presentation must distinguish these four, and it does not claim that they are the only kinds there are.

The frame requires a presentation to distinguish these four kinds, and it does not claim they are the only kinds there are.

no axioms what this means
Statement uses: List, String
Proof uses: List.cons, List.nil
```
def requiredKinds : List String := ["base-reality", "surreality", "preality", "areality"]
```
def Hyperfields.Fields.Hyperstructure.declaresAllRequiredKinds All four kinds are declared line 54 source
Whether every designated kind is declared.

A presentation that omits one of the four designated kinds has not distinguished it, so the check requires all four.
Prerequisites: Hyperfields.Fields.Hyperstructure.requiredKinds

no axioms what this means
Statement uses: List, String, Bool
Proof uses: List.all, Hyperfields.Fields.Hyperstructure.requiredKinds, Hyperfields.Finite.mem
2 instances, coercions and auxiliary constants left out.
```
def declaresAllRequiredKinds (declared : List String) : Bool :=
…
```
def Hyperfields.Fields.Hyperstructure.kindsAreDistinct The kinds are distinct line 61 source
Whether the declared kinds are pairwise distinct.

Two names for one kind would make the taxonomy say less than it appears to, so the list is checked to have no repeats.
Prerequisites: Hyperfields.Fields.Hyperstructure.requiredKinds

no axioms what this means
Statement uses: List, String, Bool
Proof uses: BEq.beq, Nat, List.length, List.eraseDups
3 instances, coercions and auxiliary constants left out.
```
def kindsAreDistinct (declared : List String) : Bool :=
…
```
structure Hyperfields.Fields.Hyperstructure.SempiternalityView A presentation of a whole with its members and kinds line 77 source
A presentation of a whole: its abstract members, their kinds, what it contains, and what it is composed of.
The four relation carriers are separate fields on purpose. Collapsing them would erase the distinction the field exists to draw.

A view separates what a member is an instance of, what it is contained by, and what it is a component of, because those are different relations.

no axioms what this means
Statement uses: Nat
```
structure SempiternalityView (n : Nat) where
…
```
def Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOfMember Read a member's kind line 90 source
The kind assigned to a member, if any.

A member the view does not classify has no kind, which is nothing rather than a default.
Prerequisites: Hyperfields.Fields.Hyperstructure.SempiternalityView

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.SempiternalityView, Fin, Option, String
Proof uses: Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOfMember.match_1, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOf, Option.some, Prod.snd, Unit, Option.none
4 instances, coercions and auxiliary constants left out.
```
def SempiternalityView.kindOfMember {n : Nat} (view : SempiternalityView n)
    (member : Fin n) : Option String :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.SempiternalityView
def Hyperfields.Fields.Hyperstructure.SempiternalityView.relations Which relations a member stands in line 100 source
The relations a member stands in, as a list of relation names.

Being an instance of, being contained by, and being a component of are three different relations, so a member can stand in any combination of them.
Prerequisites: Hyperfields.Fields.Hyperstructure.SempiternalityView

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.SempiternalityView, Fin, List, String
Proof uses: ite, Eq, Bool, Hyperfields.Finite.mem, Hyperfields.Fields.Hyperstructure.SempiternalityView.abstractMembers, Bool.true, List.cons, List.nil, Hyperfields.Fields.Hyperstructure.SempiternalityView.contained, Hyperfields.Fields.Hyperstructure.SempiternalityView.components, HAppend.hAppend
7 instances, coercions and auxiliary constants left out.
```
def SempiternalityView.relations {n : Nat} (view : SempiternalityView n)
    (member : Fin n) : List String :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.SempiternalityView
def Hyperfields.Fields.Hyperstructure.SempiternalityView.wellShaped The axioms a presentation must satisfy line 123 source
Whether the view satisfies the presentation axioms.
The checks are:
1. Every abstract member has exactly one kind assignment, and no member outside the abstract members has one.
2. The four designated kinds are all declared, and the declared kinds are pairwise distinct.
3. Every assigned kind is a declared kind.
4. Composition requires both class and containment: every component is abstract and contained.
5. A composition has a representative of each designated kind.
Every abstract member needs exactly one kind, the designated kinds must be declared, and composition must have a representative of each.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.SempiternalityView, Bool
Proof uses: Bool.and, List.all, Fin, Hyperfields.Fields.Hyperstructure.SempiternalityView.abstractMembers, bne, Option, String, Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOfMember, Option.none, Prod, Hyperfields.Fields.Hyperstructure.SempiternalityView.kindOf, Hyperfields.Finite.mem, Prod.fst, BEq.beq, List.length, List.eraseDups, List.map, Hyperfields.Fields.Hyperstructure.declaresAllRequiredKinds, Hyperfields.Fields.Hyperstructure.SempiternalityView.declaredKinds, Hyperfields.Fields.Hyperstructure.kindsAreDistinct and 6 more
8 instances, coercions and auxiliary constants left out.
```
def SempiternalityView.wellShaped {n : Nat} (view : SempiternalityView n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.SempiternalityView
structure Hyperfields.Fields.Hyperstructure.RecursiveStructure A finite recursive structure with its three relations line 154 source
A finite recursive structure: its nodes and its three relations.
contains is the containment relation, represents the representation relation, and connects the operational connection relation. A cycle in one of them says nothing about a cycle in another, which is why the containment acyclicity check below only looks at contains.

Containment, representation, and connection are different relations, and keeping them apart is what stops a cycle in one from being a cycle in another.

no axioms what this means
Statement uses: Nat
```
structure RecursiveStructure (n : Nat) where
…
```
def Hyperfields.Fields.Hyperstructure.RecursiveStructure.noDanglingEndpoints No dangling endpoints line 165 source
Whether every endpoint of a relation is one of the structure's nodes.

A relation that names a node the structure does not have is describing something outside the structure, so every endpoint must be a node.
Prerequisites: Hyperfields.Fields.Hyperstructure.RecursiveStructure

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.RecursiveStructure, Bool
Proof uses: Bool.and, List.all, Prod, Fin, Hyperfields.Fields.Hyperstructure.RecursiveStructure.contains, Hyperfields.Finite.mem, Prod.fst, Hyperfields.Fields.Hyperstructure.RecursiveStructure.nodes, Prod.snd, Hyperfields.Fields.Hyperstructure.RecursiveStructure.represents, Hyperfields.Fields.Hyperstructure.RecursiveStructure.connects
4 instances, coercions and auxiliary constants left out.
```
def RecursiveStructure.noDanglingEndpoints {n : Nat}
    (graph : RecursiveStructure n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.RecursiveStructure
def Hyperfields.Fields.Hyperstructure.RecursiveStructure.containmentAcyclic Containment has no cycle line 188 source
Whether the containment relation is acyclic. -- L4DEL: title: Containment has no cycle -- L4DEL: intuition: A node that can reach itself by following containment is contained in itself, which no well-founded whole allows. -- L4DEL: step: From each node, walk containment forward n steps and check the node never reappears. -- L4DEL: prereq: Hyperfields.Fields.Hyperstructure.RecursiveStructure
Containment is acyclic when no node is reachable from itself by following contains. The check is a bounded reachability scan: from each node, the set of nodes reachable in one, two, ..., n steps must never contain the node itself, where n is the number of nodes. A cycle among k nodes shows up within k steps, so n steps is enough to catch every cycle.

A node that can reach itself by following containment is contained in itself, which no well-founded whole allows.
1. From each node, walk containment forward n steps and check the node never reappears.
Prerequisites: Hyperfields.Fields.Hyperstructure.RecursiveStructure

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.RecursiveStructure, Bool
Proof uses: List.all, Fin, Hyperfields.Fields.Hyperstructure.RecursiveStructure.nodes, List, List.flatMap, List.map, Prod, Prod.snd, List.filter, BEq.beq, Prod.fst, Hyperfields.Fields.Hyperstructure.RecursiveStructure.contains, List.foldl, HAppend.hAppend, List.cons, List.nil, List.range, Bool.not, Hyperfields.Finite.mem
6 instances, coercions and auxiliary constants left out.
```
def RecursiveStructure.containmentAcyclic {n : Nat}
    (graph : RecursiveStructure n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.RecursiveStructure
def Hyperfields.Fields.Hyperstructure.RecursiveStructure.wellShaped The axioms a recursive structure must satisfy line 211 source
Whether the structure satisfies the axioms.
The checks are:
1. Every relation endpoint is one of the structure's nodes.
2. The containment relation is acyclic.
A structure with a dangling endpoint describes something that is not there, and a structure with a containment cycle describes a whole that contains itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Hyperfields.Fields.Hyperstructure.RecursiveStructure, Bool
Proof uses: Bool.and, Hyperfields.Fields.Hyperstructure.RecursiveStructure.noDanglingEndpoints, Hyperfields.Fields.Hyperstructure.RecursiveStructure.containmentAcyclic
```
def RecursiveStructure.wellShaped {n : Nat} (graph : RecursiveStructure n) : Bool :=
…
```
Mentions: Hyperfields.Fields.Hyperstructure.RecursiveStructure
def Hyperfields.Fields.Hyperstructure.fullView A presentation with one member of each designated kind line 228 source
A presentation of a whole with four abstract members, one of each designated kind, all of them contained and all of them components.
Every member is an instance of the class, contained by the whole, and a component of it, which is what makes this the maximal case rather than a partial one.

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

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hyperstructure.SempiternalityView, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hyperstructure.SempiternalityView.mk, Fin, List.cons, Prod, String, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def fullView : SempiternalityView 5 where
…
```
Mentions: Hyperfields.Fields.Hyperstructure.SempiternalityView
def Hyperfields.Fields.Hyperstructure.fullStructure The recursive structure of the whole line 246 source
The recursive structure of the whole: five nodes, the subject containing the four members, and one operational connection between two members.
There is no representation edge here, which is deliberate: the frame keeps the three relations independent, and a structure that exercised only two of them would not show that.

A concrete structure lets the compiler check the acyclicity and the endpoint conditions.

standard axioms: propext what this means
Statement uses: Hyperfields.Fields.Hyperstructure.RecursiveStructure, OfNat.ofNat, Nat
Proof uses: Hyperfields.Fields.Hyperstructure.RecursiveStructure.mk, List.cons, Fin, List.nil, Prod, Prod.mk
4 instances, coercions and auxiliary constants left out.
```
def fullStructure : RecursiveStructure 5 where
…
```
Mentions: Hyperfields.Fields.Hyperstructure.RecursiveStructure
theorem Hyperfields.Fields.Hyperstructure.full_view_is_well_shaped The presentation satisfies the axioms line 255 source
The worked presentation satisfies the presentation 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.Hyperstructure.SempiternalityView.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.fullView, 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 256
  before
```
⊢ fullView.wellShaped = true
```
  after
  no goals remain
```
theorem full_view_is_well_shaped : fullView.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hyperstructure.full_structure_is_well_shaped The recursive structure satisfies the axioms line 261 source
The worked recursive structure satisfies the structure 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.Hyperstructure.RecursiveStructure.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.fullStructure, 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 262
  before
```
⊢ fullStructure.wellShaped = true
```
  after
  no goals remain
```
theorem full_structure_is_well_shaped : fullStructure.wellShaped = true := by
…
```
theorem Hyperfields.Fields.Hyperstructure.a_member_stands_in_three_relations A member stands in three relations at once line 274 source
A member that is abstract, contained, and a component stands in all three relations.
This is the claim the frame exists to make. The three relations are independent, so one member can be in all of them at once without the relations being identified.

The point of the field is that instance, containment, and composition are separate relations that can hold of the same member simultaneously.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, String, Hyperfields.Fields.Hyperstructure.SempiternalityView.relations, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.fullView, Fin, List.cons, List.nil
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 276
  before
```
⊢ fullView.relations 1 = ["instance_of", "contained_by", "component_of"]
```
  after
  no goals remain
```
theorem a_member_stands_in_three_relations :
    fullView.relations 1 = ["instance_of", "contained_by", "component_of"] := by
…
```
theorem Hyperfields.Fields.Hyperstructure.the_subject_stands_in_no_relation A member outside the abstract class stands in no relation line 285 source
The subject of the view stands in none of the three member relations.
The subject is the whole that presents the members, not a member of it.

The subject is not an instance of the class it presents, so it stands in none of the three member relations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, String, Hyperfields.Fields.Hyperstructure.SempiternalityView.relations, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.fullView, Fin, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 287
  before
```
⊢ fullView.relations 0 = []
```
  after
  no goals remain
```
theorem the_subject_stands_in_no_relation :
    fullView.relations 0 = [] := by
…
```
theorem Hyperfields.Fields.Hyperstructure.the_designated_kinds_are_distinct The kinds are pairwise distinct line 292 source
The four designated kinds are pairwise distinct.

The four designated kinds must be four different kinds, or the taxonomy would collapse.

no axioms what this means
Statement uses: Eq, Nat, List.length, String, List.eraseDups, Hyperfields.Fields.Hyperstructure.requiredKinds
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
5 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 294
  before
```
⊢ requiredKinds.eraseDups.length = requiredKinds.length
```
  after
  no goals remain
```
theorem the_designated_kinds_are_distinct :
    requiredKinds.eraseDups.length = requiredKinds.length := by
…
```
theorem Hyperfields.Fields.Hyperstructure.a_missing_designated_kind_is_rejected A missing designated kind is rejected line 304 source
A view that declares only three of the four designated kinds is rejected.
This is the negative case. A checker that never rejects anything is not a check, and this theorem is what makes the positive case meaningful.

The frame requires all four, so a view that omits one is not a presentation of the kind the frame describes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperstructure.SempiternalityView.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.SempiternalityView.mk, Fin, List.cons, Prod, String, 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 312
  before
```
⊢ { subject := 0, kindOf := [(1, "base-reality"), (2, "surreality"), (3, "preality")], abstractMembers := [1, 2, 3],
        contained := [1, 2, 3], components := [1, 2, 3],
        declaredKinds := ["base-reality", "surreality", "preality"] }.wellShaped =
    false
```
  after
  no goals remain
```
theorem a_missing_designated_kind_is_rejected :
    ({ subject := 0,
…
```
theorem Hyperfields.Fields.Hyperstructure.a_composition_missing_a_kind_is_rejected A composition missing a kind is rejected line 322 source
A view whose composition omits the areality representative is rejected.
The composition has three members instead of four, so it does not represent every designated kind.

A composition must represent each designated kind, so dropping one member breaks the composition requirement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperstructure.SempiternalityView.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.SempiternalityView.mk, Fin, List.cons, Prod, String, 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 330
  before
```
⊢ { subject := 0, kindOf := [(1, "base-reality"), (2, "surreality"), (3, "preality")], abstractMembers := [1, 2, 3],
        contained := [1, 2, 3], components := [1, 2, 3],
        declaredKinds := ["base-reality", "surreality", "preality", "areality"] }.wellShaped =
    false
```
  after
  no goals remain
```
theorem a_composition_missing_a_kind_is_rejected :
    ({ subject := 0,
…
```
theorem Hyperfields.Fields.Hyperstructure.a_containment_cycle_is_rejected A containment cycle is rejected line 341 source
A structure whose containment relation loops back to its own start is rejected.
This is the negative case for acyclicity, and it is the reason the frame requires acyclic containment rather than merely well-formed endpoints.

A whole that contains itself is not a finite recursive structure, so the acyclicity check must be able to fail.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperstructure.RecursiveStructure.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.RecursiveStructure.mk, List.cons, Fin, List.nil, Prod, Prod.mk, 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 346
  before
```
⊢ { nodes := [0, 1], contains := [(0, 1), (1, 0)], represents := [], connects := [] }.wellShaped = false
```
  after
  no goals remain
```
theorem a_containment_cycle_is_rejected :
    ({ nodes := [0, 1],
…
```
theorem Hyperfields.Fields.Hyperstructure.a_dangling_endpoint_is_rejected A dangling relation endpoint is rejected line 357 source
A structure whose relation names a node it does not have is rejected.
This is the second negative case, and it is independent of the acyclicity check: a structure can be acyclic and still describe a node that is not there.

A relation to a node the structure does not have describes something that is not there.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Bool, Hyperfields.Fields.Hyperstructure.RecursiveStructure.wellShaped, OfNat.ofNat, Nat, Hyperfields.Fields.Hyperstructure.RecursiveStructure.mk, List.cons, Fin, List.nil, Prod, Prod.mk, 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 362
  before
```
⊢ { nodes := [0, 1], contains := [(0, 1), (1, 2)], represents := [], connects := [] }.wellShaped = false
```
  after
  no goals remain
```
theorem a_dangling_endpoint_is_rejected :
    ({ nodes := [0, 1],
…
```
def Hyperfields.Fields.Hyperstructure.entry Hyperstructure explainer entry line 372 source
The canonical Hyperstructure record used by the unified portal.

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

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