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

JSON: Used in an explanation or its source, but not expanded by this annotation. Follow its linked source.
L4DEL: Lean4 Domain Explanation Language

12 declarations, 0 contain sorry, 0 axioms

The ecosystem manifest, emitted from the Lean registry

ecosystem.json used to be a hand-maintained file that had to be kept in step with Hyperfields.Registry by hand, and the release gate could only check that the two agreed on the entries that the gate happened to look at. This module removes the duplication: the Lean registry IS the record, and this module renders it.

Running

lake env lean --run Hyperfields.Manifest > ecosystem.json

writes the manifest the portal consumes. The Python side reads the same file, so there is one record of the ecosystem and one place it can be wrong.

The emitted JSON is deliberately plain: one object per entry, with the same field names the portal already used. The renderer is total, so every entry in the registry appears in the output, and the release gate's one-to-one correspondence check now holds by construction rather than by review.

Imports (4)

Imported by 1 file

Hyperfields.lean

def Hyperfields.Manifest.jsonString Escape a string as a JSON string literal line 44 source
Escape a string as a JSON string literal, including the quotes.
Only the characters JSON actually requires to be escaped are escaped. A summary that contained a raw control character would produce invalid JSON, so the five structural escapes are handled and everything else is emitted verbatim.

A summary may contain quotes and backslashes, so the renderer must escape them rather than emit invalid JSON.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String
Proof uses: String.foldl, Char, ite, Eq, Bool, BEq.beq, Char.ofNat, Bool.true, HAppend.hAppend, Char.toString
5 instances, coercions and auxiliary constants left out.
```
def jsonString (value : String) : String :=
…
```

def Hyperfields.Manifest.roleString Render a role as the manifest's role string line 57 source

Render a role as the manifest's role string.

The manifest's vocabulary is fixed and public, so each role maps to exactly one published string.

no axioms what this means

Statement uses: Hyperfields.EcosystemRole, String

Proof uses: Hyperfields.Manifest.roleString.match_1, Unit

def roleString : EcosystemRole → String
  | .hyperfield => "hyperfield"
  | .groundedLayer => "grounded-layer"
  | .structuralHub => "structural-hub"
  | .ordinalInfrastructure => "ordinal-infrastructure"
  | .metaFramework => "meta-framework"

-- L4DEL: title: Render a grounding as the manifest's grounding string
-- L4DEL: intuition: The manifest publishes the same readable grounding the catalogue states, so the renderer delegates to the one place that decides it.
/-- Render a grounding as the manifest's grounding string. -/

Mentions: Hyperfields.EcosystemRole

def Hyperfields.Manifest.groundingString Render a grounding as the manifest's grounding string line 67 source
Render a grounding as the manifest's grounding string.

The manifest publishes the same readable grounding the catalogue states, so the renderer delegates to the one place that decides it.

standard axioms: propext what this means
Statement uses: Hyperfields.Grounding, String
Proof uses: Hyperfields.Grounding.display
```
def groundingString (grounding : Grounding) : String :=
…
```
Mentions: Hyperfields.Grounding

def Hyperfields.Manifest.modeString Render one operating mode as the manifest's mode string line 73 source

Render one operating mode as the manifest's mode string.

The manifest's vocabulary is fixed and public, so each mode maps to exactly one published string.

no axioms what this means

Statement uses: Hyperfields.OperatingMode, String

Proof uses: Hyperfields.Manifest.modeString.match_1, Unit

def modeString : OperatingMode → String
  | .formative => "formative"
  | .communicative => "communicative"
  | .compositional => "compositional"
  | .integrative => "integrative"
  | .reflective => "reflective"

-- L4DEL: title: Render a source state as the manifest's source-state string
-- L4DEL: intuition: The manifest's vocabulary is fixed and public, so each source state maps to exactly one published string.
/-- Render a source state as the manifest's source-state string. -/

Mentions: Hyperfields.OperatingMode

def Hyperfields.Manifest.sourceStateString Render a source state as the manifest's source-state string line 83 source

Render a source state as the manifest's source-state string.

The manifest's vocabulary is fixed and public, so each source state maps to exactly one published string.

no axioms what this means

Statement uses: Hyperfields.SourceState, String

Proof uses: Hyperfields.Manifest.sourceStateString.match_1, Unit

def sourceStateString : SourceState → String
  | .publicMainPinned => "public-main-pinned"
  | .publicWithoutMain => "public-without-main"
  | .localCandidateUnpublished => "local-candidate-unpublished"

-- L4DEL: title: Render a review state as the manifest's review-state string
-- L4DEL: intuition: The manifest's vocabulary is fixed and public, so each review state maps to exactly one published string.
/-- Render a review state as the manifest's review-state string. -/

Mentions: Hyperfields.SourceState, main

def Hyperfields.Manifest.reviewString Render a review state as the manifest's review-state string line 91 source
Render a review state as the manifest's review-state string.

The manifest's vocabulary is fixed and public, so each review state maps to exactly one published string.

no axioms what this means
Statement uses: Hyperfields.ReviewState, String
Proof uses: Hyperfields.Manifest.reviewString.match_1, Unit
```
def reviewString : ReviewState → String
  | .sourceDerivedUnreviewed => "source-derived-unreviewed"
  | .ownerReviewed => "owner-reviewed"

-- L4DEL: title: Render the kind of a grounding as a closed tag
-- L4DEL: intuition: A consumer must be able to tell the three grounding kinds apart without parsing prose, so the kind is published as its own closed value.
/-- Render the kind of a grounding as a closed tag. -/
```
Mentions: Hyperfields.ReviewState
def Hyperfields.Manifest.groundingKindString Render the kind of a grounding as a closed tag line 98 source
Render the kind of a grounding as a closed tag.

A consumer must be able to tell the three grounding kinds apart without parsing prose, so the kind is published as its own closed value.

no axioms what this means
Statement uses: Hyperfields.Grounding, String
Proof uses: Hyperfields.Manifest.groundingKindString.match_1, Unit, Hyperfields.RepoId, List
```
def groundingKindString : Grounding → String
  | .fieldPrimitive => "field-primitive"
  | .grounded _ _ => "grounded"
  | .unresolved => "unresolved"

-- L4DEL: title: Render the bases a grounded entry stands on
-- L4DEL: intuition: A grounded entry names its upstream fields as data, so a consumer can reason about the dependency without parsing the prose form.
/-- Render the bases a grounded entry stands on, primary first. -/
```
Mentions: Hyperfields.Grounding
def Hyperfields.Manifest.groundingBases Render the bases a grounded entry stands on line 106 source
Render the bases a grounded entry stands on, primary first.

A grounded entry names its upstream fields as data, so a consumer can reason about the dependency without parsing the prose form.

standard axioms: propext what this means
Statement uses: Hyperfields.Grounding, List, String
Proof uses: Hyperfields.Manifest.groundingBases.match_1, Hyperfields.RepoId, List.cons, Hyperfields.RepoId.displayName, List.map, List.nil
```
def groundingBases (grounding : Grounding) : List String :=
…
```
Mentions: Hyperfields.Grounding
def Hyperfields.Manifest.renderEntry Render one entry as a JSON object line 126 source
Render one entry as a JSON object.
The field set is fixed. A coordinate that does not exist is published as null rather than omitted, so a consumer can tell "there is no repository" apart from "this manifest does not say".
The grounding is published twice on purpose. grounding is the prose the portal prints, and groundingKind plus groundingBases are the structured form. A consumer that wants to branch on the kind of grounding must not have to parse the prose, and a consumer that wants to print the prose must not have to reconstruct the list-joining rules.

Every entry publishes the same thirteen fields, so a field cannot appear for one repository and be missing for another.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hyperfields.Entry, String
Proof uses: List, Prod, List.cons, Prod.mk, Hyperfields.Manifest.jsonString, Hyperfields.Entry.slug, Hyperfields.Entry.displayName, Hyperfields.RepoId.moduleName, Hyperfields.Entry.id, Hyperfields.Manifest.roleString, Hyperfields.Entry.role, Hyperfields.Manifest.groundingString, Hyperfields.Entry.grounding, Hyperfields.Manifest.groundingKindString, HAppend.hAppend, String.intercalate, List.map, Hyperfields.Manifest.groundingBases, Hyperfields.OperatingMode, Hyperfields.Manifest.modeString and 16 more
2 instances, coercions and auxiliary constants left out.
```
def renderEntry (entry : Entry) : String :=
…
```
Mentions: Hyperfields.Entry
def Hyperfields.Manifest.render Render the whole manifest line 154 source
Render the whole manifest.

The manifest carries the portal revision it was built for, so a published copy can be bound to the commit that produced it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Hyperfields.Entry, String
Proof uses: HAppend.hAppend, Hyperfields.Manifest.jsonString, String.intercalate, List.map, Hyperfields.Manifest.renderEntry
2 instances, coercions and auxiliary constants left out.
```
def render (entries : List Entry) (portalRevision : String) : String :=
…
```
Mentions: Hyperfields.Entry
def Hyperfields.Manifest.allEntries Every entry the registry holds line 173 source
Every entry the registry holds, in the order the portal lists them.
This is the registry's own list, not a second list. A hand-maintained copy here could disagree with Hyperfields.registry about which entries exist and in what order, and the disagreement would only show up as a portal that publishes a different sequence than the one Lean checks.

The manifest renders the registry's own list, so a second copy here could disagree about which entries exist and in what order.

standard axioms: propext what this means
Statement uses: List, Hyperfields.Entry
Proof uses: Hyperfields.registry
```
def allEntries : List Entry := Hyperfields.registry
…
```
Mentions: Hyperfields.Entry, Hyperfields.registry
def main The manifest emitter line 192 source
The emitter renders the Lean registry as JSON, so the published record is a build product rather than a second copy of the declarations.
Prerequisites: Hyperfields.Manifest.render

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, String, IO, Unit
Proof uses: ite, Eq, Bool, List.contains, Bool.true, IO.println, Hyperfields.Bridges.renderBridges, Bind.bind, IO.Error, Option, liftM, BaseIO, EIO, IO.getEnv, Hyperfields.Manifest.renderEntry.match_2, Hyperfields.Manifest.render, Hyperfields.Manifest.allEntries
9 instances, coercions and auxiliary constants left out.
```
def main (args : List String) : IO Unit := do
…
```