isomorphism
plain-language theorem explainer
Definitional record for a structure-preserving bijection between two models in the Primitive Recognition Calculus first-order language. Used locally when cardinality gaps are invoked to block any identification of the reals with a countable elementary equivalent. No proof: pure structure data packaging the map and preservation witnesses.
Claim. An isomorphism is a bundled structure-preserving bijection between two models of the Primitive Recognition Calculus first-order language. In particular, if two models have distinct cardinalities, no such isomorphism can exist, so $\mathbb{R}\simeq N$ is ruled out for any countable model $N$.
background
The ambient module studies non-forcing: whether first-order model theory can pin down the real continuum (or the PRC carrier) up to unique isomorphism. Imports are Mathlib satisfiability, real cardinality, and the continuum cardinal.
Sibling results in the same file establish that the reals admit a countable elementary-equivalent model, hence are not first-order categorical, and that the first-order theory is underdetermined. The present structure is the witness type for sameness of models: once cardinalities differ, the witness type is empty.
In the broader Foundation layer this separates what pure FO logic can say from what the Recognition Composition Law and the T5–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) actually supply.
proof idea
Definitional structure only: no tactics, no lemmas, no proof body. Fields package the underlying map together with the language-preservation obligations as data. Downstream non-categoricity arguments then observe that distinct cardinals make the type uninhabited.
why it matters
Local load-bearing definition for the non-forcing cluster: real_not_first_order_categorical, real_has_countable_ee_model, and real_first_order_underdetermined. Those results underwrite a Foundation claim that PRC physics is not a first-order inevitability; the J-cost functional equation and the forcing chain carry content FO model theory cannot recover.
Reported downstream edges (cohomology isos, arithmetic toNat bridges, sparse $\mu$ reductions) are largely name-collisions with Mathlib isomorphism infrastructure rather than genuine consumers of this PRC structure. Scientific significance stays inside the model-theory non-forcing argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.