`Hyperfields/Core.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
URL: Used in an explanation or its source, but not expanded by this annotation. Follow its linked source.

16 declarations, 0 contain sorry, 0 axioms

A typed vocabulary for the hyperfield ecosystem

The types in this module keep four questions separate:

What kind of ecosystem artifact is this?
Is its presentation field-primitive, grounded in another field, or unresolved?
How does it operate: formatively, communicatively, compositionally, integratively, or reflectively?
How far has this catalogue entry itself been reviewed?

Compiling the vocabulary checks those distinctions. It does not prove that a repository has found physically or metaphysically absolute axioms.

Imports (1)

Imported by 4 files

inductive Hyperfields.RepoId Stable ecosystem identifiers line 23 source
Stable identifiers for repositories and unpublished field candidates known to this catalogue.

A closed identifier type prevents dependencies from being recorded as misspelled free text.

no axioms what this means
```
inductive RepoId where
…
```
def Hyperfields.RepoId.moduleName The explainer module a repository is explained in line 56 source
The name of the dedicated Lean module that explains this repository.

Every catalogued repository has one dedicated explainer module, so a field cannot be present in an aggregate while absent from the public surface.

no axioms what this means
Statement uses: Hyperfields.RepoId, String
Proof uses: Hyperfields.instReprRepoId.repr.match_1, Unit
```
def RepoId.moduleName : RepoId → String
  | .hyperchaos => "Hyperchaos"
  | .hyperorder => "Hyperorder"
  | .hyperemergence => "Hyperemergence"
  | .hyperobjectivity => "Hyperobjectivity"
  | .hypersubjectivity => "Hypersubjectivity"
  | .hyperreality => "Hyperreality"
  | .hypertime => "Hypertime"
  | .hyperspace => "Hyperspace"
  | .hypergeometry => "Hypergeometry"
  | .hypertopology => "Hypertopology"
  | .hyperstructure => "Hyperstructure"
…
```
Mentions: Hyperfields.RepoId, Hyperfields.hyperchaos, Hyperfields.hyperorder, Hyperfields.hyperemergence, Hyperfields.hyperobjectivity, Hyperfields.hypersubjectivity, Hyperfields.hyperreality, Hyperfields.hypertime, Hyperfields.hyperspace, Hyperfields.hypergeometry, Hyperfields.hypertopology, Hyperfields.hyperstructure
def Hyperfields.RepoId.displayName The readable name of a repository line 99 source
The published display name of a repository.
This is not the module name. grounded-hypercalculi is explained by the module GroundedHypercalculi but published under the title "Grounded Hypercalculi", and meta-morphoscripted-origination is published as "Meta-Morphoscripted-Origination" under the module MetaMorphoscriptedOrigination. Keeping the two apart lets the catalogue name a repository the way its owner names it and still point at the module that checks the entry.

A repository's display name is its published title, which is not always the same as the module that explains it.

no axioms what this means
Statement uses: Hyperfields.RepoId, String
Proof uses: Hyperfields.instReprRepoId.repr.match_1, Unit
```
def RepoId.displayName : RepoId → String
  | .hyperchaos => "Hyperchaos"
  | .hyperorder => "Hyperorder"
  | .hyperemergence => "Hyperemergence"
  | .hyperobjectivity => "Hyperobjectivity"
  | .hypersubjectivity => "Hypersubjectivity"
  | .hyperreality => "Hyperreality"
  | .hypertime => "Hypertime"
  | .hyperspace => "Hyperspace"
  | .hypergeometry => "Hypergeometry"
  | .hypertopology => "Hypertopology"
  | .hyperstructure => "Hyperstructure"
…
```
Mentions: Hyperfields.RepoId, Hyperfields.hyperchaos, Hyperfields.hyperorder, Hyperfields.hyperemergence, Hyperfields.hyperobjectivity, Hyperfields.hypersubjectivity, Hyperfields.hyperreality, Hyperfields.hypertime, Hyperfields.hyperspace, Hyperfields.hypergeometry, Hyperfields.hypertopology, Hyperfields.hyperstructure
def Hyperfields.RepoId.slug The catalogue slug of a repository line 139 source
The catalogue slug of a repository: the URL segment the portal publishes it under.
Most slugs are the identifier spelled in lower case. Three are not, because their owners' repository names are hyphenated, and the catalogue publishes the owner's spelling rather than a normalised one.

The slug is the published URL segment, so it must be a function of the identifier rather than a second hand-written list.

no axioms what this means
Statement uses: Hyperfields.RepoId, String
Proof uses: Hyperfields.instReprRepoId.repr.match_1, Unit
```
def RepoId.slug : RepoId → String
  | .hyperchaos => "hyperchaos"
  | .hyperorder => "hyperorder"
  | .hyperemergence => "hyperemergence"
  | .hyperobjectivity => "hyperobjectivity"
  | .hypersubjectivity => "hypersubjectivity"
  | .hyperreality => "hyperreality"
  | .hypertime => "hypertime"
  | .hyperspace => "hyperspace"
  | .hypergeometry => "hypergeometry"
  | .hypertopology => "hypertopology"
  | .hyperstructure => "hyperstructure"
…
```
Mentions: Hyperfields.RepoId, Hyperfields.hyperchaos, Hyperfields.hyperorder, Hyperfields.hyperemergence, Hyperfields.hyperobjectivity, Hyperfields.hypersubjectivity, Hyperfields.hyperreality, Hyperfields.hypertime, Hyperfields.hyperspace, Hyperfields.hypergeometry, Hyperfields.hypertopology, Hyperfields.hyperstructure
inductive Hyperfields.EcosystemRole Ecosystem roles line 171 source
A repository's role is distinct from whether its internal account is grounded.

A repository's role in the map is independent of whether the structure it presents is grounded in another field.

no axioms what this means
```
inductive EcosystemRole where
…
```
inductive Hyperfields.Grounding Relative grounding line 185 source
Grounding is relative to the presentation recorded here. fieldPrimitive means "presented as primitive inside this field", not "proved absolutely primitive in reality".

A field may be primitive in its own presentation, explicitly grounded in named upstream structure, or still unresolved.

no axioms what this means
```
inductive Grounding where
…
```
def Hyperfields.joinNames The readable form of a grounding line 201 source
Join a list of names the way the catalogue joins them, with a serial comma before the final item when there are three or more.
Two items join with "and" alone. Three or more join with a comma before "and", so a reader can see where the list ends. This is the same rendering the published catalogue has always used.

A grounding names the fields it stands on, so the readable form must say which, not merely that a grounding exists.

standard axioms: propext what this means
Statement uses: List, String
Proof uses: Hyperfields.joinNames.match_1, Unit, HAppend.hAppend, ToString.toString, List.getLastD, List.dropLast, String.intercalate
3 instances, coercions and auxiliary constants left out.
```
def joinNames (names : List String) : String :=
…
```
def Hyperfields.Grounding.display Render a grounding as text line 222 source
Render a grounding as the sentence the catalogue publishes.
fieldPrimitive is rendered "field-relative primitive", not "primitive", because being primitive inside one field's own presentation is a claim about that presentation and not a claim about reality. A grounded entry names its primary basis first and then any additional bases.

A grounding names the fields it rests on, and the rendering joins them the way a sentence would rather than the way a list would.
Prerequisites: Hyperfields.Grounding

standard axioms: propext what this means
Statement uses: Hyperfields.Grounding, String
Proof uses: Hyperfields.Grounding.display.match_1, Unit, Hyperfields.RepoId, List, List.cons, Hyperfields.RepoId.displayName, List.map, HAppend.hAppend, ToString.toString, Hyperfields.joinNames
3 instances, coercions and auxiliary constants left out.
```
def Grounding.display (grounding : Grounding) : String :=
…
```
Mentions: Hyperfields.Grounding
inductive Hyperfields.OperatingMode Operating modes line 233 source
Multiple modes may describe one field; communicative and formative are not opposites.

A field can expose formative structure while also communicating, composing, integrating, or reflecting across fields.

no axioms what this means
```
inductive OperatingMode where
…
```
inductive Hyperfields.SourceState Public source state line 244 source
What public source coordinate is available for an entry.

A pinned main commit, a repository without a main ref, and an unpublished local candidate require different evidence claims.

no axioms what this means
```
inductive SourceState where
…
```
inductive Hyperfields.ReviewState Explanation review state line 253 source
Review state of the explanatory text in this repository, not of the source project.

Compiling generated or source-derived prose cannot silently convert it into Tyler-reviewed prose.

no axioms what this means
```
inductive ReviewState where
…
```
structure Hyperfields.SourceCoordinate Exact source coordinate line 270 source
Exact public bytes used as the source for an explanatory entry.
revision is optional because a public repository can exist without a resolvable main commit. A repository URL alone is still a true coordinate claim: the repository is public, but no commit was pinned, so the entry carries publicWithoutMain rather than a false forty-character pin. Keeping the revision optional in the type keeps that distinction visible to Lean instead of hiding it behind an empty string.

Repository, revision, and branch travel together so an explanation can be bound to source bytes.

no axioms what this means
```
structure SourceCoordinate where
…
```
structure Hyperfields.Entry One hyperfield ecosystem entry line 282 source
One ecosystem entry. summary is explanatory prose; its review field prevents that prose from being confused with a kernel-checked theorem.

Identity, role, grounding, operating modes, prose, source evidence, and review state remain separately visible.

no axioms what this means
```
structure Entry where
…
```
def Hyperfields.Entry.sourceShapeValid Validate the shape of a source claim line 308 source
A public-main entry is internally well-shaped only when it carries an exact source coordinate.
The three states are checked separately because they make different claims. A pinned entry claims a specific commit and therefore needs all three coordinates. A publicWithoutMain entry claims only that a public repository exists, so it must carry a repository and must not carry a revision it cannot honour. An unpublished candidate must carry no public coordinate at all.

A public-main claim needs a repository, a forty-character revision, and the main branch; a public repository without a main commit may carry the repository alone; unresolved source states must not carry a false pin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hyperfields.Entry, Bool
Proof uses: Hyperfields.Entry.sourceShapeValid.match_2, Hyperfields.SourceState, Option, Hyperfields.SourceCoordinate, Hyperfields.Entry.sourceState, Hyperfields.Entry.source, Bool.and, Bool.not, String.isEmpty, Hyperfields.SourceCoordinate.repository, Hyperfields.Entry.sourceShapeValid.match_1, String, Hyperfields.SourceCoordinate.revision, BEq.beq, Nat, String.length, OfNat.ofNat, Unit, Bool.false, Hyperfields.SourceCoordinate.branch and 2 more
4 instances, coercions and auxiliary constants left out.
```
def Entry.sourceShapeValid (entry : Entry) : Bool :=
…
```
Mentions: Hyperfields.Entry
def Hyperfields.Entry.awaitingOwnerReview Identify explanations awaiting owner review line 326 source
No entry may claim owner review merely because this Lean catalogue compiles.

Structural compilation and semantic review are separate gates.

no axioms what this means
Statement uses: Hyperfields.Entry, Bool
Proof uses: BEq.beq, Hyperfields.ReviewState, Hyperfields.Entry.review, Hyperfields.ReviewState.sourceDerivedUnreviewed
1 instances, coercions and auxiliary constants left out.
```
def Entry.awaitingOwnerReview (entry : Entry) : Bool :=
…
```
Mentions: Hyperfields.Entry
theorem Hyperfields.grounded_has_primary A grounded entry names an upstream basis line 333 source
Grounding is carried by the constructor, so a grounded record cannot omit its primary dependency.
1. Inspect the grounded constructor.
2. Return its required primary repository identifier.
no axioms what this means
Statement uses: Hyperfields.RepoId, List, Exists, Eq, Hyperfields.Grounding, Hyperfields.Grounding.grounded
Proof uses: Exists.intro, rfl
Tactic trace: 1 steps
1. exact ⟨primary, rfl⟩ line 335
  before
```
primary : RepoId
additional : List RepoId
⊢ ∃ basis, Grounding.grounded primary additional = Grounding.grounded basis additional
```
  after
  no goals remain
```
theorem grounded_has_primary (primary : RepoId) (additional : List RepoId) :
    ∃ basis, Grounding.grounded primary additional = Grounding.grounded basis additional := by
…
```
Mentions: Hyperfields.RepoId