fixes

Author: tobias-rothmann

ArkLib/Commitments/Functional/Hachi/RingSwitch/Reduction.lean

@@ -165,22 +165,10 @@ theorem vecLInftyNorm_le_of_liftShort (s : RlinStatement Φ n μ) (w : LiftedWit
     vecLInftyNorm Φ w.z ≤ s.bound :=
   le_trans hshort.1 hside
 
-/-! ### Why the CWSS certificate is exposed only as `liftPackage.isCWSS`
-
-We deliberately do **not** provide a standalone `lift_coordinateWiseSpecialSound` restated in
-Hachi's `relRlinE`/`relLiftE` relation vocabulary. Doing so forces the elaborator to check a
-`whnf` defeq between that vocabulary and the generic `Lift.relLin`/`Lift.relOutE`/`Lift.verifier`
-*inside the full `coordinateWiseSpecialSound` proposition* — which unfolds `Rq`'s computable layer
-(via the `verifier`) and times out (`maximum number of heartbeats` at `whnf`). The certificate is
-therefore `liftPackage.isCWSS` (generic `Lift.coordinateWiseSpecialSound` specialized). Crucially,
-the `▷` seams in `Composition.lean` still close by `rfl`: that `rfl` compares only the two relations
-(structurally identical after β-reduction — same `*ᵥ` subterms), never the verifier. -/
-
-/-- Hachi's `Lift` instance as a composable CWSS package, **assembled wholesale from generic
-`Lift.package`** at the cyclotomic presentation: the verifier, structure, purity witness, and
-CWSS certificate are all the generic layer's. Hachi supplies only the presentation data
+/-- Hachi's `Lift` instance as a composable CWSS package, reusing the generic ring-switching
+`Lift.package` at the cyclotomic presentation. Hachi supplies only the presentation data
 (`cyclotomicPresentation`/`isPresentation_cyclotomic`) and the norm implication
-(`vecLInftyNorm_le_of_liftShort`). -/
+(`vecLInftyNorm_le_of_liftShort`); the CWSS certificate is `liftPackage.isCWSS`. -/
 noncomputable def liftPackage (init : ProbComp σ) (impl : QueryImpl oSpec (StateT σ ProbComp))
     (hd : 0 < Φ.φ.natDegree) :
     CWSSPackage init impl

ArkLib/Data/Lattices/CyclotomicRing/QuotientLift.lean

@@ -21,13 +21,14 @@ import ArkLib.Data.Lattices.Vectors
   `Commitments/Functional/Hachi/RingSwitch/Reduction.lean`, since `Data` does not import
   `ProofSystem`):
 
-  * `Rq.natDegree_val_toPoly_lt'` — representatives are degree-reduced (any modulus of
-    positive degree, generalizing the `powTwoCyclotomic`-pinned version);
   * `val_toPoly_injective` — representatives are injective;
   * `modulus_dvd_toPoly_add_sub` / `modulus_dvd_toPoly_mul_sub` — the coset laws: reduction
     changes the representative of a sum/product by a multiple of the modulus, via the
     semantic quotient bridge `quotientHom`.
 
+  The remaining presentation law — representatives are degree-reduced — is
+  `Rq.natDegree_val_toPoly_lt'` in `Rq.lean`, next to the other `Rq` degree lemmas.
+
   ## References
 
   * [Huang, M.-Y. M., Mao, X., and Zhang, J., *Sublinear Proofs over Polynomial Rings*][HMZ25]
@@ -43,17 +44,7 @@ variable {R : Type*} [Field R]
 
 variable [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) [IsCyclotomic Φ]
 
-/-! ## Degree bound and injectivity of canonical representatives -/
-
-/-- A reduced representative has `natDegree` below `d = deg φ` — the any-modulus version of
-`Rq.natDegree_val_toPoly_lt` (which is pinned to `powTwoCyclotomic`), with the dimension
-positivity `0 < d` as an explicit hypothesis. -/
-theorem Rq.natDegree_val_toPoly_lt' (hd : 0 < Φ.φ.natDegree) (a : Rq Φ) :
-    a.1.toPoly.natDegree < Φ.φ.natDegree := by
-  rcases eq_or_ne a.1.toPoly 0 with h0 | hne
-  · rw [h0, Polynomial.natDegree_zero]; exact hd
-  · rw [CompPoly.CPolynomial.natDegree_toPoly]
-    exact Polynomial.natDegree_lt_natDegree hne (Φ.degree_toPoly_lt_of_reduced a.2)
+/-! ## Injectivity of canonical representatives -/
 
 omit [IsCyclotomic Φ] in
 /-- Canonical representatives are injective: `Rq` elements with equal representative

ArkLib/Data/Lattices/CyclotomicRing/Rq.lean

@@ -293,16 +293,22 @@ theorem mk_sum {ι : Type*} (s : Finset ι) (f : ι → CPolynomial R) :
   · intro a s ha ih
     rw [Finset.sum_insert ha, Finset.sum_insert ha, mk_add, ih]
 
-/-- A reduced representative of the power-of-two cyclotomic ring has `natDegree` below the ring
-dimension `2^α`. -/
-theorem natDegree_val_toPoly_lt (α : ℕ) (a : Rq (powTwoCyclotomic (R := R) α)) :
-    a.1.toPoly.natDegree < (powTwoCyclotomic (R := R) α).φ.natDegree := by
+/-- A reduced representative has `natDegree` below `d = deg φ`, for **any** modulus of positive
+degree (the dimension positivity `0 < d` is an explicit hypothesis). The `powTwoCyclotomic`-pinned
+`Rq.natDegree_val_toPoly_lt` below is derived from this general version. -/
+theorem natDegree_val_toPoly_lt' (hd : 0 < Φ.φ.natDegree) (a : Rq Φ) :
+    a.1.toPoly.natDegree < Φ.φ.natDegree := by
   rcases eq_or_ne a.1.toPoly 0 with h0 | hne
-  · rw [h0, Polynomial.natDegree_zero, powTwoCyclotomic_natDegree]
-    exact pow_pos (by norm_num) α
+  · rw [h0, Polynomial.natDegree_zero]; exact hd
   · rw [CompPoly.CPolynomial.natDegree_toPoly]
-    exact Polynomial.natDegree_lt_natDegree hne
-      ((powTwoCyclotomic (R := R) α).degree_toPoly_lt_of_reduced a.2)
+    exact Polynomial.natDegree_lt_natDegree hne (Φ.degree_toPoly_lt_of_reduced a.2)
+
+/-- A reduced representative of the power-of-two cyclotomic ring has `natDegree` below the ring
+dimension `2^α` — the special case of `Rq.natDegree_val_toPoly_lt'` for `φ = X^{2^α} + 1`. -/
+theorem natDegree_val_toPoly_lt (α : ℕ) (a : Rq (powTwoCyclotomic (R := R) α)) :
+    a.1.toPoly.natDegree < (powTwoCyclotomic (R := R) α).φ.natDegree :=
+  natDegree_val_toPoly_lt' (powTwoCyclotomic (R := R) α)
+    (by rw [powTwoCyclotomic_natDegree]; exact pow_pos (by norm_num) α) a
 
 /-! ## Constant embedding and coefficient-vanishing facts