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

AFA: Anti-Foundation Axiom
APG: accessible pointed graph
L4DEL: Lean4 Domain Explanation Language
URL: Used in an explanation or its source, but not expanded by this annotation. Follow its linked source.

38 declarations, 0 contain sorry, 0 axioms

Initial source-pinned ecosystem registry

Each public entry below points to the exact main commit inspected on 2026-10-13. Candidate branches and dirty local worktrees are deliberately not promoted into this registry. Five field candidates have no public repository yet and are marked as such.

Every explanation begins as sourceDerivedUnreviewed. Lean checks the structure of the catalogue, but Tyler's review is the gate for changing an explanation to ownerReviewed.

Imports (1)

Hyperfields.Core

Imported by 30 files

def Hyperfields.sourceOnMain Bind an entry to a public main revision line 19 source
The repository URL and exact revision are constructed together.

standard axioms: propext what this means
Statement uses: String, Option, Hyperfields.SourceCoordinate
Proof uses: Option.some, Hyperfields.SourceCoordinate.mk, HAppend.hAppend, ToString.toString
3 instances, coercions and auxiliary constants left out.
```
def sourceOnMain (slug revision : String) : Option SourceCoordinate :=
…
```
Mentions: Hyperfields.SourceCoordinate
def Hyperfields.sourceWithoutMain Bind an entry to a public repository without a main pin line 27 source
A public repository with no resolvable main commit still has a true URL, and inventing a revision for it would be a false coordinate.

standard axioms: propext what this means
Statement uses: String, Option, Hyperfields.SourceCoordinate
Proof uses: Option.some, Hyperfields.SourceCoordinate.mk, HAppend.hAppend, ToString.toString, Option.none
3 instances, coercions and auxiliary constants left out.
```
def sourceWithoutMain (slug : String) : Option SourceCoordinate :=
…
```
Mentions: Hyperfields.SourceCoordinate
def Hyperfields.mkPublicEntry Construct a source-pinned public entry line 43 source
Construct a public-main entry.
The slug and the display name are derived from the identifier rather than passed in. A second hand-written list of the same facts could disagree with the identifier, and the disagreement would publish an entry under a name its own module does not use.

Every public-main entry begins with an exact coordinate and unreviewed explanatory status.

standard axioms: propext what this means
Statement uses: Hyperfields.RepoId, Hyperfields.EcosystemRole, Hyperfields.Grounding, List, Hyperfields.OperatingMode, String, Hyperfields.Entry
Proof uses: Hyperfields.Entry.mk, Hyperfields.RepoId.slug, Hyperfields.RepoId.displayName, Hyperfields.SourceState.publicMainPinned, Hyperfields.sourceOnMain, Hyperfields.ReviewState.sourceDerivedUnreviewed
```
def mkPublicEntry
    (id : RepoId)
    (role : EcosystemRole)
    (grounding : Grounding)
    (modes : List OperatingMode)
    (summary revision : String) : Entry :=
…
```
Mentions: Hyperfields.RepoId, Hyperfields.EcosystemRole, Hyperfields.Grounding, Hyperfields.OperatingMode, Hyperfields.Entry
def Hyperfields.mkUnpublishedEntry Construct an unpublished field candidate line 63 source
A local candidate is registered without inventing a public source coordinate or settled grounding.

no axioms what this means
Statement uses: Hyperfields.RepoId, String, List, Hyperfields.OperatingMode, Hyperfields.Entry
Proof uses: Hyperfields.Entry.mk, Hyperfields.RepoId.slug, Hyperfields.RepoId.displayName, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.unresolved, Hyperfields.SourceState.localCandidateUnpublished, Option.none, Hyperfields.SourceCoordinate, Hyperfields.ReviewState.sourceDerivedUnreviewed
```
def mkUnpublishedEntry
    (id : RepoId)
    (summary : String)
    (modes : List OperatingMode) : Entry :=
…
```
Mentions: Hyperfields.RepoId, Hyperfields.OperatingMode, Hyperfields.Entry
def Hyperfields.hyperchaos Hyperchaos line 83 source
A deliberately unresolved field frame records uses of chaos without silently choosing a native meaning.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperchaos, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.unresolved, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, List.nil

field frame: A typed place to record a proposed field while its native axioms remain unresolved.
```
def hyperchaos : Entry := mkPublicEntry .hyperchaos .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperorder Hyperorder line 90 source
Hyperorder records finite ordering structure while treating an absent relation as unknown rather than false.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperorder, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.fieldPrimitive, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative, List.nil
```
def hyperorder : Entry := mkPublicEntry .hyperorder .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperemergence Hyperemergence line 97 source
Hyperemergence asks whether coherent behavior persists across levels rather than merely appearing at one level.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperemergence, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperstratum, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.integrative
```
def hyperemergence : Entry := mkPublicEntry .hyperemergence .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperobjectivity Hyperobjectivity line 104 source
Hyperobjectivity studies what remains invariant across situated presentations.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperobjectivity, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperreality, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hyperobjectivity : Entry := mkPublicEntry .hyperobjectivity .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hypersubjectivity Hypersubjectivity line 111 source
Hypersubjectivity makes the situated perspective part of the formal object instead of erasing it.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hypersubjectivity, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperreality, List.cons, Hyperfields.RepoId, Hyperfields.RepoId.hyperobjectivity, List.nil, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hypersubjectivity : Entry := mkPublicEntry .hypersubjectivity .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperreality Hyperreality line 118 source
Hyperreality provides the repository's current taxonomy of reality presentations and their containment order.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperreality, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.fieldPrimitive, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.integrative, List.nil
```
def hyperreality : Entry := mkPublicEntry .hyperreality .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hypertime Hypertime line 125 source
Hypertime records branching and order among reality presentations without assuming an outside clock.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hypertime, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperreality, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hypertime : Entry := mkPublicEntry .hypertime .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperspace Hyperspace line 132 source
Hyperspace records placement among observable realities without silently converting placement into passage.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperspace, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperreality, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hyperspace : Entry := mkPublicEntry .hyperspace .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hypergeometry Hypergeometry line 138 source
A finite local candidate records chart, metric, and transport structure without claiming a public source or native completion.

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkUnpublishedEntry, Hyperfields.RepoId.hypergeometry, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, List.nil
```
def hypergeometry : Entry := mkUnpublishedEntry .hypergeometry
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkUnpublishedEntry
def Hyperfields.hypertopology Hypertopology line 143 source
A finite local candidate records open, closure, boundary, and continuity structure without claiming a public source or native completion.

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkUnpublishedEntry, Hyperfields.RepoId.hypertopology, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, List.nil
```
def hypertopology : Entry := mkUnpublishedEntry .hypertopology
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkUnpublishedEntry
def Hyperfields.hyperstructure Hyperstructure line 148 source
A finite local candidate separates abstract roles, containers, components, and exact presentation isomorphism.

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkUnpublishedEntry, Hyperfields.RepoId.hyperstructure, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.integrative, List.nil
```
def hyperstructure : Entry := mkUnpublishedEntry .hyperstructure
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkUnpublishedEntry
def Hyperfields.hyperdynamics Hyperdynamics line 153 source
A finite local candidate records transitions, path lifting, and coupled products without claiming native dynamics are complete.

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkUnpublishedEntry, Hyperfields.RepoId.hyperdynamics, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional, List.nil
```
def hyperdynamics : Entry := mkUnpublishedEntry .hyperdynamics
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkUnpublishedEntry
def Hyperfields.hypermechanics Hypermechanics line 158 source
A finite local candidate records guarded rewrites, conservation, noninterference, and connection rules.

no axioms what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkUnpublishedEntry, Hyperfields.RepoId.hypermechanics, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional, List.nil
```
def hypermechanics : Entry := mkUnpublishedEntry .hypermechanics
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkUnpublishedEntry
def Hyperfields.hypergrammar Hypergrammar line 164 source
Hypergrammar is the communicative field for forming and relating expressions across the ecosystem.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hypergrammar, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.fieldPrimitive, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative, List.nil
```
def hypergrammar : Entry := mkPublicEntry .hypergrammar .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperlogic Hyperlogic line 171 source
Hyperlogic is presented as Hypermath's logic counterpart.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperlogic, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hyperlogic : Entry := mkPublicEntry .hyperlogic .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hypermath Hypermath line 178 source
Hypermath is the ecosystem's primitive mathematical kernel and Lean-facing bridge.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hypermath, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.fieldPrimitive, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative, List.nil
```
def hypermath : Entry := mkPublicEntry .hypermath .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperphysics Hyperphysics line 185 source
Hyperphysics applies the hyperfield programme to physical law while keeping model evidence distinct from physical confirmation.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperphysics, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional
```
def hyperphysics : Entry := mkPublicEntry .hyperphysics .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperethics Hyperethics line 192 source
Hyperethics applies the hyperfield programme to moral and governance structure.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperethics, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative
```
def hyperethics : Entry := mkPublicEntry .hyperethics .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperchemistry Hyperchemistry line 199 source
Hyperchemistry models how operations compose inside Hyperphysics.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperchemistry, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hyperphysics, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional
```
def hyperchemistry : Entry := mkPublicEntry .hyperchemistry .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperbiology Hyperbiology line 205 source
Hyperbiology is registered without a public main coordinate, so its current public source remains unresolved here.

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.Entry.mk, Hyperfields.RepoId.hyperbiology, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.unresolved, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional, List.nil, Hyperfields.SourceState.publicWithoutMain, Hyperfields.sourceWithoutMain, Hyperfields.ReviewState.sourceDerivedUnreviewed
```
def hyperbiology : Entry := {
…
```
Mentions: Hyperfields.Entry
def Hyperfields.hyperprobability Hyperprobability line 220 source
Hyperprobability isolates the field structure of bounded uncertainty and guaranteed outcomes.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperprobability, Hyperfields.EcosystemRole.hyperfield, Hyperfields.Grounding.unresolved, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.communicative, List.nil
```
def hyperprobability : Entry := mkPublicEntry .hyperprobability .hyperfield
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperstratum Hyperstratum line 227 source
Hyperstratum organizes form, frame, field, relation, graph, structure, and representation across levels.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperstratum, Hyperfields.EcosystemRole.structuralHub, Hyperfields.Grounding.unresolved, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.integrative, Hyperfields.OperatingMode.reflective, List.nil
```
def hyperstratum : Entry := mkPublicEntry .hyperstratum .structuralHub
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.hyperorganization Hyperorganization line 234 source
Hyperorganization is registered as a structural hub pending an owner-reviewed account of its relation to the fields.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.hyperorganization, Hyperfields.EcosystemRole.structuralHub, Hyperfields.Grounding.unresolved, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.integrative, Hyperfields.OperatingMode.reflective, List.nil
```
def hyperorganization : Entry := mkPublicEntry .hyperorganization .structuralHub
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.ordinatics Ordinatics line 241 source
Ordinatics supplies ordinal-first arithmetic and staged semantics rather than being silently relabelled as a hyperfield.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.ordinatics, Hyperfields.EcosystemRole.ordinalInfrastructure, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.nil, Hyperfields.RepoId, List.cons, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional
```
def ordinatics : Entry := mkPublicEntry .ordinatics .ordinalInfrastructure
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.metamathethicology Metamathethicology line 248 source
Metamathethicology combines meta-level accounts without transferring authority among them automatically.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.metamathethicology, Hyperfields.EcosystemRole.metaFramework, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.cons, Hyperfields.RepoId, Hyperfields.RepoId.hyperlogic, Hyperfields.RepoId.hyperethics, Hyperfields.RepoId.hyperphysics, List.nil, Hyperfields.OperatingMode, Hyperfields.OperatingMode.integrative, Hyperfields.OperatingMode.reflective
```
def metamathethicology : Entry := mkPublicEntry .metamathethicology .metaFramework
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.metaMorphoscriptedOrigination Meta-Morphoscripted-Origination line 255 source
This framework studies how narratives of origination are formed and transformed under limited cognition.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.metaMorphoscriptedOrigination, Hyperfields.EcosystemRole.metaFramework, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypergrammar, List.cons, Hyperfields.RepoId, Hyperfields.RepoId.hyperreality, List.nil, Hyperfields.OperatingMode, Hyperfields.OperatingMode.communicative, Hyperfields.OperatingMode.reflective
```
def metaMorphoscriptedOrigination : Entry := mkPublicEntry .metaMorphoscriptedOrigination
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.groundedHypercalculi Grounded Hypercalculi line 264 source
The calculi are grounded because they operate over lower-level Hypermath and adjacent foundational concepts.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.groundedHypercalculi, Hyperfields.EcosystemRole.groundedLayer, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.cons, Hyperfields.RepoId, Hyperfields.RepoId.ordinatics, Hyperfields.RepoId.groundedHypersetTheory, List.nil, Hyperfields.OperatingMode, Hyperfields.OperatingMode.compositional, Hyperfields.OperatingMode.communicative
```
def groundedHypercalculi : Entry := mkPublicEntry .groundedHypercalculi
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.groundedHypersetTheory Grounded Hyperset Theory line 275 source
The hyperset layer is grounded in lower-level mathematical structure while supplying APGs, AFA, and bisimulation machinery.
Sources and attribution: Pinned repository

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.mkPublicEntry, Hyperfields.RepoId.groundedHypersetTheory, Hyperfields.EcosystemRole.groundedLayer, Hyperfields.Grounding.grounded, Hyperfields.RepoId.hypermath, List.cons, Hyperfields.RepoId, Hyperfields.RepoId.ordinatics, List.nil, Hyperfields.OperatingMode, Hyperfields.OperatingMode.formative, Hyperfields.OperatingMode.compositional
```
def groundedHypersetTheory : Entry := mkPublicEntry .groundedHypersetTheory
…
```
Mentions: Hyperfields.Entry, Hyperfields.mkPublicEntry
def Hyperfields.registry The complete initial catalogue line 284 source
The complete initial catalogue, with no inference from list order.

List order is presentation order only and carries no hidden hierarchy.

standard axioms: propext what this means
Statement uses: List, Hyperfields.Entry
Proof uses: List.cons, Hyperfields.hyperchaos, Hyperfields.hyperorder, Hyperfields.hyperemergence, Hyperfields.hyperobjectivity, Hyperfields.hypersubjectivity, Hyperfields.hyperreality, Hyperfields.hypertime, Hyperfields.hyperspace, Hyperfields.hypergeometry, Hyperfields.hypertopology, Hyperfields.hyperstructure, Hyperfields.hyperdynamics, Hyperfields.hypermechanics, Hyperfields.hypergrammar, Hyperfields.hyperlogic, Hyperfields.hypermath, Hyperfields.hyperphysics, Hyperfields.hyperethics, Hyperfields.hyperchemistry and 10 more
```
def registry : List Entry := [
…
```
Mentions: Hyperfields.Entry
def Hyperfields.sourceShapeFailures Source-shape failures line 297 source
All entries whose public-source shape is internally valid.

Invalid source-state and coordinate combinations remain explicit instead of being dropped.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Hyperfields.Entry
Proof uses: List.filter, Bool.not, Hyperfields.Entry.sourceShapeValid, Hyperfields.registry
```
def sourceShapeFailures : List Entry := registry.filter (fun entry => !entry.sourceShapeValid)
```
Mentions: Hyperfields.Entry
def Hyperfields.ownerReviewQueue Owner review queue line 302 source
Every initial explanation still awaits Tyler's semantic review.

This list is the operative semantic review backlog for the initial catalogue.

standard axioms: propext what this means
Statement uses: List, Hyperfields.Entry
Proof uses: List.filter, Hyperfields.Entry.awaitingOwnerReview, Hyperfields.registry
```
def ownerReviewQueue : List Entry := registry.filter Entry.awaitingOwnerReview
```
Mentions: Hyperfields.Entry, Hyperfields.Entry.awaitingOwnerReview
theorem Hyperfields.registry_has_28_entries The initial registry has twenty-eight entries line 308 source
The list is explicit, so Lean can reduce its length exactly.
1. Unfold the registry.
2. Compute the list length.
standard axioms: propext what this means
Statement uses: Eq, Nat, List.length, Hyperfields.Entry, Hyperfields.registry, 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 309
  before
```
⊢ registry.length = 28
```
  after
  no goals remain
```
theorem registry_has_28_entries : registry.length = 28 := by
…
```
theorem Hyperfields.registry_sources_are_well_shaped Every source coordinate has the expected shape line 315 source
Public-main entries carry a nonempty repository URL, a forty-character revision, and the main branch; unpublished or no-main entries carry no false pin.
1. Unfold the registry and source-shape checker.
2. Compute every finite case.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, List, Hyperfields.Entry, Hyperfields.sourceShapeFailures, List.nil
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 316
  before
```
⊢ sourceShapeFailures = []
```
  after
  no goals remain
```
theorem registry_sources_are_well_shaped : sourceShapeFailures = [] := by
…
```
Mentions: Hyperfields.sourceShapeFailures
theorem Hyperfields.initial_registry_awaits_owner_review No explanation is silently owner-reviewed line 322 source
The initial catalogue remains visibly pending Tyler's review even though Lean checks its structure.
1. Filter the registry by its review state.
2. Verify that every entry remains in the review queue.
standard axioms: propext what this means
Statement uses: Eq, Nat, List.length, Hyperfields.Entry, Hyperfields.ownerReviewQueue, Hyperfields.registry
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 323
  before
```
⊢ ownerReviewQueue.length = registry.length
```
  after
  no goals remain
```
theorem initial_registry_awaits_owner_review : ownerReviewQueue.length = registry.length := by
…
```