What is hosted here
A first-class ecosystem section
This page, its dedicated Lean module, its source coordinate, and its place in the complete ecosystem directory are published together. It is not merely a row hidden inside a registry.
Groundinggrounded in Hypermath and Ordinatics
Operating modes
- formative
- compositional
Explanation reviewsource-derived, unreviewed
Portal coordinateff739b69f4b4
What Lean checks
Identity and catalogue integration
The dedicated module elaborates an Entry that resolves directly to the canonical registry definition. The release gate also requires this page, its generated Lean page, and its manifest record to agree.
Source boundary
Provenance without authority transfer
The explanatory record is bound to the exact public main commit linked above. Source provenance establishes what was inspected; it does not establish the truth of every external claim.
Semantic boundary
Awaiting owner review
The current explanation remains visibly unreviewed by Tyler. Compilation cannot silently promote source-derived prose to owner-reviewed doctrine.