webpage: Operator Firing Order as a Mechanism for Ethanol-to-Hydrocarbon Selectivity: A Contact-Geometric Analysis of ZSM-5 and MCM-22 Zeolites Description: Zeolite pore topology governs product selectivity in ethanol conversion to hydrocarbons, yet the mechanism by which topology determines which intermediates form and survive has remained unresolved: HZSM-5 and HMCM-22 have nominally identical acid chemistry and both possess 10-ring apertures, but produce markedly different product distributions, coke locations, and deactivation profiles. This paper proposes that the differentiating variable is the sequential firing order of four geometric operations experienced by a reacting intermediate: Compression (adsorption, C), Constraint (aperture gating, K), Folding (branching/oligomerization/aromatization, F), and Unfolding (selective desorption, U). ZSM-5's 10-ring channels enforce the order C▷K▷F▷U (constraint before folding); MCM-22's 12-ring supercages and external pockets enforce C▷F▷K▷U (folding before constraint). Version 3 locates exactly where the order-dependence comes from — and corrects v2 on this point (see below): the aperture gate commutes exactly with a pointwise nonlinearity, so it is the fold's inter-site coupling (amplitude transport) that fails to commute, both with the on-site nonlinearity and, in consequence, with the gate. All three commutation facts are kernel-verified in Lean 4. The hypothesis is supported by five independent published lines of evidence (molecular dynamics, operando DRIFTS, and structural-modification studies, reread through the operator-order lens), a reproducible coarse-grained nonlinear-Schrödinger (DNLS) simulation in which the two orders produce a ~35× selectivity ratio, and seven formal theorems connecting the hypothesis to the simulation model. Every claim carries an explicit status tag — [VERIFIED] (Lean 4 kernel), [MODEL], [SIMULATION], or [OPEN] — and nothing outside the first tag is presented as proved. Three falsifiable predictions are derived, each with an explicit experimental protocol and pass/fail criterion, directly testable by contact-time DRIFTS. The formal layer is machine-checked: the accompanying Lean 4 development (github.com/TOTOGT/io) compiles against the Lean kernel in continuous integration on every commit, with per-theorem axiom audits (#print axioms) showing exactly [propext, Classical.choice, Quot.sound] — no sorryAx — for all 19 verified theorems: the three commutation theorems of the corrected Theorem 1 (ZeoliteCommutation.lean), nine supporting results (CatGT_Main.lean), and seven chain-level order-dependence theorems in exactly existential form (Theorem53NonCommutativity.lean). The remaining obligations (continuum-limit gate/fold non-commutation, the contact-morphism scaling law, the selectivity–order bijection) are explicitly tracked as open. No claim in this work is asserted as machine-verified without a corresponding, inspectable CI log. Changes in v3. Theorem 1 of v1–v2 asserted [K,F] ≠ 0 for the aperture gate and a pointwise fold via an unsupported boundary-term argument; that statement was false — the two commute exactly, for every state. Theorem 1 is restated as a three-part locus-of-non-commutativity theorem, all three parts kernel-verified; downstream claims are re-tagged accordingly. The v2 supplements ALGEBRAIC_PROOFS_ALL_7_THEOREMS.md, CatGT_PROOFS_COMPLETE.lean, and CatGT_v2.lean are withdrawn (the Lean files compiled only because sorry compiles) and replaced by OPERATOR_ORDER_DERIVATIONS_AND_STATUS.md and ZeoliteCommutation.lean. Files: manuscript (.tex/.pdf), DNLS simulation code (dm3_dnls_zeolite_simulation.py), figures, kernel-checked Lean 4 proofs (ZeoliteCommutation.lean), and derivations with per-claim verification status (OPERATOR_ORDER_DERIVATIONS_AND_STATUS.md).