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

19 declarations, 0 contain sorry, 0 axioms

The foundation architecture, as typed structure

The ecosystem's architecture was declared directly by Tyler Roost and is recorded in prose in docs/FOUNDATION_ARCHITECTURE.md. This module makes the parts of it that are finite and decidable into typed Lean, so that the catalogue can carry the architecture rather than only describe it.

Three things are encoded here.

The four semantic axes. WHAT (what is the structure), HOW (how does it come to exist and compose), WHY (why is it there), and WHERE-WHEN (where and when). The axes are not an exclusive partition. A field occupies a profile of axes, and the four named fields are the canonical instance of each axis rather than its only member. metamathethicology is the proof of this: it is explicitly a combination field, so the family already thinks in composites.
The derivation order. The order in which fields become available. This is an availability order, not an authority order: stage 0 does not outrank stage 8, it is merely built first.
The two paired relations. hypergeometry is to hyperspace as hypertopology is to hypertime, and hypermath and hyperlogic are the what and the how that together underpin everything else.

What is not encoded here is the self-kernel and its composition. That belongs to hypermath and hyperlogic, and this module cites them rather than restating them. The same rule the family already follows: a foundation imports nothing, and a catalogue cites rather than duplicates.

Imports (1)

Hyperfields.Core

Imported by 1 file

Hyperfields/AllFields.lean

inductive Hyperfields.Architecture.Axis The four semantic axes line 54 source
The four semantic axes a field may occupy.
what is the structure itself. how is how it comes to exist and how it composes. why is creation, will, consciousness, and consent. whereWhen is placement, index, and physical application.
These are axes, not a partition. A field may occupy several, and the four canonical fields are the primary instance of each axis rather than its only member.

A field answers some of what, how, why, and where-when; a field that answered all four would be a different kind of thing entirely.

no axioms what this means
```
inductive Axis where
…
```

def Hyperfields.Architecture.Axis.string The published name of an axis line 64 source

The published name of an axis.

The axis vocabulary is fixed and public, so each axis renders to exactly one string.

no axioms what this means

Statement uses: Hyperfields.Architecture.Axis, String

Proof uses: Hyperfields.Architecture.instReprAxis.repr.match_1, Unit

def Axis.string : Axis → String
  | .what => "what"
  | .how => "how"
  | .why => "why"
  | .whereWhen => "where-when"

-- L4DEL: title: The axis profile of a field
-- L4DEL: intuition: A field may answer several questions at once, so its profile is a set rather than a single label.
/--
The axes a field occupies.

The profile is a set, so a field that answers two questions says so, and the

Mentions: Hyperfields.Architecture.Axis

abbrev Hyperfields.Architecture.AxisProfile The axis profile of a field line 78 source
The axes a field occupies.
The profile is a set, so a field that answers two questions says so, and the empty profile is a distinguishable state rather than a missing value.

A field may answer several questions at once, so its profile is a set rather than a single label.

no axioms what this means
Proof uses: List, Hyperfields.Architecture.Axis
```
abbrev AxisProfile := List Axis
```
Mentions: Hyperfields.Architecture.Axis
def Hyperfields.Architecture.stageOf The stage a field becomes available at line 93 source
The stage at which a field becomes available.
Stage 0 is the self-kernel and its how. Each later stage is built from what came before. This is an availability order and carries no authority claim: stage 8 is not more important than stage 0, it is merely built later.

Availability is a build order, not a ranking, so a late stage is not a lesser field.

no axioms what this means
Statement uses: Hyperfields.RepoId, Nat
Proof uses: Hyperfields.Architecture.stageOf.match_1, Unit, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def stageOf (id : RepoId) : Nat :=
…
```
Mentions: Hyperfields.RepoId
def Hyperfields.Architecture.allIds Every field, in derivation order line 128 source
Every field the catalogue carries, in derivation order.

The catalogue is listed in the order the fields become available, so a reader can see what each one is built on.
Prerequisites: Hyperfields.RepoId

no axioms what this means
Statement uses: List, Hyperfields.RepoId
Proof uses: List.cons, Hyperfields.RepoId.hypermath, Hyperfields.RepoId.hyperlogic, Hyperfields.RepoId.hypertopology, Hyperfields.RepoId.hypergeometry, Hyperfields.RepoId.hyperorder, Hyperfields.RepoId.hyperchaos, Hyperfields.RepoId.hyperemergence, Hyperfields.RepoId.hypertime, Hyperfields.RepoId.hyperspace, Hyperfields.RepoId.hyperdynamics, Hyperfields.RepoId.hypermechanics, Hyperfields.RepoId.hyperreality, Hyperfields.RepoId.hyperstructure, Hyperfields.RepoId.hyperphysics, Hyperfields.RepoId.hyperethics, Hyperfields.RepoId.hyperobjectivity, Hyperfields.RepoId.hypersubjectivity, Hyperfields.RepoId.hypergrammar, Hyperfields.RepoId.hyperorganization and 10 more
```
def allIds : List RepoId := [
…
```
Mentions: Hyperfields.RepoId
def Hyperfields.Architecture.axisProfile Which question each field answers line 147 source
The axis profile of every field.

A field may answer more than one of what, how, why, and where-when, so the profile is a list rather than a single axis.
Prerequisites: Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile

no axioms what this means
Statement uses: List, Prod, Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile
Proof uses: List.cons, Prod.mk, Hyperfields.RepoId.hypermath, Hyperfields.Architecture.Axis, Hyperfields.Architecture.Axis.what, List.nil, Hyperfields.RepoId.hyperlogic, Hyperfields.Architecture.Axis.how, Hyperfields.RepoId.hypertopology, Hyperfields.Architecture.Axis.whereWhen, Hyperfields.RepoId.hypergeometry, Hyperfields.RepoId.hyperorder, Hyperfields.RepoId.hyperchaos, Hyperfields.RepoId.hyperemergence, Hyperfields.RepoId.hypertime, Hyperfields.RepoId.hyperspace, Hyperfields.RepoId.hyperdynamics, Hyperfields.RepoId.hypermechanics, Hyperfields.RepoId.hyperreality, Hyperfields.RepoId.hyperstructure and 16 more
```
def axisProfile : List (RepoId × AxisProfile) := [
…
```
Mentions: Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile
def Hyperfields.Architecture.profileOf Look up a field's axes line 182 source
Look up a field's axis profile.

A field the table does not carry has no axes, which is the empty list rather than an error.
Prerequisites: Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile

no axioms what this means
Statement uses: Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile
Proof uses: Hyperfields.Architecture.profileOf.match_1, Option, Prod, List.find?, BEq.beq, Prod.fst, Hyperfields.Architecture.axisProfile, Prod.snd, Unit, List.nil, Hyperfields.Architecture.Axis
1 instances, coercions and auxiliary constants left out.
```
def profileOf (id : RepoId) : AxisProfile :=
…
```
Mentions: Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile
structure Hyperfields.Architecture.Pairing The two paired relations line 202 source
The two declared pairings.
hypergeometry is the metamathematical structure that can form geometries and hyperspace is the dimensionality of structures; that relation is the same one that holds between hypertopology and hypertime. The second pair is hypermath and hyperlogic themselves, the what and the how, which together underpin everything else.

Two pairs of fields stand to each other the same way, and the pairing is the reason the derivation order is not arbitrary.

no axioms what this means
```
structure Pairing where
…
```
def Hyperfields.Architecture.pairings The three declared pairings line 211 source
The declared pairings.

Each pairing names two fields that stand to each other the same way, which is why the derivation order is not arbitrary.
Prerequisites: Hyperfields.Architecture.Pairing

no axioms what this means
Statement uses: List, Hyperfields.Architecture.Pairing
Proof uses: List.cons, Hyperfields.Architecture.Pairing.mk, Hyperfields.RepoId.hypergeometry, Hyperfields.RepoId.hyperspace, Hyperfields.RepoId.hypertopology, Hyperfields.RepoId.hypertime, Hyperfields.RepoId.hypermath, Hyperfields.RepoId.hyperlogic, List.nil
```
def pairings : List Pairing := [
…
```
Mentions: Hyperfields.Architecture.Pairing
theorem Hyperfields.Architecture.every_field_has_a_stage Every field has a stage line 226 source
Every catalogued field has a stage and an axis profile.

The stage table covers the whole catalogue, so no field is left without a place in the derivation order.
1. Check each of the twenty-eight fields against the stage bound.
Prerequisites: Hyperfields.Architecture.allIds, Hyperfields.Architecture.stageOf

no axioms what this means
Statement uses: Eq, Bool, List.all, Hyperfields.RepoId, Hyperfields.Architecture.allIds, Decidable.decide, LE.le, Nat, Hyperfields.Architecture.stageOf, OfNat.ofNat, Bool.true
Proof uses: of_decide_eq_true, id, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 228
  before
```
⊢ (allIds.all fun id => decide (stageOf id ≤ 8)) = true
```
  after
  no goals remain
```
theorem every_field_has_a_stage :
    allIds.all (fun id => stageOf id ≤ 8) = true := by
…
```
Mentions: Hyperfields.Architecture.stageOf
theorem Hyperfields.Architecture.every_stage_is_nonneg No stage is negative line 234 source
The stage of every field is at least zero.

A stage is a natural number, so the lower bound holds by construction and the check confirms the table was not built with a negative.
Prerequisites: Hyperfields.Architecture.allIds, Hyperfields.Architecture.stageOf

no axioms what this means
Statement uses: Eq, Bool, List.all, Hyperfields.RepoId, Hyperfields.Architecture.allIds, Decidable.decide, LE.le, Nat, OfNat.ofNat, Hyperfields.Architecture.stageOf, Bool.true
Proof uses: of_decide_eq_true, id, Eq.refl
7 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 236
  before
```
⊢ (allIds.all fun id => decide (0 ≤ stageOf id)) = true
```
  after
  no goals remain
```
theorem every_stage_is_nonneg :
    allIds.all (fun id => 0 ≤ stageOf id) = true := by
…
```
Mentions: Hyperfields.Architecture.stageOf
theorem Hyperfields.Architecture.catalogue_and_stages_agree The catalogue has twenty-eight fields line 242 source
The catalogue and the stage table agree on the number of fields.

The list is written out, so Lean can count it exactly rather than trusting a number in prose.
Prerequisites: Hyperfields.Architecture.allIds

no axioms what this means
Statement uses: Eq, Nat, List.length, Hyperfields.RepoId, Hyperfields.Architecture.allIds, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 243
  before
```
⊢ allIds.length = 28
```
  after
  no goals remain
```
theorem catalogue_and_stages_agree : allIds.length = 28 := by
…
```
theorem Hyperfields.Architecture.every_field_occupies_an_axis Every field answers some question line 249 source
Every catalogued field has a non-empty axis profile.

A field with no axis would be a field that answers nothing, so the table is checked to have no such entry.
Prerequisites: Hyperfields.Architecture.allIds, Hyperfields.Architecture.profileOf

no axioms what this means
Statement uses: Eq, Bool, List.all, Hyperfields.RepoId, Hyperfields.Architecture.allIds, Bool.not, List.isEmpty, Hyperfields.Architecture.Axis, Hyperfields.Architecture.profileOf, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 251
  before
```
⊢ (allIds.all fun id => !List.isEmpty (profileOf id)) = true
```
  after
  no goals remain
```
theorem every_field_occupies_an_axis :
    allIds.all (fun id => !(profileOf id).isEmpty) = true := by
…
```
Mentions: Hyperfields.Architecture.profileOf
theorem Hyperfields.Architecture.every_axis_is_occupied All four axes are used line 257 source
The four axes are each occupied by at least one field.

An axis no field occupies would be a distinction the ecosystem declares and does not use, so each of the four is checked to have a member.
Prerequisites: Hyperfields.Architecture.allIds, Hyperfields.Architecture.profileOf

no axioms what this means
Statement uses: Eq, Bool, Bool.and, List.any, Hyperfields.RepoId, Hyperfields.Architecture.allIds, List.contains, Hyperfields.Architecture.Axis, Hyperfields.Architecture.profileOf, Hyperfields.Architecture.Axis.what, Hyperfields.Architecture.Axis.how, Hyperfields.Architecture.Axis.why, Hyperfields.Architecture.Axis.whereWhen, 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
```
⊢ ((((allIds.any fun id => List.contains (profileOf id) Axis.what) &&
          allIds.any fun id => List.contains (profileOf id) Axis.how) &&
        allIds.any fun id => List.contains (profileOf id) Axis.why) &&
      allIds.any fun id => List.contains (profileOf id) Axis.whereWhen) =
    true
```
  after
  no goals remain
```
theorem every_axis_is_occupied :
    (allIds.any (fun id => (profileOf id).contains .what) &&
     allIds.any (fun id => (profileOf id).contains .how) &&
     allIds.any (fun id => (profileOf id).contains .why) &&
     allIds.any (fun id => (profileOf id).contains .whereWhen)) = true := by
…
```
Mentions: Hyperfields.Architecture.profileOf
theorem Hyperfields.Architecture.profiles_are_total The profiles cover the catalogue exactly line 268 source
No field occupies no axis, and the profiles are total over the catalogue.

The profile table and the catalogue have the same length, so no field is missing a profile and none has two.
Prerequisites: Hyperfields.Architecture.allIds, Hyperfields.Architecture.axisProfile

no axioms what this means
Statement uses: Eq, Nat, List.length, Prod, Hyperfields.RepoId, Hyperfields.Architecture.AxisProfile, Hyperfields.Architecture.axisProfile, Hyperfields.Architecture.allIds
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
1 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 269
  before
```
⊢ axisProfile.length = allIds.length
```
  after
  no goals remain
```
theorem profiles_are_total : axisProfile.length = allIds.length := by
…
```
theorem Hyperfields.Architecture.there_are_three_pairings There are three pairings line 275 source
There are three declared pairings.

The list is explicit, so Lean can reduce its length exactly.
Prerequisites: Hyperfields.Architecture.pairings

no axioms what this means
Statement uses: Eq, Nat, List.length, Hyperfields.Architecture.Pairing, Hyperfields.Architecture.pairings, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 276
  before
```
⊢ pairings.length = 3
```
  after
  no goals remain
```
theorem there_are_three_pairings : pairings.length = 3 := by
…
```
theorem Hyperfields.Architecture.pairings_join_distinct_fields A pairing needs two fields line 282 source
No pairing joins a field to itself.

A field paired with itself would state no relation, so no declared pairing may have equal endpoints.
Prerequisites: Hyperfields.Architecture.pairings

no axioms what this means
Statement uses: Eq, List, Hyperfields.Architecture.Pairing, List.filter, BEq.beq, Hyperfields.RepoId, Hyperfields.Architecture.Pairing.left, Hyperfields.Architecture.Pairing.right, Hyperfields.Architecture.pairings, List.nil
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
1. decide line 284
  before
```
⊢ List.filter (fun pairing => pairing.left == pairing.right) pairings = []
```
  after
  no goals remain
```
theorem pairings_join_distinct_fields :
    pairings.filter (fun pairing => pairing.left == pairing.right) = [] := by
…
```
theorem Hyperfields.Architecture.the_what_how_pair_is_declared The what and the how are paired line 290 source
The canonical what/how pair is the first pairing.

Hypermath is the what and hyperlogic is the how, and the declaration that they pair is checked rather than assumed.
Prerequisites: Hyperfields.Architecture.pairings

no axioms what this means
Statement uses: Eq, Bool, List.any, Hyperfields.Architecture.Pairing, Hyperfields.Architecture.pairings, Bool.and, BEq.beq, Hyperfields.RepoId, Hyperfields.Architecture.Pairing.left, Hyperfields.RepoId.hypermath, Hyperfields.Architecture.Pairing.right, Hyperfields.RepoId.hyperlogic, 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 293
  before
```
⊢ (pairings.any fun pairing => pairing.left == RepoId.hypermath && pairing.right == RepoId.hyperlogic) = true
```
  after
  no goals remain
```
theorem the_what_how_pair_is_declared :
    pairings.any (fun pairing =>
      pairing.left == .hypermath && pairing.right == .hyperlogic) = true := by
…
```
Mentions: Hyperfields.hypermath, Hyperfields.hyperlogic
theorem Hyperfields.Architecture.the_shape_pairs_are_declared The two shape pairings are declared line 299 source
The shape/dimensionality and nearness/index pairings are both declared.

Geometry is to space as topology is to time, and both halves of that analogy are checked to be in the table.
Prerequisites: Hyperfields.Architecture.pairings

no axioms what this means
Statement uses: Eq, Bool, Bool.and, List.any, Hyperfields.Architecture.Pairing, Hyperfields.Architecture.pairings, BEq.beq, Hyperfields.RepoId, Hyperfields.Architecture.Pairing.left, Hyperfields.RepoId.hypergeometry, Hyperfields.Architecture.Pairing.right, Hyperfields.RepoId.hyperspace, Hyperfields.RepoId.hypertopology, Hyperfields.RepoId.hypertime, 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 304
  before
```
⊢ ((pairings.any fun pairing => pairing.left == RepoId.hypergeometry && pairing.right == RepoId.hyperspace) &&
      pairings.any fun pairing => pairing.left == RepoId.hypertopology && pairing.right == RepoId.hypertime) =
    true
```
  after
  no goals remain
```
theorem the_shape_pairs_are_declared :
    (pairings.any (fun pairing =>
       pairing.left == .hypergeometry && pairing.right == .hyperspace) &&
     pairings.any (fun pairing =>
       pairing.left == .hypertopology && pairing.right == .hypertime)) = true := by
…
```
Mentions: Hyperfields.hypergeometry, Hyperfields.hyperspace, Hyperfields.hypertopology, Hyperfields.hypertime