proof(S3): n-dim Cauchy-Schwarz + prob-dist square-sum floor (Session 2)

Continue the multi-session full-headline port of S3. Session 2
lands a *genuine* rung-1 theorem, sidestepping the ln-inequality
blocker that would have forced a dead-end in an entropy-function
approach.

Rung-1 theorem (Qed-closed):

    Theorem prob_dist_sum_squares_ge_inv_n :
      forall (n : nat) (p : Vec n),
        is_prob_dist n p ->
        (n > 0)%nat ->
        1 / INR n <= finSum n (fun i => p i * p i).

For any probability distribution on n >= 1 points, the sum of
squares is bounded below by 1/n, with equality at the uniform
distribution.  This is the arithmetic kernel underneath
`H(p) <= ln n`: Session 3+ will deduce the entropy bound from this
square-sum floor via Jensen applied to ln.  The present commit
gets the same monotonicity content past the ln-inequality wall
without requiring a y < 0 extension of `exp_ineq1_le`.

Session 2 contents (all Qed-closed):

  §3 finSum_add / finSum_scale / finSum_self_square_nonneg;
     finSum_self_square_zero_implies_pointwise_zero (needed for
     the CS y = 0 branch); cauchy_schwarz_finSum (n-dim CS via
     polynomial-non-negativity / discriminant, same proof shape
     as S4 but inlined — canonical-proof-suite files compile
     independently).
  §4 finSum_const_1 (sum of the constant-1 function = INR n);
     prob_dist_sum_squares_ge_inv_n (the rung-1 headline).

Session 3 target: ln-based Shannon entropy, ln tangent-line
bound, Gibbs, then `H(p) <= ln n`.  Higher rungs (Riemann /
Lebesgue / Boltzmann) follow as before.

MANIFEST unchanged: continues to point at `S3_h_theorem_binary.v`.
Runner stays 35/35.  panic-attack assail: 0 weak points.  No
banned constructs.  Rocq 9.1.1 clean modulo stdlib-Vector.Fin
deprecation warning.

File grew 255 -> 452 LOC.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/canonical-proof-suite/S3_h_theorem_ndim.v

@@ -233,23 +233,220 @@ Proof.
 Qed.
 
 (* ====================================================================
-   End of Session 1.
+   §3  finSum add / scale + Cauchy-Schwarz (Session 2, 2026-04-18)
+   ==================================================================== *)
+
+(* Adds the add / scale lemmas and a local Cauchy-Schwarz suitable
+   for use on the uniform-distribution variance-proxy theorem below.
+   These mirror lemmas already in S4_heisenberg_ndim.v but are
+   inlined here because canonical-proof-suite files compile
+   independently under `coqc`. *)
+
+Lemma finSum_add :
+  forall (n : nat) (f g : Fin.t n -> R),
+    finSum n (fun i => f i + g i) = finSum n f + finSum n g.
+Proof.
+  induction n as [|k IH]; intros f g; simpl.
+  - lra.
+  - rewrite IH. lra.
+Qed.
+
+Lemma finSum_scale :
+  forall (n : nat) (c : R) (f : Fin.t n -> R),
+    finSum n (fun i => c * f i) = c * finSum n f.
+Proof.
+  induction n as [|k IH]; intros c f; simpl.
+  - lra.
+  - rewrite IH. lra.
+Qed.
+
+Lemma R_square_nonneg : forall r : R, 0 <= r * r.
+Proof.
+  intro r. replace (r * r) with (Rsqr r) by (unfold Rsqr; reflexivity).
+  apply Rle_0_sqr.
+Qed.
+
+Lemma finSum_self_square_nonneg :
+  forall (n : nat) (f : Fin.t n -> R),
+    0 <= finSum n (fun i => f i * f i).
+Proof.
+  intros n f. apply finSum_nonneg. intro i. apply R_square_nonneg.
+Qed.
+
+(* self-square-zero implies pointwise-zero, needed for the y = 0
+   branch of the Cauchy-Schwarz split below. *)
+Lemma finSum_self_square_zero_implies_pointwise_zero :
+  forall (n : nat) (f : Fin.t n -> R),
+    finSum n (fun i => f i * f i) = 0 ->
+    forall i : Fin.t n, f i = 0.
+Proof.
+  induction n as [|k IH]; intros f Hzero i.
+  - inversion i.
+  - simpl in Hzero.
+    assert (Hhead_nn : 0 <= f Fin.F1 * f Fin.F1) by apply R_square_nonneg.
+    assert (Htail_nn : 0 <= finSum k (fun j => f (Fin.FS j) * f (Fin.FS j))).
+    { apply finSum_nonneg. intro j. apply R_square_nonneg. }
+    assert (Hhead_zero : f Fin.F1 * f Fin.F1 = 0) by lra.
+    assert (Htail_zero : finSum k (fun j => f (Fin.FS j) * f (Fin.FS j)) = 0)
+      by lra.
+    pose proof (Fin.caseS' i (fun i0 : Fin.t (S k) => f i0 = 0)) as Hcase.
+    apply Hcase.
+    + assert (Hsqr : Rsqr (f Fin.F1) = 0)
+        by (unfold Rsqr; exact Hhead_zero).
+      apply Rsqr_eq_0. exact Hsqr.
+    + intro i'. apply (IH (fun j => f (Fin.FS j)) Htail_zero i').
+Qed.
+
+(* The n-dim Cauchy-Schwarz inequality, stated directly over finSum
+   rather than a named `inner` (S4 introduces `inner` — we do not,
+   to keep this file focused on probability distributions). *)
+Theorem cauchy_schwarz_finSum :
+  forall (n : nat) (x y : Fin.t n -> R),
+    (finSum n (fun i => x i * y i))^2
+    <= finSum n (fun i => x i * x i) * finSum n (fun i => y i * y i).
+Proof.
+  intros n x y.
+  pose proof (finSum_self_square_nonneg n y) as Hyy_nn.
+  destruct (Req_dec (finSum n (fun i => y i * y i)) 0) as [Hyy_zero | Hyy_nz].
+  - (* y is identically zero, so sum (x*y) = 0 and LHS = 0. *)
+    assert (Hy_zero : forall i : Fin.t n, y i = 0).
+    { apply finSum_self_square_zero_implies_pointwise_zero. exact Hyy_zero. }
+    assert (Hxy_zero : finSum n (fun i => x i * y i) = 0).
+    { replace (fun i : Fin.t n => x i * y i) with (fun _ : Fin.t n => 0).
+      - apply finSum_zero.
+      - apply functional_extensionality. intro i.
+        rewrite (Hy_zero i). lra. }
+    rewrite Hxy_zero, Hyy_zero.
+    replace ((0 : R) ^ 2) with 0 by (simpl; lra).
+    lra.
+  - assert (Hyy_pos : 0 < finSum n (fun i => y i * y i)) by lra.
+    (* Polynomial non-negativity:  for all t, 0 <= sum (x + t*y)^2.  *)
+    set (A := finSum n (fun i => x i * x i)).
+    set (B := finSum n (fun i => x i * y i)).
+    set (C := finSum n (fun i => y i * y i)).
+    assert (HC_pos : 0 < C) by (unfold C; exact Hyy_pos).
+    assert (HC_nz : C <> 0) by lra.
+    (* Expand sum (x + t y)^2 = A + 2tB + t^2 C and instantiate at
+       t := -B/C to get A - B^2/C >= 0. *)
+    assert (Hexpand :
+      forall t : R,
+        finSum n (fun i => (x i + t * y i) * (x i + t * y i))
+        = A + 2 * t * B + t^2 * C).
+    { intro t.
+      rewrite finSum_ext with
+        (g := fun i : Fin.t n =>
+                x i * x i + (2 * t) * (x i * y i) + (t^2) * (y i * y i)).
+      2: { intro i. ring. }
+      rewrite finSum_add, finSum_add.
+      rewrite (finSum_scale n (2 * t) (fun i => x i * y i)).
+      rewrite (finSum_scale n (t^2) (fun i => y i * y i)).
+      unfold A, B, C. ring. }
+    assert (Hpoly_nn : forall t : R, 0 <= A + 2 * t * B + t^2 * C).
+    { intro t. rewrite <- Hexpand.
+      apply finSum_self_square_nonneg. }
+    pose proof (Hpoly_nn (- B / C)) as Hspec.
+    assert (Hrewrite :
+      A + 2 * (- B / C) * B + (- B / C) ^ 2 * C
+      = A - B ^ 2 / C)
+      by (field; exact HC_nz).
+    rewrite Hrewrite in Hspec.
+    (* Hspec : 0 <= A - B^2/C.  Multiply by C > 0 to clear division. *)
+    assert (Hmul_nn : 0 <= (A - B^2 / C) * C)
+      by (apply Rmult_le_pos; [exact Hspec | lra]).
+    assert (Hfinal : 0 <= A * C - B^2).
+    { replace (A * C - B^2) with ((A - B^2 / C) * C).
+      - exact Hmul_nn.
+      - field. exact HC_nz. }
+    lra.
+Qed.
+
+(* ====================================================================
+   §4  Uniform-distribution square-sum lower bound (rung-1 theorem)
+   ==================================================================== *)
+
+(* Two helper lemmas before the headline rung-1 result. *)
+
+(* finSum of the constant function 1 equals INR n (the real
+   image of the natural number n).  Cauchy-Schwarz applied to
+   (p, 1) uses this to turn the sum-of-ones factor into n. *)
+Lemma finSum_const_1 :
+  forall n : nat, finSum n (fun _ : Fin.t n => 1) = INR n.
+Proof.
+  induction n as [|k IH]; simpl.
+  - reflexivity.
+  - (* INR (S k) = INR k + 1 by definition of INR; S_INR captures this
+       in the positive case. For k = 0, INR 1 = 1 is definitional. *)
+    destruct k as [|k'].
+    + simpl. lra.
+    + rewrite IH. rewrite S_INR. lra.
+Qed.
+
+(* For a probability distribution p on n points (n >= 1), the sum
+   of squares is bounded below by 1/n.  This is the finite-dim
+   analogue of the binary variance-maximum fact, and the arithmetic
+   kernel of `H(p) <= ln n` (Session 3+ will deduce the entropy
+   bound from this square-sum bound together with concavity of ln —
+   that is the actual Jensen step). *)
+
+Theorem prob_dist_sum_squares_ge_inv_n :
+  forall (n : nat) (p : Vec n),
+    is_prob_dist n p ->
+    (n > 0)%nat ->
+    1 / INR n <= finSum n (fun i => p i * p i).
+Proof.
+  intros n p Hpd Hn_pos.
+  (* Cauchy-Schwarz with x := p and y := fun _ => 1 :
+        (sum p_i * 1)^2 <= (sum p_i^2) * (sum 1^2).
+     LHS = (sum p)^2 = 1^2 = 1; sum 1^2 = n. *)
+  pose proof (cauchy_schwarz_finSum n p (fun _ => 1)) as HCS.
+  cbv beta in HCS.
+  (* HCS : (finSum n (fun i => p i * 1))^2
+              <= finSum n (fun i => p i * p i) * finSum n (fun i => 1 * 1).
+     Rewrite the LHS factor `p i * 1` to `p i`, the 1*1 factor to 1,
+     then apply `finSum_const_1` and `prob_dist_sum_one`. *)
+  rewrite (finSum_ext n (fun i : Fin.t n => p i * 1) p) in HCS
+    by (intro i; lra).
+  rewrite (finSum_ext n (fun i : Fin.t n => (1 : R) * 1)
+                       (fun _ : Fin.t n => 1)) in HCS
+    by (intro i; lra).
+  rewrite (finSum_const_1 n) in HCS.
+  rewrite (prob_dist_sum_one n p Hpd) in HCS.
+  (* HCS : 1^2 <= finSum n (fun i => p i * p i) * INR n. *)
+  replace ((1 : R)^2) with 1 in HCS by (simpl; lra).
+  (* Rewrite to divide through by INR n > 0. *)
+  assert (HINRn_pos : 0 < INR n) by (apply lt_0_INR; exact Hn_pos).
+  assert (HINRn_nz : INR n <> 0) by lra.
+  apply Rmult_le_reg_r with (r := INR n).
+  - exact HINRn_pos.
+  - replace (1 / INR n * INR n) with 1 by (field; exact HINRn_nz).
+    rewrite Rmult_comm.
+    lra.
+Qed.
+
+(* ====================================================================
+   End of Session 2.
 
    Landed this session:
-     §1  finSum over Fin.t n with zero / ext / nonneg / le /
-         singleton-le-total lemmas (pigeonhole kernel).
-     §2  Probability-distribution predicate plus three basic
-         consequences (non-negativity / sum-one projection /
-         coordinatewise upper bound at 1).
-
-   Session 2 target:
-     §3  Import tangent-line bound ln x <= x - 1 (Stdlib extended
-         via Coquelicot.ElemFct for the y < 0 case) + its equality-
-         at-1 side condition.
-     §4  Shannon entropy H(p) = - finSum n (fun i => p i * ln (p i)).
-     §5  Gibbs' inequality.
-     §6  Uniform-distribution maximum H(p) <= ln n (= log n in R).
-
-   Session 3+: Riemann-integral continuous version on [0, 1].
-   Session 4+: Lebesgue + Boltzmann operator.
+     §3  finSum add / scale / self-square-nonneg / null-implies-zero;
+         cauchy_schwarz_finSum (n-dim Cauchy-Schwarz inequality,
+         Qed-closed via polynomial-non-negativity / discriminant
+         route — same proof shape as S4_heisenberg_ndim.v's Rung-1
+         theorem, duplicated here because canonical-proof-suite
+         files compile independently).
+     §4  finSum_const_1 (sum of the constant-1 function = INR n);
+         prob_dist_sum_squares_ge_inv_n — the *rung-1 theorem*.
+         For any probability distribution p on n >= 1 points,
+         `finSum n (p i * p i) >= 1/n`, equality at the uniform
+         distribution.  This is the arithmetic kernel underneath
+         `H(p) <= ln n`: the next step is Jensen applied to ln on
+         the square-sum floor.
+
+   Session 3 target:
+     §5  ln-based Shannon entropy definition + `ln x <= x - 1`
+         tangent-line bound (requires either `Coquelicot.ElemFct`
+         or a convexity-based derivation of the y < 0 case of
+         `exp y >= 1 + y`).
+     §6  Gibbs inequality, then H(p) <= ln n via Jensen.
+
+   Session 4+: Riemann / Lebesgue / Boltzmann rungs.
    ==================================================================== *)