Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Han, Ji and Xiong’s Sec Grammar Conjecture

Abstract

The number of distinct terms in every positive iterate of the Sec q-derivative is the formula of Conjecture III.7.

Theorem 1.1 (Conjecture III.7 resolved).

Lean statement: D5/S3/Combinatorics/QGrammar/SecGrammar.result

Proof. Machine-checked in Lean as D5/S3/Combinatorics/QGrammar/SecGrammar.result (✓ std3). ∎

Resolves. Problems/han-ji-xiong-sec-grammar-support (proved) by D5/S3/Combinatorics/QGrammar/SecGrammar.result.

Source. Repository-derived.

Acknowledgement. Guo-Niu Han, Kathy Q. Ji, Huan Xiong (2026). q-Derivative Grammar. DOI: 10.48550/arXiv.2604.23959. URL: https://arxiv.org/abs/2604.23959v2.

Commentary.

For every positive natural n, the support of the n-fold q-derivative of y at index zero has cardinality omegaFormula n. This proves Conjecture III.7 for the Sec grammar.

References