finish Feild.lean

[MrBrain295]

No description provided.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: finish Feild.lean

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

PR Overview

This PR completes the module ArkLib/Data/Lattices/CyclotomicRing/Subfield/Field.lean by closing all remaining sorry placeholders and removing all dependency gaps. The file now provides a fully unconditional formal proof of the field isomorphism theorems for subfields of a special family of cyclotomic rings, resolving the last known open obligations in this component.

Proof Completion (sorries removed)

• All prior sorry placeholders in Field.lean have been eliminated.
• The theorem reverse_X_pow_add_one is added, proving a self-reciprocal identity for X^n + 1 (explicitly: reverse(n)(X^n + 1) = X^n + 1).
• The theorem not_associated_reverse_self is added, establishing (via a root-orbit argument) that an irreducible factor of X^{2^α} + 1 over Z_q, where q ≡ 5 mod 8 and α ≥ 1, cannot be self-reciprocal.
• The previously sorry-ed theorem no_selfReciprocal_factor, which asserts that reversal swaps the two irreducible factors in the relevant setting, is now proved using the two lemmas above.
• As a consequence, the definitions galoisAutₛ_fixed_isUnit and the field isomorphism theorems (establishing isomorphisms between subfields) are now unconditional — their hypotheses are fully satisfied by the completed proof chain.
• Status comments and docstrings throughout the file have been updated to reflect that all dependencies are closed.

Mathematical Formalization

The core change concentrates in Field.lean; no other files are modified. The newly added lemmas and the completed proof of no_selfReciprocal_factor fill the last gap in the argument that certain Galois-fixed subfields of the cyclotomic ring are in fact subfields (isomorphic to finite fields), a key ingredient for the broader cryptographic or lattice-based protocol soundness.

Infrastructure / CI

No infrastructure or CI changes.

Documentation

Docstrings updated where theorems were added or status changed.

Refactoring

No refactoring.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	264
❌ Lines Removed	12

---

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**

Findings

• Blank lines in proof bodies (violates "Avoid empty lines inside definitions or proofs"): In not_associated_reverse_self, there are empty lines after the by line and between hζ1 and hζne? Specifically, an empty line follows the by after not_associated_reverse_self (line with by then blank line then classical). Also a blank line appears between hζne : ζ ≠ 0 and the comment "the order of ζ".

• Blank lines in theorem statements: In no_selfReciprocal_factor, the proof contains an empty line after the by (line with by then blank line then classical).

• Multiple trailing blank lines (line with three empty lines before the next theorem): The diff shows several consecutive blank lines after not_associated_reverse_self and before the next theorem (no_selfReciprocal_factor).

• The open Polynomial in scope: Added open Polynomial in on reverse_X_pow_add_one and on not_associated_reverse_self. That is acceptable, but note that the second open Polynomial inis placed immediately before aomit` block; there is no issue.

• Naming/Case: not_associated_reverse_self is a theorem name using snake_case (correct). The name reverses the order: reverse_self may be ambiguous with guideline _of_ hypothesis ordering, but it is acceptable and not a clear violation.

• Use of reverse_mul_of_domain: The diff uses Polynomial.reverse_mul_of_domain; guideline prefers dot notation p.reverse_mul_of_domain? The theorem is a global theorem, so Polynomial.reverse_mul_of_domain is consistent with the guideline stating "Use namespaces to group related definitions (e.g., List.map)" — not a violation.

• Alignment in calc: In no_selfReciprocal_factor, the calc block for hdeg1 uses rw [reverse_natDegree, ...]—no calc block there. Not relevant.

• Line lengths: Checked that no lines exceed 100 characters in the added code by visual inspection; the longest line appears to be the hTcard block, e.g., simpa only [Finset.coe_range, Set.mem_Iio] at hi hj is under 100. No violation found.

• Docstring updates: The status updates are accurate (no sorry), and the Proof outline section is updated accordingly. No issue.

• Use of by placement: All by are placed at end of line (no violation).

• Indentation: 2-space indentation is used (correct).

• Empty lines in proofs: This is the main violation. Per style guide: "Avoid empty lines inside definitions or proofs." There are at least two such empty lines: one after the by in not_associated_reverse_self, one between hζne and the order-of comment, and one after by in no_selfReciprocal_factor. Additionally, there is an excessive block of empty lines (three) between theorem definitions.

Summary list:

• [Style] Remove empty lines inside proof bodies (occurs in both new theorem proofs).
• [Style] Remove extra consecutive blank lines between declarations (three blank lines before no_selfReciprocal_factor).
• No other violations of the supplied contributing guidelines found.

---

📄 **Per-File Summaries**

• ArkLib/Data/Lattices/CyclotomicRing/Subfield/Field.lean: The file now contains no sorrys. The theorem reverse_X_pow_add_one (self-reciprocal identity for X^n + 1) and not_associated_reverse_self (root-orbit argument that an irreducible factor of X^{2^α}+1 over Z_q with q ≡ 5 mod 8, α ≥ 1 cannot be self-reciprocal) were added. The previously sorry-ed theorem no_selfReciprocal_factor (reversal swaps the two irreducible factors) was completed using these two new lemmas. The status comment and docstrings were updated to reflect that all dependency gaps are closed; galoisAutₛ_fixed_isUnit and the field isomorphism theorems are now unconditional.

---

Last updated: 2026-08-06 14:14 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.