MetaDoesNotForceObjectCert
plain-language theorem explainer
A Prop-valued certificate packing two facts: the formal meta-language distinguishes some propositions, yet that meta distinction does not force every inhabited object carrier to be non-singleton. Anyone auditing the honest scope of the T-1 self-bootstrap route cites it. The declaration is a bare structure; a sibling theorem fills both fields from two named lemmas.
Claim. A certificate consisting of two assertions: (i) there exist propositions $P,Q$ with $P \neq Q$; (ii) it is false that every inhabited type $K$ contains distinct elements $x,y \in K$. Together these record that meta-level distinguishability does not uniformly force object-level non-singletonness.
background
The module isolates a sharp limit of the T-1 self-bootstrap route. In the formal language one can distinguish propositions (there exist $P \neq Q$ as Props). That is a meta-level fact about the ambient logic.
Object carriers are ordinary types. The unit type is inhabited and has only one element, so the universal claim "every inhabited $K$ has two distinct points" is false. The certificate packages exactly this separation: meta distinction is real, and it does not push down to a uniform object-level non-singleton theorem.
The same packaging pattern appears nearby in the self-reference stack (meta-realization certificates that record structural obligations without claiming a full instance). Here the content is purely logical scope, not a physical forcing step from the T0–T8 chain.
proof idea
No proof body: this is a structure definition whose type is Prop. The two fields are named hypotheses (existential meta distinction; negation of uniform object non-singletonness). A downstream theorem constructs an inhabitant by assigning meta_language_distinguishes to the first field and meta_distinction_does_not_force_object_distinction to the second. The actual work lives in those two lemmas; the structure only names the bundled claim.
why it matters
It earns its place as the honest-scope package for the self-bootstrap route: meta language can tell propositions apart, yet the unit carrier blocks any claim that every inhabited object type is non-singleton. Downstream, metaDoesNotForceObjectCert is the theorem-backed inhabitant of this certificate, wiring the two sibling lemmas into the structure.
In the broader foundation stack this sits next to self-reference and meta-realization certificates: it prevents over-reading T-1 as forcing object-level multiplicity on every carrier. It does not itself advance T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$); it fences what the bootstrap is allowed to claim so later forcing steps are not smuggled in from pure meta distinction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.