feat(Verified-zkEVM#138): expose explicit xi P1 alpha invariant

Author: lalalune

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P1ConditionalAll.lean

@@ -66,6 +66,23 @@ theorem βHenselStructuredWeightInvariant_all_of_lift'
   βHenselStructuredWeightInvariant_all_of_lift H x₀ R hHyp hH hDH hlift hα
     (ClaimA2.weight_ξ_bound x₀ hH hHyp hdR2 hDH hDRx0)
 
+/-- Direct `P1Conditional` alias for the explicit-`ξ` carved-alpha all-prefix route. -/
+theorem βHenselStructuredWeightInvariant_all_of_alphaWeight
+    (x₀ : F) (R : F[X][X][Y]) (hHyp : ClaimA2.Hypotheses x₀ R H)
+    (hH : 0 < H.natDegree) {D : ℕ}
+    (hDH : Bivariate.totalDegree H ≤ D)
+    (hlift : ∀ t : ℕ,
+      embeddingOf𝒪Into𝕃 H (βHensel H x₀ R hHyp t)
+        = αGenuine H x₀ R hHyp t
+            * (liftToFunctionField (H := H) H.leadingCoeff) ^ (t + 1)
+            * (embeddingOf𝒪Into𝕃 H (ClaimA2.ξ x₀ R H hHyp)) ^ (2 * t - 1))
+    (hα : AlphaGenuineRegularWeightLe H x₀ R hHyp hH D)
+    (hξ : weight_Λ_over_𝒪 hH (ClaimA2.ξ x₀ R H hHyp) D
+            ≤ WithBot.some ((Bivariate.natDegreeY R - 1) * (D - Bivariate.natDegreeY H + 1))) :
+    ∀ k, βHenselStructuredWeightInvariant (D := D) H x₀ R hHyp hH k :=
+  AlphaWeight.βHenselStructuredWeightInvariant_all_of_alphaWeight
+    H x₀ R hHyp hH hDH hlift hα hξ
+
 /-- Direct `P1Conditional` alias for the discharged-`ξ` carved-alpha all-prefix route. -/
 theorem βHenselStructuredWeightInvariant_all_of_alphaWeight'
     (x₀ : F) (R : F[X][X][Y]) (hHyp : ClaimA2.Hypotheses x₀ R H)
@@ -80,8 +97,8 @@ theorem βHenselStructuredWeightInvariant_all_of_alphaWeight'
             * (embeddingOf𝒪Into𝕃 H (ClaimA2.ξ x₀ R H hHyp)) ^ (2 * t - 1))
     (hα : AlphaGenuineRegularWeightLe H x₀ R hHyp hH D) :
     ∀ k, βHenselStructuredWeightInvariant (D := D) H x₀ R hHyp hH k :=
-  AlphaWeight.βHenselStructuredWeightInvariant_all_of_alphaWeight'
-    H x₀ R hHyp hH hDH hDRx0 hdR2 hlift hα
+  βHenselStructuredWeightInvariant_all_of_alphaWeight H x₀ R hHyp hH hDH hlift hα
+    (ClaimA2.weight_ξ_bound x₀ hH hHyp hdR2 hDH hDRx0)
 
 /-- Package the `P1Conditional` `DivWeightLe` route into an all-`k` structured invariant. -/
 theorem βHenselStructuredWeightInvariant_all_of_divWeight
@@ -637,6 +654,7 @@ end BCIKS20.HenselNumerator
 -- axiom dependencies beyond the imported standard surface.
 #print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_lift
 #print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_lift'
+#print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_alphaWeight
 #print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_alphaWeight'
 #print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_divWeight
 #print axioms BCIKS20.HenselNumerator.βHenselStructuredWeightInvariant_all_of_divWeight'