feat(lattices): prove the Hachi subfield factor swap

[MrBrain295]

No description provided.

[github-actions]

🤖 PR Summary

sorry delta: -1 (1 removed) — net proof progress

The Hachi Lemma 5 formalization is now complete. The final gap—proving that an irreducible factor p₁ of X^{2^α}+1 over ℤ_q (with q ≡ 5 mod 8, α ≥ 1) is not self‑reciprocal—has been filled. The Lean file Field.lean gains two new theorems not_associated_reverse_self and no_selfReciprocal_factor, and the auxiliary lemma reverse_X_pow_add_one is added. All previously present sorrys are removed, making the entire chain unconditional. The blueprint .tex is updated to reflect this completion.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	279
❌ Lines Removed	31

---

Lean Declarations

✏️ Added: 2 declaration(s)

ArkLib/Data/Lattices/CyclotomicRing/Subfield/Field.lean (2)

• theorem not_associated_reverse_self (hq5 : q % 8 = 5) {α : ℕ} (hα : 1 ≤ α)
• theorem reverse_X_pow_add_one {R : Type*} [Semiring R] [Nontrivial R] {n : ℕ} :

---

sorry Tracking

✅ Removed: 1 `sorry`(s)

ArkLib/Data/Lattices/CyclotomicRing/Subfield/Field.lean (1)

• theorem no_selfReciprocal_factor (hq5 : q % 8 = 5) {α : ℕ} (hα : 1 ≤ α) (L211)

---

📋 **Additional Analysis**

The diff fills the final sorry (no_selfReciprocal_factor), rewrites the Status section from "open for contribution" to "complete", removes all sorry references from the module docstring and the Blueprint TeX, and updates commentary accordingly.

Violation of the naming convention for no_selfReciprocal_factor:

The theorem name contains the string selfReciprocal, which mixes lowerCamelCase and what appears to be a compound word. According to the style guide, Theorems and Proofs should use snake_case. The name no_self_reciprocal_factor would be correct.

The auxiliary theorem not_associated_reverse_self appears to be a lemma (theorem) aiding the main result; its name is not consistent with the snake_case convention for theorems (it uses lowerCamelCase). This is a violation.

Summary of Violations:

• no_selfReciprocal_factor: Theorems must use snake_case. (Should be no_self_reciprocal_factor)
• not_associated_reverse_self: Theorems must use snake_case. (Should be not_associated_reverse_self is arguably already snake_case – let me re-check: not_associated_reverse_self has underscores and is all lower-case apart from the first word, which is a standard snake_case pattern. Actually, it is snake_case.) A re-check: not_associated_reverse_self is snake_case. Therefore not a violation. That leaves only no_selfReciprocal_factor.

No other violations of the supplied instructions were found.

---

📄 **Per-File Summaries**

• ArkLib/Data/Lattices/CyclotomicRing/Subfield/Field.lean: This diff fills the last gap in the Hachi Lemma 5 chain by proving no_selfReciprocal_factor (blueprint Lemma 4.5) and its core lemma not_associated_reverse_self. The former is now a full proof (replacing the previous sorry), and the latter is a new theorem establishing that an irreducible factor p₁ of X^{2^α}+1 over Z_q (with q ≡ 5 mod 8, α ≥ 1) cannot be self-reciprocal, using a root-orbit argument in the field K = AdjoinRoot p₁. The existing theorem reverse_X_pow_add_one is also added, proving that X^n + 1 is self-reciprocal. The status comments throughout the file are updated to reflect that all proofs are now complete and unconditional.
• blueprint/src/lattices/hachi_subfield.tex: The blueprint now records that Lemma 5.4 (no_selfReciprocal) has been formalized, removing the previously noted sorry. The status summary and final paragraph are updated to reflect that the entire Hachi Lemma 5 formalization is complete, including the fixed subring being a field isomorphic to $(F_{q^k}$ and the packing map and trace formula. The sole remaining sorry is eliminated, and the section now describes the completed formalization rather than a work‑in‑progress.

---

Last updated: 2026-08-30 08:27 UTC.

[github-actions]

Build Timing Report

• Commit: bc0a5a5
• Message: finish Feild.lean
• Ref: patch-2
• Comparison baseline: 0bc5c50 from current base of main.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	825.58	600.41	-225.17	ok
Warm rebuild	2.26	2.09	-0.17	ok
Validation wrapper	2.47	2.12	-0.35	ok

Incremental Rebuild Signal

• Warm rebuild saved 598.32s vs clean (287.28x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
75.00	132.00	-57.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
46.00	68.00	-22.00	ArkLib/ProofSystem/Stir/Combine.lean
44.00	56.00	-12.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
40.00	56.00	-16.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
39.00	53.00	-14.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
39.00	60.00	-21.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
36.00	48.00	-12.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
36.00	51.00	-15.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
33.00	54.00	-21.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
30.00	42.00	-12.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
27.00	39.00	-12.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
25.00	34.00	-9.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
25.00	33.00	-8.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
24.00	31.00	-7.00	ArkLib/OracleReduction/Security/RoundByRound.lean
24.00	28.00	-4.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean
24.00	34.00	-10.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
23.00	30.00	-7.00	ArkLib/Commitments/Functional/KZG/FunctionBinding/EvaluationBindingConflict.lean
23.00	37.00	-14.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
22.00	31.00	-9.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
22.00	23.00	-1.00	ArkLib/Commitments/Functional/KZG/Binding.lean

[quangvdao]

PR Review findings

1. Moderate: Update the canonical Hachi status documentation

The proof is complete, but the subfield landing page still lists no_selfReciprocal_factor as open. The blueprint also says the theorem remains a sorry in the theorem statement and the status summary. This contradicts the completion claim in Field.lean.

Why it matters: Contributors who use the blueprint or landing page will think the main Hachi subfield theorem remains open. The documentation dependency status is also wrong.

Required correction: Add \leanok, remove the stale sorry text, update the blueprint status summary, and remove the theorem from the landing page's open items.

2. Low: Fix the PR title and add a description

The title, finish Feild.lean, has a typo and does not follow the repository's PR conventions. The PR body is empty.

Required correction: A suitable title is feat(lattices): prove the Hachi subfield factor swap. Please add a short body that states the theorem, the root orbit argument, and the validation performed.

3. Low: Clean up the added formatting

There are four consecutive blank lines. Several added lines exceed the repository's 100 character guideline.

Required correction: Remove the extra blank lines and wrap the long lines.

Specification alignment

Requirement	Assessment
Remove the final sorry from Field.lean	Met
Prove the root orbit contradiction using -1 ∉ ⟨q⟩	Met
Derive reversal swapping the two irreducible factors	Met
Preserve downstream field and isomorphism results	Met. The full Lean CI build passes.
Update the blueprint and landing page status	Not met
Follow the PR metadata conventions	Not met

I found no mathematical correctness issue. The proof establishes the root order, computes the extension degree, identifies the roots as a Frobenius orbit, and obtains the required contradiction if the inverse root belongs to that orbit. I found no circular dependency or bad edge case at α = 1.

Residual risks and unverified surfaces

I could not independently run #print axioms because the pinned Lean 4.31.0 toolchain was unavailable locally. The exact head passes the full Lean CI build. A source scan found no sorry, admit, axiom, or Lean.ofReduceBool in the changed file.

The website job is currently failing because of unrelated missing blueprint declarations. The Lean build and all other checks pass.

Deslop and abstraction review

Earned abstractions

Declaration	Responsibility	Assessment
reverse_X_pow_add_one	Proves that Xⁿ + 1 is self reciprocal	Focused and reusable
not_associated_reverse_self	Owns the root orbit argument that excludes self reciprocity	Long but cohesive
no_selfReciprocal_factor	Converts that exclusion into the factor swap	Clean assembly

Unnecessary or overgrown abstractions

I found none.

Reviewed exact head bc0a5a5986fd53105c8a87c9eb0d9360be85e58b.

[MrBrain295]

@quangvdao is this good to merge now?