Sousa et al. (2014) posed a specific mechanistic question that remains unanswered: HZSM-5 and HMCM-22 zeolites have nominally identical acid chemistry and both possess 10-ring apertures, yet ethanol conversion over them produces markedly different product distributions, coke locations, and deactivation profiles. This paper proposes a mechanism and states it as a testable theorem.
The central result, the Self-Trapping Selectivity Principle (Theorem 1), models the reaction coordinate on a contact manifold \(\mathcal{X}_\text{cat}\) whose Reeb vector field \(R=\partial_z\) supplies coordinate structure — but, being volume-preserving, cannot itself confine anything. The actual confinement comes from the DNLS equation's self-trapping transition: pathways whose radial coordinate satisfies \(r \leq r^*(\lambda)\) remain confined, where \(r^*\) is the DNLS self-trapping width — \(4aJ/(\lambda P)\) at fixed conserved norm \(P\), the convention adopted here for quasi-one-dimensional channels, or \(a\sqrt{J/\lambda}\) at fixed peak amplitude — \(a\) is a lattice-spacing length scale, \(J\) is inter-site coupling, and \(\lambda\) is the on-site binding energy. Zeolite pore selectivity and Pt–Sn metal-ensemble effects (Corollary 1) are both instances of this one confinement mechanism. Two falsifiable predictions are stated. A third, the DNLS self-trapping threshold in zeolite pores (Prediction 1), is reopened in this version: its 2026-09-19 formula is withdrawn because the formula and its accompanying sentence contradicted each other and its supporting argument misread the literature parameter χ = λN/J (see §4 and the To-Do).
This is a narrower paper than earlier drafts. A macroscopic extrudate-shape corollary and a seven-domain "Coherence Bridge" claiming the same functional form recurs across unrelated physical systems (Faraday rotation, swarm intelligence, the Collatz conjecture among them) have been cut — neither survived scrutiny as evidence for anything beyond the two catalytic cases actually tested here, and dimensional analysis alone predicts the shared functional form without requiring shared geometry. What remains is scoped to what can be checked: zeolite selectivity and Pt–Sn ensembles, against real literature, with the open items — a quantitative fit against Sousa et al.'s actual measured selectivity, and the connection between the DNLS confinement claim and a fixed point of the discrete operator pipeline — stated as open rather than assumed. A Lean 4 formal verification of the core inequality accompanies this paper.
Keywords: zeolite shape-selectivity · HZSM-5 · HMCM-22 · Pt–Sn ensemble effect · discrete nonlinear Schrödinger equation · contact geometry · self-trapping · Lean 4
Sousa et al. (2014) compared ethanol-to-hydrocarbon conversion over HZSM-5 and HMCM-22 zeolites — both 10-ring, nominally identical acid chemistry — and found markedly different product distributions, coke locations, and deactivation profiles. Their in-situ DRIFTS data is direct evidence that pore topology, not acidity, is the operative variable, but the mechanism connecting topology to the observed selectivity difference was not derived. A separate but structurally similar question exists for Pt–Sn bimetallic catalysts: Sn promotion is well established to increase propylene selectivity in propane dehydrogenation by breaking up large Pt ensembles (a geometric, not electronic, effect), but the two are not usually treated as instances of the same underlying mechanism.
This paper proposes that both are: a single confinement mechanism, modeled on the discrete nonlinear Schrödinger (DNLS) equation, in which a reaction pathway's spatial extent is bounded by a self-trapping radius \(r^*(\lambda)\) set by the competition between inter-site coupling and on-site binding energy. Zeolite pore geometry and Pt-ensemble size are two different physical realizations of the same bound.
The confining mechanism needs stating carefully, because an earlier version of this claim was wrong. The reaction coordinate is modeled on a contact manifold \(\mathcal{X}_\text{cat}\) whose Reeb vector field \(R=\partial_z\) supplies coordinate structure — but a Reeb flow preserves contact volume and so cannot have an attracting set of smaller volume than its basin (so no attracting fixed point, periodic orbit or lower-dimensional attractor; the whole space trivially attracts itself, so the qualification is needed), for any choice of contact form, on any contact manifold. The actual confinement is not the Reeb flow; it is the DNLS equation's self-trapping transition, a separate and genuinely different mechanism, stated as Theorem 1 below. (Corrected 2026-09-19: earlier drafts called the Reeb orbits "helical attractors" — they are neither helical nor attracting.)
We define the catalyst contact manifold as \(\mathcal{X}_\text{cat} = (\mathbb{R}^3, \alpha_\text{cat})\) with \(\alpha_\text{cat} = dz - r^2\,d\theta\) in cylindrical coordinates \((r, \theta, z)\), where \(r\) is the pore aperture (Å), \(\theta\) is the catalytic cycle phase, and \(z\) is the reaction coordinate.
Note (2026-09-21): with this \(\alpha_\text{cat}\), \(d\alpha_\text{cat}=-2r\,dr\wedge d\theta\) and \(\alpha\wedge d\alpha=-2r\,dz\wedge dr\wedge d\theta\). The factor \(r\) is an artefact of the polar chart, which degenerates on the axis. With \(u=r\cos\theta,\ v=r\sin\theta\) one has \(r^2d\theta=u\,dv-v\,du\), so \(\alpha_\text{cat}=dz-(u\,dv-v\,du)\), \(d\alpha_\text{cat}=-2\,du\wedge dv\) and \(\alpha\wedge d\alpha=-2\,du\wedge dv\wedge dz\), nowhere zero on \(\mathbb{R}^3\), the axis included. So \(\alpha_\text{cat}\) is a contact form on all of \(\mathbb{R}^3\) (negative for the orientation \(du\wedge dv\wedge dz\), in the sense of Etnyre 2006), and the restriction to \(r\neq0\) stated in the 2026-09-20 note is not needed. DERIVED by hand, not formalized.
The Reeb vector field (defined by \(\iota_R d\alpha = 0\) and \(\alpha(R) = 1\); Geiges 2010, §2.5) is \(R = \partial_z\), and it does satisfy both — the pairing \(\alpha(R)=1\) is machine-checked (reeb_alpha_eq_one). In the separate file ReebFlow.lean, kernel-checked 2026-09-21 under Lean 4.32.0 / Mathlib v4.32.0 (eight axiom reports on the three standard axioms, no warnings), the following are verified in an elementary coordinate model: the orbit has velocity \(R\) and satisfies the flow law; the flow preserves \(\alpha\) (with the tangent map the actual Fréchet derivative); \(\iota_R d\alpha=0\); and the flow preserves \(\alpha\wedge d\alpha\). There \(d\alpha\) is defined from \(\alpha\) by the constant-field formula, not typed in. In ReebFlowExtDeriv.lean (kernel-checked 2026-09-21, same toolchain; eleven axiom reports on the three standard axioms, linter warnings only) it is proved equal to Mathlib's extDeriv of \(\alpha_\text{cat}\) as a Mathlib 1-form, with value \(-2r\,dr\wedge d\theta\), and \((\alpha\wedge d\alpha)(\partial_r,\partial_\theta,\partial_z)=-2r\); the wedge itself is still the explicit formula, not a Mathlib wedge. In ReebNoAttractor.lean (kernel-checked 2026-09-21, same toolchain; nine axiom reports on the three standard axioms) the step from volume preservation to no attracting set is verified in the elementary \((r,\theta,z)\)-chart model: \(\mu(U)\le\mu(A)\) for measure-preserving maps and a closed \(A\) with finite-measure thickening; translation preserves Lebesgue measure; a nonempty closed invariant set attracting a neighbourhood of itself is the whole space; there is no nonempty compact invariant set; and the unqualified claim is refuted (the whole space attracts itself). Still by hand: that the contact volume is a constant multiple of Lebesgue measure in the Cartesian chart, and that the model flow is the manifold's Reeb flow; no single theorem instantiates the general result at the Reeb flow. The Lean file defines the orbit as \((r_0,\theta_0,z_0+t)\) and proves its \(z\)-advance is \(t\,\alpha(R)\); that this curve is the integral curve of \(R\) is by inspection. But its integral curves \((r_0, \theta_0, z_0 + t)\) hold \(r\) and \(\theta\) fixed: they are straight vertical lines, not helices. And since the Reeb flow preserves \(\alpha\) (hence \(\alpha \wedge d\alpha\), the contact volume), it is volume-preserving and therefore cannot have an attracting set of smaller volume than its basin (so no attracting fixed point, periodic orbit or lower-dimensional attractor; the whole space trivially attracts itself, so the qualification is needed), for any choice of contact form on any contact manifold. Proof sketch (derived by hand): if a closed set \(A\) attracts every point of \(U\), the sets \(E_N=\{x\in U:\phi_n x\in A_\varepsilon\ \forall n\ge N\}\) increase to a set containing \(U\) and each has measure at most \(\mu(A_\varepsilon)\), so \(\mu(U)\le\mu(A)\). For this flow, translation in \(z\) and an isometry, more is true: a nonempty closed invariant set attracting a neighbourhood of itself is all of \(\mathbb{R}^3\), and there is no nonempty compact invariant set. (The flow of \(R\) is the case \(H\equiv-1\) of Gaset et al. 2020, Prop. 9, where \(X_{-1}=R\).) Dissipation on a contact manifold requires a contact Hamiltonian flow \(X_H\) with \(R(H)\neq0\): there \(\mathcal{L}_{X_H}\alpha=-R(H)\alpha\), so \(\mathcal{L}_{X_H}(\alpha\wedge d\alpha)=-2R(H)\,\alpha\wedge d\alpha\) (derived by hand). This paper does not derive its confinement from such a flow. (Corrected 2026-09-19; see Theorem 1.) The actual confinement claimed below comes from the DNLS equation's self-trapping transition, a separate and genuinely dissipative-free localization phenomenon (Eilbeck, Lomdahl & Scott 1985) — the contact manifold supplies coordinates, not the confining dynamics.
Define the pipeline \(G = U \circ F \circ K \circ C\), where the four operators act on a state \(\psi \in L^2(\mathcal{X}_\text{cat})\):
| Operator | Physical role | Catalytic interpretation |
|---|---|---|
| \(C\) | Compression | Adsorption / pore entry |
| \(K\) | Constrained path | Transition-state geometry; pore wall constraint |
| \(F\) | Fold | Selectivity filter; irreversible branching |
| \(U\) | Stabilisation | Product desorption; catalyst regeneration |
On a lattice of \(N\) catalytic sites, the DNLS equation is:
\[ i\dot{\psi}_n = -J(\psi_{n+1} + \psi_{n-1}) - \lambda|\psi_n|^2\psi_n \]
where \(J > 0\) is inter-site coupling and \(\lambda > 0\) is the on-site binding energy. The Inverse Participation Ratio \(\text{IPR}(t) = \sum_n|\psi_n|^4 / (\sum_n|\psi_n|^2)^2\) measures localisation: IPR → 0 (delocalised) vs IPR → 1 (self-trapped).
Renamed and corrected 2026-09-19 (was "Helical Selectivity Principle"). The Reeb vector field \(R=\partial_z\) is a genuine fact about \(\alpha_\text{cat}\) (§2.1), but its flow is volume-preserving and so cannot confine or attract anything; the actual confinement below comes from DNLS self-trapping, and \(r^*(\lambda)\) now carries an explicit length scale so it can be compared to a physical radius at all. See the To-Do entry for what's still open.
Let \((\mathcal{X}_\text{cat}, \alpha_\text{cat})\) be the catalyst contact manifold with Reeb field \(R=\partial_z\), \(a\) a lattice-spacing length scale, and \(G = U \circ F \circ K \circ C\) the generative pipeline. Define the self-trapping tube \(\mathcal{T}_\lambda = \{(r,\theta,z) : r \leq r^*(\lambda)\}\), with \(r^*\) the DNLS self-trapping width in one of two conventions (see Normalization, below): at fixed conserved norm \(P=\sum_n|\psi_n|^2\), \(r^*_P(\lambda) := 4aJ/(\lambda P)\) — adopted here, since the norm is what the DNLS equation conserves and one adsorbed intermediate has \(P=1\); or at fixed peak amplitude \(A=\sqrt2\), \(r^*_A(\lambda) := a\sqrt{J/\lambda}\), the form used in earlier drafts. Both are genuine lengths and both decrease as \(\lambda\) increases. Scope: the fixed-norm law is a quasi-one-dimensional (channel) result, valid for \(r^*\gtrsim 2a\); below \(J/\lambda\approx0.25\) the state is essentially single-site and \(r^*\approx a\) in either convention. In two- and three-dimensional cages there is no continuous \(r^*\) at all: the state either fills the cage or sits on one to two sites, with a threshold in \(\lambda P/J\) (see Prediction 1). So the smooth form of (iii) applies to channels such as ZSM-5's, not to cages such as MCM-22's supercage. Then:
(i) \(\mathcal{T}_\lambda\) is a coordinate region of \(\mathcal{X}_\text{cat}\), not a dynamical attractor: \(R\)'s flow preserves \(\alpha \wedge d\alpha\) and so has no attracting set of smaller volume than its basin, and its orbits are straight lines in \(z\), not helices. \(\mathcal{T}_\lambda\) is simply the set of points with \(r \leq r^*(\lambda)\).
(ii) MODEL A DNLS state whose radial coordinate satisfies the self-trapping condition remains confined to \(r(t) \leq r^*(\lambda)\) under the pipeline's (energy-conserving) dynamics — the discrete self-trapping transition of the DNLS equation itself is the confining mechanism, not the contact manifold's Reeb flow. How this connects to a fixed point of the discrete pipeline \(G\) is not established here; see the To-Do entry.
(iii) The transition-state selectivity is \(\sigma = 1 - (r^*/r_\text{pore})^2\): at fixed norm \(\sigma_P = 1 - 16\,\big(J/(\lambda P)\big)^2 (a/r_\text{pore})^2\), quadratic in \(J/\lambda\); at fixed amplitude \(\sigma_A = 1 - (J/\lambda)(a/r_\text{pore})^2\). Both are dimensionally consistent, unlike the earlier \(\sigma = 1 - J/(\lambda r_\text{pore}^2)\), which required \(J/\lambda\) to carry length² on its own. The two-zeolite test against Sousa et al. depends only on \(r^*\) (same acid chemistry, same \(r^*\)), not on which convention holds; the convention enters only when \(r^*\) is converted back into a lattice spacing \(a\).
The form \(r^*=a\sqrt{J/\lambda}\) is what a continuum sech soliton of fixed peak amplitude \(A\) gives: \(w=a\sqrt{2J/\lambda}/A\). The DNLS is usually studied at fixed conserved norm \(P=\sum|\psi_n|^2\), where the soliton width is \(w\simeq 4Ja/(\lambda P)\) — linear, not square-root, in \(J/\lambda\). SIMULATION scripts/soliton_width_check.py (400-site ring, \(J=1\), \(P=1\), energy minimisation at fixed norm): widths 9.977, 19.988, 40.171 at \(\lambda=0.4,0.2,0.1\) against \(4J/(\lambda P)=10,20,40\); fitted exponent \(d\ln w/d\ln\lambda=-1.005\) over \(\lambda\in[0.1,0.4]\) (a square-root law would give \(-0.5\)); \(-1.006\) against \(P\) at \(\lambda=0.1\). The \(\lambda=0.05\) point is finite-ring affected and excluded. Valid only for \(w\gg a\), i.e. \(J/\lambda\gg1\). The direction of the claim (larger \(\lambda\), smaller \(r^*\), more confinement) is the same either way; the quantitative form of \(r^*\), and so the numbers in \(\sigma\), depend on which normalization the physical problem realises, and that is not decided here.
Update 2026-09-23. DERIVED For the continuum profile \(A\,\mathrm{sech}(x/w)\), matching the \(\mathrm{sech}^3\) terms gives \(2Ja^2=\lambda A^2w^2\), and the discrete norm gives \(P=2A^2w/a\); eliminating \(A\) yields \(w=4Ja/(\lambda P)\). The elimination is machine-checked as algebra (sech_width_fixed_norm), as is the fact that the earlier \(a\sqrt{J/\lambda}\) is the fixed-amplitude width at \(A=\sqrt2\) (criticalRadius_eq_fixedAmplitude); both kernel-checked 2026-09-23 under Lean/Mathlib v4.14.0. Decision: fixed norm is adopted as the primary convention, because the DNLS equation conserves \(P\), not \(A\), and a single adsorbed intermediate has \(P=1\). The fixed-amplitude form is kept, labelled as a convention. SIMULATION 2001-site chain, \(P=1\), normalised gradient flow: widths 3.94, 7.97, 31.99 at \(J/\lambda=1,2,8\) against \(4J/\lambda=4,8,32\); peak amplitude matches \(\sqrt{\lambda/8J}\) to four digits; at \(J/\lambda\le0.25\) the ground state is essentially single-site (IPR 0.72–0.99). Update 2026-09-24: the matching relation \(2Ja^2=\lambda A^2w^2\) is no longer assumed. sech_stationary_forces proves that \(A\,\mathrm{sech}(x/w)\) solves the stationary continuum equation \(-Ja^2\varphi''-\lambda\varphi^3=\omega\varphi\) at every \(x\) only if \(2Ja^2=\lambda A^2w^2\) and \(\omega=-Ja^2/w^2\), and sech_solves_stationary proves the converse. The derivatives are proved, not typed in (sechProfile_hasDerivAt, sechProfile'_hasDerivAt). sech_width_fixed_norm_of_stationary chains these into \(w=4Ja/(\lambda P)\); all kernel-checked under Lean/Mathlib v4.14.0. Still open: (a) the continuum limit itself (discrete Laplacian \(\approx a^2\partial_x^2\), relative error of order \((a/w)^2\), checked only numerically) and the norm relation \(P=2A^2w/a\) (\(\int\mathrm{sech}^2=2\), by hand), which remains a hypothesis; (b) dimensionality — by scaling, \(P\sim(J/\lambda)(w/a)^{d-2}\), so in two dimensions the norm sets a threshold rather than a width, and in three the stationary branch is unstable. The fixed-norm width law therefore applies to quasi-1D channels (the ZSM-5 straight channels), not to 3D cages such as the MCM-22 supercage, where lattice discreteness sets the scale. That was a scaling argument; the 2026-09-24 cage simulation under Prediction 1 confirms it numerically.
What is held fixed, and what it means for an adsorbate. \(r^*_P=4aJ/(\lambda P)\) holds the conserved norm \(P=\sum_n|\psi_n|^2\) fixed (linear in \(J/\lambda\); the peak occupation \(A^2=\lambda P^2/8J\) then rises with \(\lambda\)); \(r^*_A=(a/A)\sqrt{2J/\lambda}\) holds the peak amplitude fixed (square root). The V5 form \(a\sqrt{J/\lambda}\) is \(A=\sqrt2\), i.e. peak occupation \(|\psi|^2=2\) in model units, and the norm it implies, \(P=2A^2w/a=4\sqrt{J/\lambda}\), changes with \(\lambda\), so it is not a fixed-norm statement. In the model \(|\psi_n|^2\) is the occupation of site \(n\) and \(P\) the total amount of localized species: fixed \(P\) is a fixed total coverage of the channel segment (one adsorbed intermediate has \(P=1\)); fixed \(A\) is a fixed peak occupation per site with total coverage free to vary. This paper adopts fixed \(P\) as a modelling choice because the equation conserves it. Which one a real zeolite channel realises, and how \(\psi,\lambda,J,P\) map to measured coverages and energies, is not established here. For the Sousa comparison, \(r^*\) from \(\sigma=1-(r^*/r_\text{pore})^2\) is convention-free, but converting it to \(a\) always carries an unknown dimensionless group (\(\lambda P/J\) or \(\lambda A^2/J\)). Two-site illustration only (the dimer has no length scale): in the two-site DNLS dimer, holding \(P\) fixed makes the dynamics depend on \(\lambda,P\) only through \(\Lambda=\lambda P/J\), while holding the amplitude fixed gives \(\lambda n_1/J\) — different moment-map levels, different control groups; the chain's \(w/a=4/\Lambda\) is the same combination. This illustrates the normalisation choice and nothing more.
On a bimetallic Pt–Sn surface, MODEL the promoter Sn reduces the size of contiguous Pt ensembles. In the model this constrains pathways to those requiring ≤ 2 adjacent Pt atoms, recovering the geometric ensemble effect — and, via Theorem 1(iii)'s \(\sigma=1-(r^*/r_\text{pore})^2\), correctly predicts selectivity increasing with Sn loading (Prediction 2), not decreasing as earlier drafts of that prediction had it.
Removed 2026-09-19: a Corollary 2 on macroscopic extrudate-pellet shape optimization sat here in earlier drafts. Its optimality claim was, and remains, unproved (still [OPEN] in the Lean file — see the To-Do entry), and it doesn't bear on either of this paper's two actual catalytic test cases (zeolite pore selectivity, Pt–Sn ensembles). Cut rather than kept as decoration.
OPEN Reopened 2026-09-20. The formula stated in the 2026-09-19 revision, \(\lambda_c\approx J(\sigma_\text{LJ}/r_\text{pore})^2\), is withdrawn. Two problems. First, that revision contradicted itself: the formula increases as \(r_\text{pore}\) decreases, while the accompanying sentence said smaller pores need less nonlinearity. Second, its supporting argument read \(N\) in the Eilbeck–Lomdahl–Scott parameter \(\chi=\lambda N/J\) as a site count \(N\sim(r_\text{pore}/\sigma_\text{LJ})^2\). In the DNLS literature \(N\) there is the conserved norm \(\sum_j|A_j|^2\), not the number of sites. (Read from the Eilbeck–Johansson review, arXiv:nlin/0211049; the 1985 paper itself has not been re-checked.)
What the deposit does support, for a uniform state on an \(N\)-site ring at fixed norm \(P\), is a modulational-instability threshold that decreases with site count: \(\lambda_\text{MI}=NJ(1-\cos\tfrac{2\pi}{N})\approx 2\pi^2J/N\) — DERIVED from the Bogoliubov dispersion \(\omega_k^2=\epsilon_k(\epsilon_k-2\lambda\rho)\), \(\epsilon_k=2J(1-\cos k)\), \(\rho=P/N\), at \(k=2\pi/N\). SIMULATION scripts/mi_threshold_check.py brackets it: for \(N=8,16,32\) the peak density relative to uniform is 1.00 at \(0.7\lambda_\text{MI}\), and 7.10 / 5.02 / 4.69 at \(1.5\lambda_\text{MI}\), 6.95 / 13.32 / 7.55 at \(3\lambda_\text{MI}\), norm conserved to six digits. A bracket only; it does not locate the threshold more finely than the 0.7× to 1.5× interval. A separate energetic estimate for full localisation, \(\lambda P\gtrsim 4J\) (from \(w\simeq 4Ja/(\lambda P)\lesssim a\)), is independent of \(N\) at large \(N\) and was not simulated.
Update 2026-09-24. SIMULATION scripts/cage_threshold_check.py: ground states of hard-walled DNLS cages at fixed norm \(P=1\), \(J=1\), relaxed from both an extended and a single-site start. In 1D (41 sites) the state narrows continuously as \(\lambda\) grows, with no threshold. In 2D (31×31) a localized branch first exists at \(\lambda P/J\in(5.5,6]\) and becomes the ground state at \(\lambda P/J\in(6.5,7]\). In 3D (9³, 11³, 13³) it first exists at \(\lambda P/J\in(7.8,8.0]\) and becomes the ground state between 10.0 and 12 (\((10.0,10.5]\) for 11³); between the two thresholds both states exist. The localized state is one to two sites (IPR ≥ 0.64), and its IPR and energy are the same for 9³ and 13³, so it does not depend on the cage's site count. There are no intermediate widths in 2D or 3D. This settles two of the three choices listed below, numerically: the relevant \(N\) is the norm, and the 2D cross-section is treated. What remains is mapping \(\lambda\), \(J\) and \(P\) to measurable quantities, and temperature: these are ground states, and thermal activation between the two branches could narrow the bistable window. The qualitative prediction that follows: an abrupt, possibly hysteretic change in intermediate populations in MCM-22's supercages and 2D channels, and a smooth change in ZSM-5's 1D channels, as a control parameter such as loading crosses threshold. The thresholds above are bare-lattice numbers and are not converted to experimental units.
These are thresholds for two different notions of "self-trapped" on a 1D ring; neither has been mapped to a zeolite pore. That mapping needs an operational definition of \(\lambda_c\), a decision whether the relevant \(N\) is a site count or a norm, and a treatment of a two-dimensional pore cross-section (the literature reports a finite threshold in 2D that 1D does not have). A falsifiable version of this prediction needs those three choices first, then a molecular-dynamics comparison. The sign of the dependence of \(\lambda_c\) on pore size is not asserted.
Corrected 2026-09-19 — see the To-Do entry. The fraction of surviving size-2 Pt-only ensembles on \(\text{Pt}_{1-x}\text{Sn}_x\) — the geometric quantity driving the undesired hydrogenolysis/coking pathway — is proposed to scale as \((1-x)^2\) (pending resolution against the alternative form \(1-x^2\); see ensemble_scaling_forms_diverge below), matching the DNLS confinement fraction: \((1-x)^2 \approx (r^*/r_\text{pore})^2\). Propane dehydrogenation selectivity toward propylene is the complement of this survival fraction, \(\sigma = 1-(r^*/r_\text{pore})^2 \approx 1-(1-x)^2\) — increasing from 0 at \(x=0\) toward 1 as \(x\to1\), matching the empirically established effect of Sn addition raising propylene selectivity by breaking up large Pt ensembles. Earlier drafts equated \((1-x)^2\) directly with selectivity — backwards, since \((1-x)^2\) is a decreasing quantity (ensemble survival) while selectivity is its increasing complement. Testable via in-situ XAS measurements of average Pt ensemble size correlated against measured propylene selectivity.
Removed 2026-09-19: a Prediction 3 claiming a "helical phase" θ(t)=ωt+θ₀ in the reaction coordinate sat here in earlier drafts. It depended entirely on the Reeb orbits being helical, which they aren't — the orbits hold θ fixed (Theorem 1(i)); there is no advancing angular phase for a measurement to detect. Cut rather than restated around a different, unestablished mechanism.
The file CatGT_Main.lean (deposited in TOTOGT/io; the filename predates the retitling and is kept so the repository and CI still resolve) provides sorry-free Lean 4 proofs of a square-root-monotonicity inequality, the selectivity identity that Theorem 1 uses in both normalizations, the algebraic amplitude-to-norm elimination behind \(r^*_P=4aJ/(\lambda P)\), a proof that the sech profile solves the stationary continuum DNLS equation exactly when \(2Ja^2=\lambda A^2w^2\), the fixed-norm confinement tube and the stationary-sech width at general amplitude (which equals \(r^*\) at \(A=\sqrt2\)), a computational DNLS scaffold, a scalar Lyapunov-decay map, and one honest open obligation. 28 theorems, 0 admits, 0 sorries.
Verification status of the file quoted below. Author's runs of the current file on 2026-10-06: 28/28 #print axioms report only [propext, Classical.choice, Quot.sound] under Lean/Mathlib v4.14.0 (the CI pin, compiled with lake env lean through the AXLE checkout, which has the same pins), and under Lean/Mathlib v4.32.0 (lake build CatGT on the byte-identical mirror in TOTOGT/geometry); no errors, warnings only for unused hypotheses and one unreachable ring. The geometry CI gate now expects all 28; at 23 it passed (run #546), and its result at 28 is not quoted here. This repository's own CI prints the same 28 axiom lines on every push; its result for the current commit is on the repository's Actions tab and is not quoted here. Earlier history: 23/23 on both pins on 2026-09-24 (before §4d; that 23-theorem file is the one deposited as V6, 10.5281/zenodo.22929142, and §4d is a later addition that is not in the V6 deposit); the 13-theorem version was run under v4.32.0 (13/13, sha256 prefix 19e8df03ad44) and 18/18 under v4.14.0 on 2026-09-23. A hand run establishes the file on the day it is run.
Revision note (2026-07-10): two theorems on this page previously proved vacuous statements — catgt_dm3_transport proved ∃ shape, True (true for any shape) and ensemble_scaling proved ∃ selectivity, selectivity = (1-x)² (true by construction for any x) — and both reported "closed"/"admit" badges that overstated what was actually established. Both have been corrected below to prove real, checkable facts instead, and the deeper open claims each was gesturing at (Corollary 2 optimality; which Pt–Sn scaling law is correct) are now stated as open prose rather than dressed up as theorems.
Note: Lean 4 reserves the bare λ character for anonymous-function syntax, so it cannot be used as a parameter/identifier name — the source uses lam/hlam where this page's prose uses \(\lambda\). The snippets below show the actual compiling identifiers.
Note (2026-09-20): the length scale \(a\) has now been carried into the Lean file: criticalRadius (a J lam) := a * Real.sqrt (J / lam), and criticalRadius_pos, criticalRadius_antitone, helical_selectivity, selectivityFactor and selectivityFactor_eq were restated and re-proved against it (this closes the 2026-09-19 gap that the quoted code did not match Theorem 1). reeb_orbit_advances (§6 of the file) proves the z-advance of the orbit equals \(t\,\alpha(R)\), from the actual 1-form pairing. The snippets below are extracted from the file itself. The theorem name helical_selectivity is retained from the earlier draft that called the confining set a "helical attractor"; the paper no longer claims that, and a rename (which touches the Lean file, CI axiom list, README and this page) has not been done — do not read the name as asserting helical structure. Also note what it proves: its hypothesis \(r^2\le a^2J/\lambda\) is the squared form of its conclusion, so it is monotonicity of the square root and carries no DNLS dynamics.
/-- Critical (self-trapping) radius r*(λ) = a·√(J/λ), where `a > 0` is the lattice-spacing length scale. J and λ are both energies, so J/λ is dimensionless and `a` is what gives r* the dimension of a length (Theorem 1's 2026-09-19 correction on the paper's page). NOTE: this is the *definition* the theorems below are stated against; that r* is the physically correct DNLS self-trapping width is a separate claim, and depends on what is held fixed (see the 2026-09-20 note in the header). CONVENTION (2026-09-23): this is the FIXED-AMPLITUDE branch, A = √2 (criticalRadius_eq_fixedAmplitude, §4b); the fixed-norm branch is criticalRadiusNorm. -/ noncomputable def criticalRadius (a J lam : ℝ) (ha : 0 < a) (hJ : 0 < J) (hlam : 0 < lam) : ℝ := a * Real.sqrt (J / lam) /-- **Self-Trapping Selectivity Principle** — formal core of Theorem 1. r² ≤ a²·(J/λ) ⟹ r ≤ r*(λ) = a·√(J/λ). NOTE (what this does and does not say): the hypothesis is the squared form of the conclusion, so this is the equivalence "r ≤ r* ⟸ r² ≤ r*²" for r ≥ 0, i.e. sqrt-monotonicity. It does NOT derive confinement from any DNLS dynamics; that is Theorem 1(ii)'s open content. -/ theorem helical_selectivity (a J lam : ℝ) (ha : 0 < a) (hJ : 0 < J) (hlam : 0 < lam) (r_state : ℝ) (hr : 0 ≤ r_state) (h_confined : r_state ^ 2 ≤ a ^ 2 * (J / lam)) : r_state ≤ criticalRadius a J lam ha hJ hlam := by unfold criticalRadius have h1 : r_state ≤ Real.sqrt (a ^ 2 * (J / lam)) := by rw [← Real.sqrt_sq hr]; exact Real.sqrt_le_sqrt h_confined have h2 : Real.sqrt (a ^ 2 * (J / lam)) = a * Real.sqrt (J / lam) := by rw [Real.sqrt_mul (sq_nonneg a), Real.sqrt_sq ha.le] rw [h2] at h1 exact h1
/-- Selectivity factor σ = 1 - (r*/r_pore)² = 1 - (J/λ)(a/r_pore)². -/
noncomputable def selectivityFactor (a J lam r_pore : ℝ)
(ha : 0 < a) (hJ : 0 < J) (hlam : 0 < lam) (hr : 0 < r_pore) : ℝ :=
1 - (criticalRadius a J lam ha hJ hlam / r_pore) ^ 2
theorem selectivityFactor_eq (a J lam r_pore : ℝ)
(ha : 0 < a) (hJ : 0 < J) (hlam : 0 < lam) (hr : 0 < r_pore) :
selectivityFactor a J lam r_pore ha hJ hlam hr
= 1 - (J / lam) * (a / r_pore) ^ 2 := by
unfold selectivityFactor criticalRadius
have hs : Real.sqrt (J / lam) ^ 2 = J / lam :=
Real.sq_sqrt (div_nonneg hJ.le hlam.le)
have hkey : (a * Real.sqrt (J / lam) / r_pore) ^ 2
= (J / lam) * (a / r_pore) ^ 2 := by
calc (a * Real.sqrt (J / lam) / r_pore) ^ 2
= Real.sqrt (J / lam) ^ 2 * (a / r_pore) ^ 2 := by ring
_ = (J / lam) * (a / r_pore) ^ 2 := by rw [hs]
rw [hkey]
/-- **Fixed-norm width.** From the sech matching condition and the norm relation, eliminating the amplitude A gives w = 4Ja/(λP). Algebra only: the two hypotheses are the continuum ansatz. -/ theorem sech_width_fixed_norm (a J lam A w P : ℝ) (ha : 0 < a) (hlam : 0 < lam) (hP : 0 < P) (h_match : 2 * J * a ^ 2 = lam * A ^ 2 * w ^ 2) (h_norm : P * a = 2 * A ^ 2 * w) : w = 4 * J * a / (lam * P) := by rw [eq_div_iff (mul_pos hlam hP).ne'] have h1 : (w * (lam * P) - 4 * J * a) * a = 0 := by linear_combination (w * lam) * h_norm - 2 * h_match rcases mul_eq_zero.1 h1 with h | h · linarith · exact absurd h ha.ne' /-- Fixed-norm self-trapping radius r*_P = 4aJ/(λP). -/ noncomputable def criticalRadiusNorm (a J lam P : ℝ) : ℝ := 4 * a * J / (lam * P) /-- Fixed-norm selectivity: σ_P = 1 - (r*_P/r_pore)² = 1 - 16·(J/(λP))²·(a/r_pore)² — quadratic in J/λ, where the fixed-amplitude σ is linear. -/ noncomputable def selectivityFactorNorm (a J lam P r_pore : ℝ) : ℝ := 1 - (criticalRadiusNorm a J lam P / r_pore) ^ 2 theorem selectivityFactorNorm_eq (a J lam P r_pore : ℝ) : selectivityFactorNorm a J lam P r_pore = 1 - 16 * (J / (lam * P)) ^ 2 * (a / r_pore) ^ 2 := by unfold selectivityFactorNorm criticalRadiusNorm ring
Removed 2026-09-19: this section previously quoted catgt_dm3_transport (later corrected to catgt_dm3_disk), the Lean support for the extrudate-shape Corollary 2. That corollary is cut from this narrower paper (see §3); the theorem itself still exists, verified, in CatGT_Main.lean, and remains listed in the Sorry Audit below as an accurate inventory of that file — it just no longer has a matching claim in this paper's prose to illustrate.
/-- The two proposed Pt–Sn scaling forms are NOT the same function:
(1-x)² and 1-x² agree only at x∈{0,1}; at x=1/2, 1/4 ≠ 3/4.
Which form is physical is OPEN (awaits XAS, Part III). -/
theorem ensemble_scaling_forms_diverge :
(1 - (1/2 : ℝ)) ^ 2 ≠ 1 - (1/2 : ℝ) ^ 2 := by norm_num
Correction (2026-06-18): earlier versions of the zeolite operator-order paper (v1, Zenodo 10.5281/zenodo.20563363, and v2, Zenodo 10.5281/zenodo.21296707) asserted that the aperture gate K fails to commute with a pointwise fold Fψ = ψ + λ|ψ|²ψ, via a boundary term ∝ δ(r − rap). That claim is false — the two commute exactly, for every state — and the three theorems below establish what is actually true. Order-dependence is carried by whichever operator transports amplitude between sites, never by a gate acting pointwise.
-- 3-site ring, real amplitudes (so |v|²v = v³). def coupling (v : Fin 3 → ℝ) : Fin 3 → ℝ := ![v 1 + v 2, v 0 + v 2, v 0 + v 1] def onsite (v : Fin 3 → ℝ) : Fin 3 → ℝ := fun i => (v i) ^ 3 def gate (v : Fin 3 → ℝ) : Fin 3 → ℝ := ![v 0, 0, v 2] def psi : Fin 3 → ℝ := ![1, 1, 0] /-- The 0/1 aperture gate commutes with the pointwise fold — for EVERY state. -/ theorem gate_commutes (v : Fin 3 → ℝ) : gate (onsite v) = onsite (gate v) /-- Inter-site coupling does NOT commute with the on-site fold (commutator −6). -/ theorem coupling_not_commute : coupling (onsite psi) ≠ onsite (coupling psi) /-- The gate does NOT commute with the corrected fold F = coupling ∘ onsite. -/ theorem gate_fold_not_commute : gate (coupling (onsite psi)) ≠ coupling (onsite (gate psi))
These three are kernel-checked on Lean v4.33.0-rc1 + Mathlib with #print axioms reporting only [propext, Classical.choice, Quot.sound] — no sorryAx. Unlike CatGT_Main.lean and Theorem53NonCommutativity.lean, this file is not wired into lakefile.toml and so is not re-run by CI; it is standalone and self-contained, and can be re-verified by pasting it into any Lean 4 + Mathlib environment such as live.lean-lang.org.
v3 published (July 2026): the corrected paper — "Operator Firing Order as the Missing Mechanism in Ethanol-to-Hydrocarbon Selectivity: Contact-Geometric Analysis of ZSM-5 and MCM-22 Zeolites" (Grossi, Zenodo 10.5281/zenodo.21429016, supersedes v1–v2 at zenodo.org/records/20563363) — restates the operator-order hypothesis around the corrected commutation results above and states seven theorems with explicit [VERIFIED]/[MODEL]/[SIMULATION]/[OPEN] tags per claim (its §4.4); nothing tagged short of [VERIFIED] may be cited as proved. (This paragraph is retained as v3's historical record; see v4 below.)
v4 published (September 2026): Zenodo 10.5281/zenodo.22849726 (supersedes v3 above). v4 narrows Theorem 4 to the aperture-specific scope its proof actually supports, replaces Theorem 5's unproved (and arithmetically backwards — it moved a barrier feature in the wrong direction) rescaling assertion with a derived one, and adds two evidentiary caveats distinguishing the paper's restated literature review from its actual novel content. A new status tag, [DERIVED] (a complete proof given in the text, not yet in Lean), was introduced for Theorem 5(ii)–(iii); Theorem 5(i) itself — the contactomorphism claim — is kernel-checked in ContactMorphism.lean (see the audit block below) and tagged [VERIFIED].
Reference correction (June 2026): independently of the commutation fix, 6 of the paper's original 10 references carried fabricated titles, page numbers, or author lists despite correct-looking DOIs (e.g. a citation to Sastre, Catlow & Corma attached to the wrong paper under its own DOI; an author list for ref. [1] naming people who did not write it). All references were re-checked against CrossRef and corrected in v3; one unverifiable entry (Zhou et al.) was dropped rather than left uncorrected. The full before/after list and per-reference diagnosis are in zeolite_paper_reference_corrections.md in the repository. (This section of the page last updated 2026-09-19.)
This does not contradict DFT-based active-site design — it addresses a different question. DFT explains why a given site is reactive; it is silent on why identical acid sites in different pore geometries give different products. The Brønsted–Evans–Polanyi relation corresponds to the linearisation of \(K\) near \(x^*\) (that connection remains stated informally; \(x^*\) is not formally defined here — see the To-Do entry). The Thiele modulus is the ratio \(r_\text{pore}/r^*(\lambda)\).
The firing order of the compression/constraint/fold/unfold operators is not fixed but system-dependent. In ZSM-5, constraint fires before folding (the pore constrains first). In MCM-22, folding fires before constraint (the intermediate folds inside the supercage first). This operator-order switching under varied temperature, pressure, or concentration is a falsifiable DRIFTS prediction, independent of the self-trapping radius claim above.
1. Quantitative fit against Sousa et al.'s measured selectivity, blocked on access to the data tables — see the To-Do entry. 2. Normalization of \(r^*(\lambda)\): fixed norm adopted (§3); the sech relation is derived from the continuum equation, but the continuum limit and the norm relation are not; in 2D and 3D cages \(r^*\) is a threshold, not a width (simulated; not mapped to experimental units). 3. Prediction 1: an operational definition of \(\lambda_c\), the role of \(N\), and 2D pore cross-sections (§4). 4. Finite-size scaling of \(r^*(\lambda)\) for chain lengths \(N \in \{100, 500, 1000\}\). 5. Definition of \(C,K,F,U\) and \(x^*\) on \(L^2(\mathcal{X}_\text{cat})\).
Open items tracked against this page, in the same spirit as the Sorry Audit above: nothing here is fixed by asserting it fixed. Checked off only once a corrected theorem, formula, or citation actually replaces the flagged one.
latticeA) and its caption. Figure 4/the Coherence Bridge is addressed separately below rather than by propagating a into it, since the deeper issue there is what the bridge claims, not just its units.criticalRadius now takes the length scale \(a\) (a * Real.sqrt (J / lam)), and helical_selectivity and selectivityFactor_eq were re-proved against it. Kernel-checked by the author on Lean 4.32.0 / Mathlib v4.32.0 (13/13 axioms clean). Still open on this item: (a) the run was repeated on the final file after the comment-only edits (clean); (b) the repository CI pins v4.14.0 and has not been run on this version; (c) the theorem name helical_selectivity is stale — renaming (proposed selfTrapping_selectivity) means changing the Lean file, the CI #print axioms list, README and this page, and is pending; (d) the file's header comment still cites Zenodo 10.5281/zenodo.19117399, not this paper's 10.5281/zenodo.22851704 — comment-only, not changed so all copies of the file stay identical.scripts/mi_threshold_check.py). Still needed before Prediction 1 can be falsifiable: an operational definition of \(\lambda_c\), whether the relevant \(N\) is sites or norm, and the 2D pore cross-section. Note also that the 2026-09-19 Corollary 1 wording ("raising \(\lambda_c\) and shrinking \(r^*\)") depended on that relation and was removed in V5.1.sech_width_fixed_norm); single-site floor at \(J/\lambda\lesssim0.25\) found numerically. Still open: derivation from the lattice equation, and the 2D/3D case (scaling says the fixed-norm width law is quasi-1D only). Update 2026-09-24: sech relation derived from the continuum equation (sech_stationary_forces, 23/23 on v4.14.0); 2D/3D cage thresholds simulated (scripts/cage_threshold_check.py), see Prediction 1. Still open: continuum limit, norm relation, mapping to experimental units, temperature.[OPEN] with no data behind it, and it doesn't bear on either test case this paper actually makes. Its supporting Lean theorem (catgt_dm3_disk) still exists, verified, in CatGT_Main.lean — cutting it from this paper's prose doesn't touch the Lean file itself.ensemble_scaling_forms_diverge should be resolved, not left open.ensemble_scaling_forms_diverge comment, and the Sorry Audit's "still open" line all updated to keep these two quantities distinct. The genuinely open question — whether \((1-x)^2\) or \(1-x^2\) is the correct survival form — is unaffected and remains open, now correctly scoped as a question about survival probability, not about selectivity.10.5281/zenodo.19117399 is used both as this paper's own identifier (masthead, footer) and as the citation for "GTCT — Part I" (reference 7) — confirm this is an intentional self-reference and not a copy-paste duplicate.10.5281/zenodo.22851704, updated in the masthead and footer. 10.5281/zenodo.19117399 remains correctly attached only to reference [7] ("GTCT — Part I of the GOMC Opus"), a separate work this paper no longer claims to be part of — not a duplicate, just no longer shared. (V5.1, 2026-09-20: reference [7] has since been removed from the reference list; this paper no longer cites it.)CatGT_Main.lean (catgt_dm3_transport, ensemble_scaling) predates the June-date correction applied elsewhere on this page — confirm whether it should also move, or whether it's a genuinely separate, later event.Convex.Basic plus a 2D isoperimetric lemma; targeted for Part II.catgt_dm3_disk) still exists, verified, in CatGT_Main.lean — this item would only matter again if a future, separate paper picked the extrudate-shape claim back up.ContactMorphism.lean); Theorem 5(ii)–(iii) (the WKB momentum correspondence and L² norm preservation) remain [DERIVED], and Theorem 7's selectivity–order bijection remains [OPEN] — cross-referenced here rather than duplicated.CatGT_Main.lean's own header still described itself as "Part I of the GOMC Opus," named its central theorem "Helical Selectivity Principle (HSP)," and stated a "Relation to GTCT."