Finite concave spectral counting inequalities and an exact counting distinction are established, including eight Lean files with AXLE receipts under standard axioms, but second and third moments alone cannot force a gain, and no stronger zeta proportion is asserted.
hunts/cycle_moments (Record 89 of 98 in chronological sequence)
Guiding Question
Can joint cycle moments strengthen simple-real counting beyond its quadratic bound?
Method & Verification
Eight standalone Lean 4.33.0 files were checked via AXLE with printed axioms restricted to propext, Classical.choice, and Quot.sound, beside exact finite examples, 160-bit interval sign checks, and Haar-unitary probes that do not establish a population gain.
Lineage & Relationships
None
Primary Sources (at pin 8fa46e134)
Editorial Notes
No explicit Status field in the root case-log entry; disposition is completed from RESULTS.md bounded outcome. Evidence grade is measured under ALIGNMENT weakest-step discipline: while eight individual Lean declarations have AXLE kernel-check receipts, the moment scans, mixed inequalities, and absence of an asymptotic zeta proportion gain are measured and unproved, so the composite row grade is measured rather than kernel-checked.
Date Provenance
commit f6bf075fd4ddd5f419826cf9abe10cd5b1b3a16b, hunts/cycle_moments/RESULTS.md, author 2026-09-05T12:51:19-07:00