What Elimination Leaves Behind: Definability and the Limits of Metaphysical Reduction in Polynomial S5 Semantics

What is eliminated when a modal semantics dispenses with possible worlds? Polynomial ring semantics for finite S5 has exactly the same resolution on modal truth-types as Kripke semantics, so it reveals no additional modal facts. Its diagnostic value lies elsewhere: redundant formula-indexed coordinates, a quotient of world structure, and information irreducible to a chosen base coexist in one formalism and can be separated. We prove that every admissible valuation decomposes into an actual categorical assignment and a definable profile of alternatives containing it. Formula-indexed modal coordinates can be eliminated without eliminating that profile. More generally, every Boolean subalgebra of the finite proposition algebra determines a possible reduction base, a partition of the semantic carrier, adjoint upper and lower envelopes, and an exact ambiguity gap. The bases form a lattice; actual-base and cluster invariance are two points whose meet contains only the constants. The profile-ring presentation adds explicit polynomial envelopes, gap polynomials, and deal-membership certificates for an arbitrary generated base. For the actual-atom base, direct elimination removes the profile coordinates from the envelopes and is stable under vocabulary restriction. Exact support bounds quantify the modal variation that remains. Finally, projectivity classifies symmetric independent-inclusion probability laws, while mixtures and natural selectors show that neither a probabilistic nor a deterministic completion is forced. The resulting position is constructive but neutral: algebraic semantics parameterizes the base of a reduction claim, and polynomial coordinates exhibit its certificates, while probability, law selection, and grounding still require additional bridge principles.