Rényi and Tsallis entropy monotonicity for Bernoulli sums
Lean formalization of coordinatewise Rényi and Tsallis entropy monotonicity for finite independent Bernoulli sums on the closed half cube, for every real order in [0,2], as stated in Hillion-Johnson Conjecture 4.4. The complete core proves both entropy comparisons and the finite inverse-score association inequality. Concrete coefficient-law and entropy definitions are checked separately. VERIFICATION.md defines exact-source Linux acceptance and distinguishes historical association-only checkpoints.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'