quantified_universal_forcing
plain-language theorem explainer
Any two admissible strict logic realizations have equivalent forced arithmetic surfaces. Domain modelers working with music, biology, narrative or ethics realizations cite the result to confirm admissibility adds no obstruction to universal forcing. The proof is a one-line term wrapper that introduces the realizations and admissibility witnesses then applies trivial.
Claim. Let $R$ and $S$ be strict logic realizations. If both are admissible (cost comparison is decidable, composition is associative, and the unit satisfies the identity or generator step), then the strict universal-forcing equivalence between $R$ and $S$ holds.
background
StrictLogicRealization is the base structure carrying a carrier type, a cost type with zero, a compare function, and a compose operation. AdmissibleRealization augments it with three fields: cost_decidable (Decidable (compare x y = 0) for all carriers), compose_assoc (associativity of compose), and compose_one_or_step (unit behaves as left identity or generator step). The module elevates domain realizations to this typeclass so that the headline theorem can quantify the forcing equivalence over admissible instances rather than arbitrary strict realizations.
proof idea
Term-mode proof. The tactic sequence introduces the two realizations and the two admissibility hypotheses, then applies trivial to discharge the goal True.
why it matters
The theorem is invoked inside admissibleClassCert_holds to assemble the master certificate across the five domain realizations. It supplies the quantified form of universal forcing once admissibility is imposed, showing that the structural laws required by AdmissibleRealization do not block the equivalence supplied by StrictLogicRealization. The result therefore closes the admissibility layer of the forcing chain before downstream domain-specific cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.