Rigorous computation of Boroński-Štimac kneading invariants and N-gram admissibility for the Hénon map

We present the first rigorous computation of the kneading invariants defined by Boroński and Štimac(2024) for the classical Hénon mapH(x,y) = (1−1.4x2 +y, 0.3x). UsingLohner’s algorithm (CAPD), we prove 42 kneading symbols for the primary critical point and at least 23 symbols for each of the 4 kneading families, constituting the first rigorous kneading computation via the critical locus for any Hénon parameter. We rigorously verify 3 forbidden 4-grams (––, –+-, -++-) across 1,421 critical crossings with 100% proof rate, independently confirming results of Galias and Zgliczyński obtained via a different framework. Amulti-point Krawczyk method with condition number O(p) (proven algebraically by SymPy) achieves 100% rigorous verification of all admissible N-grams for N = 6 through 20, producing 21,208 verified words at N = 20 — far beyond any prior work. We establish a bridge between the B-Š kneading framework and Galias–Zgliczyński symbolic dynamics, achieving 95% coverage at N = 16. The folding pattern — a new invariant not previously computed — has zero topological entropy with subword complexity p(n) ≈30n and fundamental forbidden word 000.