feat: make ap_in_ff sorry-free

[dannyply]

Fill the remaining sorrys in the finite-field almost-periodicity proof, in particular the final gap in:

lemma ap_in_ff

The main changes are in:

APAP/FiniteField.lean

The proof adds private helper lemmas for the common-kernel/Fourier-closure bridge, controls the off-closure Fourier mass by comparing F with μ T ∗^ k ∗ F, and uses a Fourier-L1 smooth-tail estimate for the specific convolution structure appearing in the finite-field argument.

There is a substantial amount of code, so I have tried to keep the new auxiliary lemmas private/local to APAP/FiniteField.lean where possible. The only non-local supporting change is a small prerequisite adjustment in:

APAP/Prereqs/Inner/Hoelder/Compact.lean

allowing the compact Hölder lemmas to be used under a [Finite α] assumption rather than only an existing [Fintype α] instance.

The quantitative statement is not weakened: the proof preserves the existing 2 ^ 32 codimension bound.

Note: Produced with assistance from a prototype agentic Lean proof-search system. Codex was used for review, refinement and simplification.

[YaelDillies]

Now that I have merged #15, you need to fix the merge conflicts here.

[dannyply]

I rebased on current master after #15 and resolved the conflicts. Made a small cleanup pass on the touched code: I removed the local heartbeat increase by splitting out a small expectation-rearrangement helper and applied the same style cleanups from #15.

[YaelDillies]

Sorry, I just pushed a large refactor to use the material that was newly upstreamed from APAP to AddCombi in leanprover-community/add-combi#2. You will need to resolve conflicts again.

[dannyply]

Rebased on current master

[dannyply]

Rebased on current master

[YaelDillies]

Can you try generalising each of the prerequisite lemmas and moving them to earlier files?

[dannyply]

Thanks, I followed your suggestions by moving the reusable lemmas to earlier files, applying the generalizations and using grw.

[dannyply]

Thanks, I updated the remaining points as suggested and did another small cleanup pass.

[dannyply]

Fixed the build failure that my local stale .olean files had missed.

[YaelDillies]

Can you update the blueprint too? You need to add \leanok in the ff item.

[dannyply]

Can you update the blueprint too? You need to add \leanok in the ff item.

Doesn't the ff item already have \leanok? I see it in blueprint/src/chapter/ff.tex right after \lean{ff}.

[YaelDillies]

Oh sorry, I mean (the proof of) ap_in_ff

[dannyply]

Removed the local preimage lemma and rewrote the use through AddMonoidHomClass.isAddFreimanHom ... .threeAPFree.

[YaelDillies]

Thank you very much!