GroundedHypercalculi.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

1 declarations, 0 contain sorry, 0 axioms

Grounded Hypercalculi

This module gives Grounded Hypercalculi a first-class page in the unified Hyperfields explainer. The complete source-pinned description and review state live in the registry entry referenced below.

Imports (1)

Hyperfields.Registry

Imported by 1 file

Hyperfields/AllFields.lean

def Hyperfields.Fields.GroundedHypercalculi.entry Grounded Hypercalculi explainer entry line 17 source
The canonical Grounded Hypercalculi record used by the unified portal.

This declaration exposes the checked ecosystem record for Grounded Hypercalculi on its own stable explainer page.
See also: Hyperfields.groundedHypercalculi

standard axioms: propext what this means
Statement uses: Hyperfields.Entry
Proof uses: Hyperfields.groundedHypercalculi
```
def entry : Hyperfields.Entry := Hyperfields.groundedHypercalculi
…
```
Mentions: Hyperfields.Entry, Hyperfields.groundedHypercalculi