Two-Locality and Finite Two-Variable Axiomatizations of iEx-Logic

We study the equational presentation of the common sequent validities of Heyting algebras and orthomodular algebras with Sasaki implication. Over the fixed fundamental-algebra base in the signature {meet, join, implication, 0, 1}, an algebra is an Ex-algebra if and only if each of its full-signature subalgebras generated by at most two elements is an Ex-algebra. The proof constructs a regular orthomodular quotient and a Heyting prime-filter representation, using a commutator ideal and its Boolean quotient for prime-negation extension. Consequently, a finite additional basis with at most two variables exists. This existence proof is nonconstructive and does not supply an explicit list. A selector construction proves that the global minimum number of additional equations with at most three variables is one. We also classify the inclusion-minimal subsets of a named eight-principle basis: exactly two, of sizes five and six. Complete finite witnesses establish four independent principles. A separate nonderivability theorem distinguishes the explicitly restricted fundamental sequent rules from ordinary equational consequence. The results cover arbitrary cardinalities and arbitrary terms in the original signature. The paper includes self-contained proofs, ancillary adjunction and quotient results, and counterexamples to failed shortcuts. The source archive contains the manuscript and complete finite-algebra tables with replay scripts.