A Necessary Formation-Theoretic Invariant for Safe Propositional Formation V2

We establish a necessity result identifying a formation-level vulnerability underlying classical self-referential paradoxes. The source of the pathology is shown to be an implicit type confusion that permits unguarded lifting from syntactic entities to propositions, thereby admitting evaluation-dependent constructions into the space of truth-bearers. We prove that, under minimal classical formation assumptions—namely:(1) strict separation between entities and propositions,(2) restriction of truth-valuation to propositions only, and(3) the requirement of explicit, inhabited formation witnesses for all admissible lifts—such evaluation-dependent constructions fail to form propositions at all. Consequently, logical leakage across formation levels is prevented prior to semantic evaluation, rather than being contained post hoc through stratification, partial semantics, or meta-theoretic restrictions. The result is necessity-based and independent of truth-theoretic choices. It does not revise semantics, weaken classical logic, or impose ad hoc semantic constraints. Instead, it identifies a formation-prior admissibility boundary that determines which expressions are eligible to become truth-bearers in the first place. Classical paradoxes are thereby diagnosed as downstream artifacts of formation failure, not as primitive semantic anomalies. The criterion is mechanically validated using two independent formal realizations:an SMT-based encoding in Z3, which eliminates all countermodels while preserving non-trivial well-formed propositions; and a type-theoretic implementation in Cubical Agda, where evaluation-dependent constructions fail at the formation (type-checking) stage prior to any notion of truth or falsity. The result constitutes a formation-prior, necessity-level invariant, formally derived and mechanically verified, which rules out an entire structural class of ill-formed propositions independently of semantics, while remaining conservative with respect to all evaluator-independent and legitimately formed propositions.