classify_permitted
plain-language theorem explainer
Every generator inventory κ produces a generable carrier that is countable and a proper subset of the reals. Objecthood classifiers cite this to mark the "permitted" commitment: free choice of inventory, constrained only by countability and non-totality. The proof is a one-line packaging of the countability and properness lemmas for the generable field.
Claim. For every generator inventory $\kappa:\mathbb{N}\to\mathbb{R}$, the generable field generated by $\kappa$ is a countable set and is not equal to all of $\mathbb{R}$.
background
In the Primitive Recognition Calculus, a generable carrier is the subfield of $\mathbb{R}$ obtained by closing a countable inventory of seed reals under the field operations admitted by the calculus. The inventory is an arbitrary map $\kappa:\mathbb{N}\to\mathbb{R}$; different choices give different carriers, but all remain countable.
The ObjecthoodRegistry module assigns each catalogued RS object a commitment kind: distinction-forced, display, completion, convention, quotient, observable, or permitted. "Permitted" means the inventory is a free but admissible choice: any countable seed set is allowed, provided the resulting carrier stays a proper subset of $\mathbb{R}$.
Upstream, GenerableReal.genField_countable and GenerableReal.genField_proper establish the two halves of that constraint for every $\kappa$. This theorem simply packages them as the registry entry for the permitted class.
proof idea
One-line term proof. For arbitrary $\kappa$, pair the two existing lemmas: countability of the generable field of $\kappa$, and properness (the generable field is not all of $\mathbb{R}$). No new algebra is done here; the theorem is the registry-facing conjunction.
why it matters
This is the registry certificate for the "permitted" cell in the Phase 8 objecthood periodic table. That table records, for each catalogued object, which commitment kind produces it: distinction-forced (rationals, coherence scale), display ($\mathbb{R}_\delta$ value map), completion ($\mathbb{R}$), convention (cost unit), quotient and observable (gauge quotient and probes), and permitted (the generable inventory).
Without this entry, objecthood would look flat: every real would appear equally "given." The permitted class makes explicit that the generable inventory is chosen, not forced, yet still constrained (countable and proper). Downstream the periodic-table theorem assembles these classify_* facts into a typed attribute on every registered object. In the broader RS forcing chain this sits below T5–T8: it does not force $J$, $\varphi$, the eight-tick octave, or $D=3$, but it fixes how free numerical content may enter the calculus without collapsing into the full continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.