proof(S4): norm triangle inequality (Session 2, §4 Qed)

Lands Session-2 content for S4_heisenberg_ndim.v (+97 LOC):

  - inner_expand_xpy       : <x+y, x+y> = <x,x> + 2<x,y> + <y,y>
  - abs_inner_le_sqrt_product : |<x,y>| <= sqrt<x,x> * sqrt<y,y>
  - norm_triangle_ndim     : **Qed** sqrt(<x+y,x+y>) <=
                             sqrt<x,x> + sqrt<y,y>

Classical derivation: expand the diagonal inner product,
bound the cross term via the Rung-1 Cauchy-Schwarz lifted into Rabs
form through Rsqr_le_abs_0, recognise the RHS as a perfect square,
take sqrt of both sides via sqrt_le_1 + sqrt_pow2 on the
already-non-negative sum.

Library: Stdlib.Reals (R_sqrt) + Lra; nra used locally for
polynomial identities.  No Coquelicot, no mathcomp-analysis.

Scope note: this is NOT Rung-2 (complex C^n Cauchy-Schwarz with
conjugate symmetry).  Rung-2 requires complex-number substrate that
isn't in the current opam switch and would need ~200 LOC of in-file
buildup (C := R * R, conjugation, modulus).  Session 2 instead
lands the real-scalar triangle inequality — a genuine Qed, a real
corollary of Rung-1, and a building block any future Rung-3
abstract pre-Hilbert record can be tested against.

Gate: panic-attack assail on S4_heisenberg_ndim.v reports 0 weak
points.  Suite: 35/35 passing, exit 0.

MANIFEST pointer stays at S4_heisenberg_discrete.v per §3.1 honest-
accounting.  Session 3+ plan: complex C^n Cauchy-Schwarz (requires
complex substrate); then abstract pre-Hilbert record; then
Heisenberg proper via self-adjoint-operator commutator algebra.

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

Author: hyperpolymath

audits/canonical-proof-suite/REPORT.a2ml

@@ -6,7 +6,7 @@
   (metadata
     (project "007")
     (suite-spec-version "1.0")
-    (run-utc "2026-04-19T02:14:44Z")
+    (run-utc "2026-04-19T02:15:25Z")
     (host "fedora")
     (manifest "audits/canonical-proof-suite/MANIFEST.a2ml"))
   (summary
@@ -19,39 +19,39 @@
     (not-started 0)
     (prover-missing 0))
   (entries
-    (entry (id "M1") (status "passing") (elapsed-ms 2695) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
-    (entry (id "M2") (status "passing") (elapsed-ms 1132) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
-    (entry (id "M3") (status "passing") (elapsed-ms 872) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
-    (entry (id "M4") (status "passing") (elapsed-ms 820) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M4_compactness_unit_interval.v") (semantic-check "verified"))
-    (entry (id "M5") (status "passing") (elapsed-ms 331) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
-    (entry (id "S1") (status "passing") (elapsed-ms 153) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
-    (entry (id "S2") (status "passing") (elapsed-ms 162) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
-    (entry (id "S3") (status "passing") (elapsed-ms 767) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S3_h_theorem_binary.v") (semantic-check "verified"))
-    (entry (id "S4") (status "passing") (elapsed-ms 767) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
-    (entry (id "S5") (status "passing") (elapsed-ms 820) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S5_shannon_source_coding.v") (semantic-check "verified"))
-    (entry (id "E1") (status "passing") (elapsed-ms 805) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_1d.v") (semantic-check "verified"))
-    (entry (id "E2") (status "passing") (elapsed-ms 2647) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
-    (entry (id "E3") (status "passing") (elapsed-ms 154) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
-    (entry (id "E4") (status "passing") (elapsed-ms 2642) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
-    (entry (id "E5") (status "passing") (elapsed-ms 125) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E5_auth_key_binding.v") (semantic-check "verified"))
-    (entry (id "M6") (status "passing") (elapsed-ms 130) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
-    (entry (id "S6") (status "passing") (elapsed-ms 122) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
-    (entry (id "E6") (status "passing") (elapsed-ms 164) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E6_cstr_mass_balance.v") (semantic-check "verified"))
-    (entry (id "M7") (status "passing") (elapsed-ms 124) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M7_linearity_of_expectation.v") (semantic-check "verified"))
-    (entry (id "M8") (status "passing") (elapsed-ms 584) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
-    (entry (id "M9") (status "passing") (elapsed-ms 332) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
-    (entry (id "M10") (status "passing") (elapsed-ms 201) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M10_knot_composition_monoid.v") (semantic-check "verified"))
-    (entry (id "M11") (status "passing") (elapsed-ms 889) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
-    (entry (id "E7") (status "passing") (elapsed-ms 227) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
-    (entry (id "S7") (status "passing") (elapsed-ms 212) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S7_lorentz_velocity_addition.v") (semantic-check "verified"))
-    (entry (id "E8") (status "passing") (elapsed-ms 190) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
-    (entry (id "M12") (status "passing") (elapsed-ms 198) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
-    (entry (id "S8") (status "passing") (elapsed-ms 227) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
-    (entry (id "E9") (status "passing") (elapsed-ms 209) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
-    (entry (id "M13") (status "passing") (elapsed-ms 154) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
-    (entry (id "M14") (status "passing") (elapsed-ms 145) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M14_max_flow_min_cut.v") (semantic-check "verified"))
-    (entry (id "S9") (status "passing") (elapsed-ms 135) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
-    (entry (id "S10") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S10_r_naught_threshold.v") (semantic-check "verified"))
-    (entry (id "E10") (status "passing") (elapsed-ms 206) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
-    (entry (id "E11") (status "passing") (elapsed-ms 295) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
+    (entry (id "M1") (status "passing") (elapsed-ms 2684) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
+    (entry (id "M2") (status "passing") (elapsed-ms 1163) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
+    (entry (id "M3") (status "passing") (elapsed-ms 853) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
+    (entry (id "M4") (status "passing") (elapsed-ms 906) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M4_compactness_unit_interval.v") (semantic-check "verified"))
+    (entry (id "M5") (status "passing") (elapsed-ms 334) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
+    (entry (id "S1") (status "passing") (elapsed-ms 144) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
+    (entry (id "S2") (status "passing") (elapsed-ms 161) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
+    (entry (id "S3") (status "passing") (elapsed-ms 805) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S3_h_theorem_binary.v") (semantic-check "verified"))
+    (entry (id "S4") (status "passing") (elapsed-ms 763) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
+    (entry (id "S5") (status "passing") (elapsed-ms 861) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S5_shannon_source_coding.v") (semantic-check "verified"))
+    (entry (id "E1") (status "passing") (elapsed-ms 839) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_1d.v") (semantic-check "verified"))
+    (entry (id "E2") (status "passing") (elapsed-ms 2430) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
+    (entry (id "E3") (status "passing") (elapsed-ms 148) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
+    (entry (id "E4") (status "passing") (elapsed-ms 2676) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
+    (entry (id "E5") (status "passing") (elapsed-ms 129) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E5_auth_key_binding.v") (semantic-check "verified"))
+    (entry (id "M6") (status "passing") (elapsed-ms 132) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
+    (entry (id "S6") (status "passing") (elapsed-ms 129) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
+    (entry (id "E6") (status "passing") (elapsed-ms 163) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E6_cstr_mass_balance.v") (semantic-check "verified"))
+    (entry (id "M7") (status "passing") (elapsed-ms 123) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M7_linearity_of_expectation.v") (semantic-check "verified"))
+    (entry (id "M8") (status "passing") (elapsed-ms 613) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
+    (entry (id "M9") (status "passing") (elapsed-ms 340) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
+    (entry (id "M10") (status "passing") (elapsed-ms 152) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M10_knot_composition_monoid.v") (semantic-check "verified"))
+    (entry (id "M11") (status "passing") (elapsed-ms 632) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
+    (entry (id "E7") (status "passing") (elapsed-ms 122) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
+    (entry (id "S7") (status "passing") (elapsed-ms 117) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S7_lorentz_velocity_addition.v") (semantic-check "verified"))
+    (entry (id "E8") (status "passing") (elapsed-ms 122) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
+    (entry (id "M12") (status "passing") (elapsed-ms 118) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
+    (entry (id "S8") (status "passing") (elapsed-ms 159) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
+    (entry (id "E9") (status "passing") (elapsed-ms 119) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
+    (entry (id "M13") (status "passing") (elapsed-ms 121) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
+    (entry (id "M14") (status "passing") (elapsed-ms 122) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M14_max_flow_min_cut.v") (semantic-check "verified"))
+    (entry (id "S9") (status "passing") (elapsed-ms 117) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
+    (entry (id "S10") (status "passing") (elapsed-ms 132) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S10_r_naught_threshold.v") (semantic-check "verified"))
+    (entry (id "E10") (status "passing") (elapsed-ms 132) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
+    (entry (id "E11") (status "passing") (elapsed-ms 116) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
   ))