entryOf
plain-language theorem explainer
Packages any proved proposition into a ClosureEntry for the Delta-native strong-closure certificate. Certificate authors cite it when wiring each closed theorem head into a named field. The body is the anonymous structure constructor: pair the proposition with its proof.
Claim. Given a proposition $P$ and a proof $h$ of $P$, form the closure entry whose closed proposition is $P$ and whose proof field is $h$.
background
In the Primitive Recognition Calculus, Delta-native strong closure is recorded as a certificate whose fields are named proof entries rather than bare theorems. A closure entry is a pair: a proposition closed together with a term of that proposition. The surrounding module assembles the full Delta-native surface (real display, generable carrier, certified analytic protocols and transformers, and related layers) into one such certificate.
entryOf is the packaging map from an arbitrary proved proposition into that entry type. Downstream, parameterized layers are stored as functions that return closure entries, so each concrete theorem head is wrapped once and then placed in the certificate record.
proof idea
One-line definition: apply the anonymous constructor of ClosureEntry, setting closed := p and proof := h. No lemmas are invoked.
why it matters
This is the uniform glue used by strongClosureCertificate, the concrete certificate that assembles the closed Delta-native theorem surface. Every field of that certificate (for example deltaReal, generableCarrier, certifiedAnalytic, certifiedTransformers) is built by calling entryOf on an existing theorem head. Without a single packaging constructor, the certificate would either duplicate structure syntax at each field or lose the named-entry discipline that makes the closed surface auditable. It sits in the Foundation layer that underwrites the forcing chain and continuum bridge, but it does not itself advance a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.