|
| 1 | +/- |
| 2 | +Copyright (c) 2026 ArkLib Contributors. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: ArkLib Contributors |
| 5 | +-/ |
| 6 | +import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.AlphaWeightDivisibility |
| 7 | +import ArkLib.Data.CodingTheory.ProximityGap.BCIKS20.P2MatchProof |
| 8 | + |
| 9 | +/-! |
| 10 | +# BCIKS20 Appendix A.4 (P1) — monic reduction of the weight invariant to the successor core (#138) |
| 11 | +
|
| 12 | +This file lands the **monic-`H` reduction** of the BCIKS20 Appendix A.4 weight invariant |
| 13 | +`AlphaGenuineRegularWeightLe` (#138), the P1 analogue of the now-proven monic P2 match |
| 14 | +`restrictedFaaDiBrunoMatch_of_monic` (#139). |
| 15 | +
|
| 16 | +For monic `H` (`H.leadingCoeff = 1`, the WLOG case of the minimal-polynomial reduction) three of the |
| 17 | +four inputs to the assembly lemma `AlphaGenuineRegularWeightLe.of_normalized_divWeight_cases_succLift` |
| 18 | +are already discharged, **axiom-clean**: |
| 19 | +
|
| 20 | +* the successor **lift identity** `hliftSucc` is `(P2_closed_of_leadingCoeff_one …).2` at order `t+1` |
| 21 | + (proven via the monic P2 match); |
| 22 | +* the **base** `h0` (`βHensel 0 = a · W𝒪` with `Λ_𝒪`-weight `≤ 1`) is `βHensel_zero_weight_le_one` |
| 23 | + together with the monic collapse `W𝒪 = 1` (`AlphaWeight.W𝒪_eq_one_of_monic`); |
| 24 | +* the `W`-factor of the successor clearing product collapses (`W𝒪 ^ (t+2) = 1`). |
| 25 | +
|
| 26 | +Hence the *entire* monic invariant follows from a single remaining obligation: the **successor |
| 27 | +divisibility-with-weight core** `SuccDivWeightLe_of_monic` — at every order, `βHensel (t+1)` is |
| 28 | +`ξ^{2t+1}`-divisible in `𝒪 H` with a quotient of `Λ_𝒪`-weight `≤ 1`. This is exactly the irreducible |
| 29 | +BCIKS20 Newton ξ-order-gain / `Λ(α_t) = 1` regularity claim; it is carried here as an explicit |
| 30 | +hypothesis, never an `axiom` or `sorry`. The reduction pins the open #138 obligation (in the monic |
| 31 | +case) to this single core, the same way `P2_closed_of_leadingCoeff_one` pinned #139. |
| 32 | +-/ |
| 33 | + |
| 34 | +open Polynomial Polynomial.Bivariate |
| 35 | +open BCIKS20AppendixA |
| 36 | +open ProximityPrize.BCIKS20.GammaGenuine |
| 37 | + |
| 38 | +namespace BCIKS20.HenselNumerator.AlphaWeight |
| 39 | + |
| 40 | +variable {F : Type} [Field F] |
| 41 | +variable (H : F[X][Y]) [Fact (Irreducible H)] [Fact (0 < H.natDegree)] |
| 42 | +variable {D : ℕ} |
| 43 | + |
| 44 | +/-- **The monic successor divisibility-with-weight obligation — the irreducible #138 core.** |
| 45 | +For monic `H` the clearing product collapses to `ξ^{2t+1}`, so the only open content of the |
| 46 | +successor divisibility-with-weight is: each `βHensel (t+1)` is `ξ^{2t+1}`-divisible in `𝒪 H` with a |
| 47 | +quotient of `Λ_𝒪`-weight `≤ 1`. This is the BCIKS20 Newton ξ-order-gain / weight-1 regularity core; |
| 48 | +it is genuinely open (the same weight-`≤-1` wall flagged in `AlphaWeight.lean`). -/ |
| 49 | +def SuccDivWeightLe_of_monic (x₀ : F) (R : F[X][X][Y]) (hHyp : ClaimA2.Hypotheses x₀ R H) |
| 50 | + (hH : 0 < H.natDegree) (D : ℕ) : Prop := |
| 51 | + ∀ t : ℕ, ∃ a : 𝒪 H, |
| 52 | + βHensel H x₀ R hHyp (t + 1) = a * (ClaimA2.ξ x₀ R H hHyp) ^ (2 * t + 1) |
| 53 | + ∧ weight_Λ_over_𝒪 hH a D ≤ WithBot.some 1 |
| 54 | + |
| 55 | +/-- **Monic reduction of the full A.4 weight invariant (#138) to its successor core.** |
| 56 | +For monic `H`, the order-0 invariant, the `W𝒪 = 1` collapse, and the successor lift identity |
| 57 | +(`P2_closed_of_leadingCoeff_one`, axiom-clean) are all discharged, so the full |
| 58 | +`AlphaGenuineRegularWeightLe` follows from *only* `SuccDivWeightLe_of_monic`. This is the P1 analogue |
| 59 | +of the proven monic P2 match: it reduces the remaining #138 obligation in the monic (WLOG) case to |
| 60 | +exactly the BCIKS20 Newton ξ-order-gain / weight-1 regularity core, with no `axiom`, no `sorry`. -/ |
| 61 | +theorem AlphaGenuineRegularWeightLe_of_monic_of_succDivWeight |
| 62 | + (x₀ : F) (R : F[X][X][Y]) (hHyp : ClaimA2.Hypotheses x₀ R H) |
| 63 | + (hH : 0 < H.natDegree) (hmonic : H.Monic) (hd : 2 ≤ H.natDegree) (hD : D ≤ H.natDegree) |
| 64 | + (hsucc : SuccDivWeightLe_of_monic H x₀ R hHyp hH D) : |
| 65 | + AlphaGenuineRegularWeightLe H x₀ R hHyp hH D := by |
| 66 | + have hlc : H.leadingCoeff = 1 := hmonic |
| 67 | + refine AlphaGenuineRegularWeightLe.of_normalized_divWeight_cases_succLift |
| 68 | + H x₀ R hHyp hH D (fun t => ?_) ?_ (fun t => ?_) |
| 69 | + · exact (BCIKS20.HenselNumerator.P2_closed_of_leadingCoeff_one H x₀ R hHyp hlc).2 (t + 1) |
| 70 | + · refine ⟨βHensel H x₀ R hHyp 0, ?_, βHensel_zero_weight_le_one H x₀ R hHyp hH hd hD⟩ |
| 71 | + rw [W𝒪_eq_one_of_monic H hmonic, mul_one] |
| 72 | + · obtain ⟨a, ha, hwt⟩ := hsucc t |
| 73 | + refine ⟨a, ?_, hwt⟩ |
| 74 | + rw [W𝒪_eq_one_of_monic H hmonic, one_pow, mul_one] |
| 75 | + exact ha |
| 76 | + |
| 77 | +end BCIKS20.HenselNumerator.AlphaWeight |
| 78 | + |
| 79 | +/-! ## Source audit -/ |
| 80 | +#print axioms |
| 81 | + BCIKS20.HenselNumerator.AlphaWeight.AlphaGenuineRegularWeightLe_of_monic_of_succDivWeight |
0 commit comments