The census counts periodic points and proves completeness; those counts encode the growth rate that IS topological entropy. This page turns boxes into the invariant: a certified lower bound h ≥ 0.3017 for the Hénon map at the classical parameters — every covering relation a strict interval inequality, the spectral bound exact, the whole certificate re-proved while this page was built — and the certified cycle counts that name the ceiling it is climbing toward.
Local working document. The bound is a theorem modulo one consumed external result (covering relations imply semi-conjugacy to the subshift — Zgliczyński–Gidea), used the way Krawczyk's theorem is consumed elsewhere in this lab. Parameters are the exact doubles nearest 1.4 and 0.3, the same objects the census certifies.
An entropy bound is only interesting next to the thing it is climbing toward. The green bar is the theorem; the hatched band is the room the certified cycle counts leave for it; ln 2 is the horseshoe the instrument reproduces before any new bound is allowed to count.
There are 340 parallelograms (h-sets) in the plane, proved pairwise disjoint by separating axes with outward rounding. For 4140 ordered pairs and durations k = 1..6, the iterate F^k provably STRETCHES the first parallelogram across the second: the two exit edges land strictly beyond the target on opposite sides, and the image avoids the target's side SLABS — finitely many strict interval inequalities, checked by adaptive bisection. Relations COMPOSE, so all durations reduce to one uniform iterate: B_K[i][j] = 1 iff some duration-exactly-K composition exists (binary — one relation per pair, never a path count), and
with the spectral bound exact (min positive row sum of powers, integer arithmetic, overflow-guarded, iteratively trimmed). The certifier can refuse an edge — and did, for most candidates; it cannot certify a false one. Dropping edges only ever lowers the bound, which is the safe direction. TWO soundness bugs were found by impossible numbers, and each now has a red control: counting mixed-duration paths as distinct itineraries once yielded h ≥ 0.61 on a map whose true entropy is ≈ 0.465 (a duration-2 relation constrains nothing at its intermediate time), and a lids-only image condition once certified a golden-mean graph converging to ln φ = 0.4812 — also past the truth. The battery now demands the exact-ln 2 horseshoe stays at ln 2 under mixed durations, and the slab condition replaced the lid condition.
The float layer that PROPOSED the boxes — a long orbit, binned; tangents by local PCA; stable directions by backward-Jacobian iteration — is believed about nothing: every box and every edge is re-derived from the interval conditions alone, and the battery re-proves the whole certificate (4140/4140 edges) on every build.
| period | points, certified exact | ln(N_p)/p | status |
|---|---|---|---|
| p = 13 | 418 | 0.4643 | completeness: EXACTLY this many, plane exhausted |
| p = 14 | 648 | 0.4624 | completeness: EXACTLY this many, plane exhausted |
| p = 15 | 1082 | 0.4658 | completeness: EXACTLY this many, plane exhausted |
| p = 16 | 1696 | 0.4648 | completeness: EXACTLY this many, plane exhausted |
The growth rate of certified cycle counts climbs to 0.4658 by p = 16 — squarely at the literature value h ≈ 0.4651 for these parameters. But counts alone are NOT a lower bound for entropy (that implication runs the other way); the covering graph is what converts counted orbits into certified entropy, and today it certifies 0.3017 — 65% of the ceiling. The gap is structure the current graph does not resolve: uniform box sizes and a single global iterate. Per-edge durations with Bowen-weighted spectral bounds, and boxes sized to local expansion, are the recorded next step.
make test re-proves everything: the ln 2 calibration at the full horseshoe, four red controls (a covering that does not hold must refuse three different ways; overlapping h-sets must refuse the graph), exactness of the spectral bound on hand matrices, and the detached certificate certs/entropy-henon.json — every h-set re-proved disjoint, every covering relation re-derived, the bound recomputed. The certificate itself is finite data: parallelogram matrices, an edge list, one integer matrix power.