Factorized ladders for generalized quantum Zernike Hamiltonians

Campoamor-Stursberg, Herranz, Latini, Marquette and Blasco, Nonlinearity 39, 055008, arXiv:2502.02491v2, Conjecture 1(iii), asks for number and ladder operators constructed from the quantum symmetries (2.8), satisfying (2.9)–(2.10) with the factorization (5.1) for every $N\geq1$. Preregistration: #19957.

The binding polynomial formulation is proved by D5.S3.Quantum.CampoamorStursbergZernikeLadder.result. Operators are complex linear endomorphisms of $\mathbb C[q_1,q_2]$. For every $N\geq1$ and every complex coefficient sequence there are two symmetries with the kinetic terms and correction span of (2.6), and number and ladder operators in the unital algebra generated by $K_1,K_2,K_3$, satisfying all four identities of the claim.

Statement echo

| Source clause | Lean counterpart | Scope | | --- | --- | --- | | Coordinate multiplication and $-i$ times partial differentiation, (2.1) | Core q, p | Fin 2 indices 0 and 1 encode source coordinates 1 and 2. | | Hamiltonian and angular momentum, (2.3), (2.5) | Core dot, hamiltonian, angularMomentum | Composition of polynomial endomorphisms; arbitrary complex coefficients. | | Normal-ordered correction monomials of positive degree at most $2N$ and grading zero, (2.6) | Core monomial, corrections | The defining span uses exactly these conditions. | | Two commuting symmetries with prescribed kinetic terms, (2.6)–(2.7) | Core IsSymmetry; both first conjuncts of claim | Momentum-order upper bound; no exact-order assertion at degenerate coefficients. | | $K_1=C$, $K_2=(I'-I)/2$, $K_3=[K_1,K_2]$, (2.8) | Core k1, k2, k3 | Literal binding definitions. | | Operators constructed from these three generators | Three Algebra.adjoin memberships in claim | The unital generated algebra; no extra hypotheses. | | Raising and lowering commutators, (2.9) | First two final conjuncts of claim | Equalities of endomorphisms. | | $K_+K_-=\Phi(H,K)$ and the shifted commutator, (2.9)–(2.10) | Last two conjuncts of claim | Core phi1, phi2, phi give exactly (5.1). | | Every order and every coefficient choice | Universal binders of claim | $N\geq1$; only indices 1 through $N$ are used. |

The divided-difference definitions are auxiliary polynomial expressions. The claim has no localization, invertibility, nondegeneracy or analytic-domain hypothesis. No clause of the binding claim is dropped.

The source computes low orders and conjectures the arbitrary-order quantum ladder factorization. Its factorization is the algebraic input to the later representation and spectrum questions. The result supplies this algebraic identity uniformly, with the stated correction bound, without claiming that it determines a physical Hilbert-space realization.

The source note is campoamor2026zernike. The settling declaration is frozen through deposit-uncovered, with no atom. Its supporting module is D5/S3/Quantum/CampoamorStursbergZernikeLadderCore.

The binding polynomial statement is proved. Conjecture 1(ii), algebraic independence, and Conjecture 2, physical spectrum and representation theory, remain open in this delivery. Exact differential order for degenerate coefficient choices and analytic operator domains are not established.

Write $D=q\cdot p$, $C=q_1p_2-q_2p_1$, $x=p_1+ip_2$, $y=p_1-ip_2$, $q_+=q_1+iq_2$, $q_-=q_1-iq_2$, and $F(t)=\sum_{k=1}^N\gamma_k t^k$. The polynomial divided difference is

$$Q_F(s,t)=\sum_{k=1}^N\gamma_k\sum_{j=0}^{k-1}s^{k-1-j}t^j.$$

For commuting $s,t$, telescoping the geometric sum gives $F(s)-F(t)=(s-t)Q_F(s,t)$. This identity is an explanation of the mechanism, not a separately exported theorem. Core ProductIdentity.factorization supplies the abstract ordered-product identities; HamiltonianIdentity.symmetry supplies the corresponding commutation identity.

The explicit ladders are

$$K_+=\tfrac12\bigl(x^2+xq_+Q_F(D,i(C+2))\bigr),\qquad K_-=\tfrac12\bigl(y^2+yq_-Q_F(D,i(2-C))\bigr),\qquad K=C/2.$$

Weyl shift relations establish both ordered products directly in the endomorphism ring. Set $I=H/2-(K_++K_-)/2$ and $I'=H/2+(K_++K_-)/2$. Normal ordering puts their corrections in the defining span. The identities $K_2=(K_++K_-)/2$ and $K_3=K_+-K_-$ reconstruct the ladders in the required generated algebra. These statements describe the construction used by result; no localization or faithful-localization bridge is used.

A failure of any conjunct of the literal claim for an allowed $N$, coefficient sequence and polynomial wavefunction would refute the binding statement. Lean checks the universal theorem in the pinned formal system. Symbolic examples alone do not establish the universal statement or claims about analytic domains.

Kernel evidence: D5/S3/Quantum/CampoamorStursbergZernikeLadder.lean, theorem result, and its imported Core module. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}. Both modules have Blueprint Scribe mirrors; the settling Describe carries the single Proved resolution claim.

Escape audit is unfinished for the fourteen public theorems listed in #21497. No Reg registration is claimed declared_validated. Missing evidence is the faithful dependent-family reconstruction and bridge, variation, sensitivity and actual observational dependence; the mathematical proofs do not supply these separate registration obligations.

Symbolic experiment

Experiment directory at commit 9f3dcb3baf7b3b158f03f978e2374438ab86873f. Script: check.py; SHA-256 e158a68aaeff7c4699928ed1e85a19c857f179f8c392ff381c44f88e1d36d72e. The immutable script was verified with git cat-file -e and extracted without modification. Command: python3 /Users/auric/.sshx/f08067f216c414018449521f/attempt-1/source-check.py; exit 0.

Computed in exact symbolic arithmetic with symbolic coefficients: for $N=1,2,3$, both symmetry commutators, both ladder commutators and both ordered-product identities on fourteen test monomials. The script also reconstructs the form (2.6) at those three orders and reproduces source (3.1), (3.2), (3.4)–(3.5) at $N=2$. These finite checks are distinct from the universal kernel theorem.

What the settlement shows

| Item | Status and evidence | Boundary | | --- | --- | --- | | Divided differences convert shifted polynomial differences into products | Proved in prose by telescoping: expand $(s-t)Σ_{j<k}s^{k-1-j}t^j$ for commuting $s,t$; consecutive terms cancel, leaving $s^k-t^k$, and then sum with coefficients $γ_k$. | The algebraic step uses the stated commuting relations. | | Weyl shifts yield both ordered ladder factorizations directly in the operator ring | Kernel-checked by settling result, with its private Ladders.raising_lowering_phi and Ladders.lowering_raising_phi proofs. | The carrier is polynomial endomorphisms. | | Normal ordering preserves grading and increases the total-degree bound by at most two per first-order factor | Kernel-checked by Core Corrections.dot_pow_mul_mem, Corrections.C_pow_mul_mem and their private first-order multiplication proof. | Positive degree and the changing bound $2(N+r)$ are retained. | | Construction for every $N\geq1$ and all complex coefficients | Kernel-checked by settling result. | No nonzero-coefficient assumption, localization or faithful-localization bridge. | | Form (2.6) total-degree and grading bound | Kernel-checked correction-span membership in result. | Every monomial has positive total degree at most $2N$ and grading zero. | | Form (2.6) momentum-order upper bound | Proved in prose: $a+b=c+d$ and $a+b+c+d\leq2N$ imply $2(c+d)\leq2N$, hence each correction monomial has momentum order $c+d\leq N$. Adding the quadratic kinetic term gives order at most $\max(2,N)$ for the full symmetry. | Exact order at degenerate coefficients is open. | | Conjecture 1(ii), algebraic independence | Open. | Not a conjunct of the binding claim and not proved by the operator identities. | | Conjecture 2, physical spectrum and representation theory | Open. | A representation, analytic domains and spectral completeness need additional arguments. | | Finite symbolic identities, correction form and source $N=2$ comparison | Computed by the experiment in Evidence, exit 0, with the stated script hash. | Exactly $N=1,2,3$ on fourteen test monomials, plus the source $N=2$ comparison. | | Algebraic prerequisite of the source's spectrum discussion | Kernel-checked by result: the factorized ladder identities hold uniformly. | This supplies the algebraic identity used by that discussion. | | Physical consequences for the source's other results | Open. | Algebraic independence, Hilbert-space realization and physical spectral completeness require additional arguments. |

The literature screen recorded in #19957 covers the source, the same-author review arXiv:2511.09541v1 and the later separation-of-variables work arXiv:2605.23748v2. No arbitrary-order quantum settlement was found in that inspected scope. Completeness is ASSUMED-UNVERIFIED.

Literature completeness is ASSUMED-UNVERIFIED. Source and literature checks attributed to the preregistration's orchestrator are source readings, not kernel evidence. The theorem establishes the binding polynomial-wavefunction formulation; analytic Hilbert-space and physical spectrum claims remain open. The four-slot escape audits are unfinished under #21497.