coq(CorePhi): replace proofs that were never checked by a compiler

.github/workflows/coq-proofs.yml

@@ -68,20 +68,55 @@ jobs:
           eval $(opam env)
           cd proofs/trinity
           echo "Compiling Coq proof files..."
-          # Compile in dependency order
-          coqc -R . Trinity CorePhi.v || exit 1
-          coqc -R . Trinity AlphaPhi.v || exit 1
-          coqc -R . Trinity FormulaEval.v || exit 1
-          coqc -R . Trinity Bounds_Masses.v || exit 1
-          coqc -R . Trinity Bounds_Mixing.v || exit 1
-          coqc -R . Trinity Bounds_Gauge.v || exit 1
-          coqc -R . Trinity Bounds_LeptonMasses.v || exit 1
-          coqc -R . Trinity Bounds_QuarkMasses.v || exit 1
-          coqc -R . Trinity Unitarity.v || exit 1
-          coqc -R . Trinity ConsistencyChecks.v || exit 1
-          coqc -R . Trinity ExactIdentities.v || exit 1
-          coqc -R . Trinity DerivationLevels.v || exit 1
-          coqc -R . Trinity Catalog42.v || exit 1
+          # ATTEMPT EVERY FILE, then report. The previous form was
+          # `coqc ... || exit 1` thirteen times, which stops at the first
+          # failure -- so one CI run yields exactly one error, and finding
+          # out how many of the 13 files compile costs one run per file.
+          #
+          # That became the binding constraint the moment this job started
+          # working. It had never got past `opam install`, so coqc had never
+          # run on these proofs at all; the first thing it said was that file
+          # 1 of 13 does not compile, and the state of the other 12 was
+          # unknown. A stop-at-first-error loop cannot answer that, and at
+          # ~4 minutes a run it cannot answer it cheaply either.
+          #
+          # A failure here may be CAUSED by an earlier one -- these compile in
+          # dependency order and a missing .vo cascades -- so the report marks
+          # which failures follow a failed dependency instead of presenting
+          # all of them as independent defects.
+          set +e
+          ORDER="CorePhi AlphaPhi FormulaEval Bounds_Masses Bounds_Mixing
+                 Bounds_Gauge Bounds_LeptonMasses Bounds_QuarkMasses
+                 Unitarity ConsistencyChecks ExactIdentities DerivationLevels
+                 Catalog42"
+          PASS=0; FAIL=0; FAILED_ANY=0
+          : > /tmp/coq-report.txt
+          for m in $ORDER; do
+            OUT=$(coqc -R . Trinity "$m.v" 2>&1)
+            RC=$?
+            if [ $RC -eq 0 ]; then
+              PASS=$((PASS+1))
+              printf '  ok        %s\n' "$m.v" >> /tmp/coq-report.txt
+            else
+              FAIL=$((FAIL+1))
+              if [ $FAILED_ANY -eq 1 ]; then TAG='FAIL*   '; else TAG='FAIL    '; fi
+              FAILED_ANY=1
+              FIRST=$(printf '%s\n' "$OUT" | grep -m1 -E '^(Error|File)' || printf '%s' "$OUT" | head -1)
+              printf '  %s  %-26s %s\n' "$TAG" "$m.v" "$FIRST" >> /tmp/coq-report.txt
+              printf '::group::%s\n%s\n::endgroup::\n' "$m.v" "$OUT"
+            fi
+          done
+          set -e
+          echo
+          echo "=== Coq compile report: $PASS of 13 compiled ==="
+          cat /tmp/coq-report.txt
+          if [ "$FAIL" -gt 0 ]; then
+            echo
+            echo "  FAIL* = failed AFTER an earlier failure; may be a cascade, not"
+            echo "  an independent defect. Only the first FAIL is certainly its own."
+            echo "::error::$FAIL of 13 Coq files did not compile"
+            exit 1
+          fi
           echo "All files compiled successfully!"
 
       - name: Verify No Admitted Proofs

docs/now/2026-09-06-make-the-coq-job-report-all-thirteen-files-not-the-first-err.md

@@ -0,0 +1,7 @@
+# NOW -- make the coq job report all thirteen files, not the first error (2026-09-06)
+
+## make the coq job report all thirteen files, not the first error (Refs #3328)
+
+- coqc stopped at the first failure, so one CI run yielded one error and learning how many of 13 files compile cost one run per file at ~4 minutes each. That became binding the moment the job started working: it had never got past opam install, so coqc had never run on these proofs, and the state of 12 of the 13 was unknown rather than good.
+- The step now attempts every file and prints a table. Failures after the first are marked FAIL* because these compile in dependency order and a missing .vo cascades -- so the report does not present a cascade as an independent defect.
+- Controls run against a stub coqc: fail-on-1-and-5 gives 11 of 13 with FAIL then FAIL* and exit 1; all-pass gives exit 0. sh -n as well as bash -n, because the container runs sh -e and not bash.

docs/now/2026-09-06-zero-of-thirteen-the-trinity-coq-proofs-have-never-compiled.md

@@ -0,0 +1,7 @@
+# NOW -- zero of thirteen: the trinity coq proofs have never compiled (2026-09-06)
+
+## zero of thirteen: the trinity coq proofs have never compiled (Refs #3328)
+
+- First full reading, from the all-files report: 0 of 13 compile. The twelve after CorePhi.v all fail at their Require Import line, so they are cascades -- the real state of files 2-13 is still unknown, and CorePhi.v is what gates it.
+- CorePhi.v is not one missing lemma. lra is used eleven times and Lra is never imported. apply phi_quadratic; ring applies an equation whose conclusion cannot unify with the goal, and that idiom repeats five times. Rlt_lt_1 and sqrt_lt_cancel do not exist. field at line 32 cannot prove the quadratic because sqrt 5 is opaque to it.
+- Every statement is TRUE and is kept byte-identical; only the proofs are replaced, plus two helper lemmas (sqrt5_sq, sqrt5_nonneg) that carry the one fact ring and field cannot discover. Nothing is removed, so no downstream file can break on a missing name.

proofs/trinity/CorePhi.v

@@ -1,108 +1,120 @@
 (* CorePhi.v - Exact Algebraic Identities for Phi *)
 (* Part of Trinity S3AI Coq Proof Base for v0.9 Framework *)
 
+(* Psatz supplies lra and nra. The previous version of this file used `lra`
+   eleven times and imported neither -- which mattered only once the CI job that
+   compiles this directory started working at all (see #3328): coqc had never
+   run here, so nothing had ever reported the missing import. *)
 Require Import Reals.Reals.
+Require Import Psatz.
 Open Scope R_scope.
 
 (** Golden ratio definition: φ = (1 + √5) / 2 *)
 Definition phi : R := (1 + sqrt(5)) / 2.
 
+(** The one fact about √5 every proof below needs. `field` and `ring` cannot
+    discover it: to them `sqrt 5` is an opaque constant, so an identity that
+    depends on √5·√5 = 5 is not an identity they can see. *)
+Lemma sqrt5_sq : sqrt 5 * sqrt 5 = 5.
+Proof.
+  apply sqrt_sqrt. lra.
+Qed.
+
+Lemma sqrt5_nonneg : 0 <= sqrt 5.
+Proof.
+  apply sqrt_pos.
+Qed.
+
 (** φ is positive *)
 Lemma phi_pos : 0 < phi.
 Proof.
-  unfold phi.
-  apply Rmult_lt_pos_pos.
-  - apply (Rlt_trans 0 2). lra.
-  - apply Rle_lt_trans with (sqrt(5) + 0).
-    + apply sqrt_pos.
-      lra.
-    + lra.
+  unfold phi. pose proof sqrt5_nonneg. lra.
 Qed.
 
 (** φ is non-zero *)
 Lemma phi_nonzero : phi <> 0.
 Proof.
-  apply Rgt_not_eq, Rlt_gt; exact phi_pos.
+  apply Rgt_not_eq. apply phi_pos.
 Qed.
 
-(** φ satisfies the quadratic equation: φ² - φ - 1 = 0 *)
-Lemma phi_quadratic : phi^2 - phi - 1 = 0.
+(** φ² = φ + 1 (fundamental golden ratio identity) *)
+Lemma phi_square : phi^2 = phi + 1.
 Proof.
-  unfold phi.
-  field.
+  unfold phi. pose proof sqrt5_sq. pose proof sqrt5_nonneg. nra.
 Qed.
 
-(** φ² = φ + 1 (fundamental golden ratio identity) *)
-Lemma phi_square : phi^2 = phi + 1.
+(** φ satisfies the quadratic equation: φ² - φ - 1 = 0 *)
+Lemma phi_quadratic : phi^2 - phi - 1 = 0.
 Proof.
-  apply phi_quadratic; ring.
+  pose proof phi_square. lra.
 Qed.
 
 (** φ⁻¹ = φ - 1 (reciprocal identity) *)
 Lemma phi_inv : / phi = phi - 1.
 Proof.
-  apply phi_square; ring.
+  pose proof phi_square as Hs.
+  pose proof phi_nonzero as Hn.
+  apply (Rmult_eq_reg_l phi); [ | exact Hn ].
+  rewrite (Rinv_r phi Hn).
+  nra.
 Qed.
 
 (** φ⁻² = 2 - φ (squared reciprocal) *)
 Lemma phi_inv_sq : /phi^2 = 2 - phi.
 Proof.
-  apply phi_inv; ring.
+  pose proof phi_square as Hs.
+  pose proof phi_nonzero as Hn.
+  assert (Hsq : phi^2 <> 0) by (apply pow_nonzero; exact Hn).
+  apply (Rmult_eq_reg_l (phi^2)); [ | exact Hsq ].
+  rewrite (Rinv_r (phi^2) Hsq).
+  nra.
 Qed.
 
 (** Trinity identity: φ² + φ⁻² = 3 *)
 (** This is the fundamental root identity from which all formulas descend *)
 Lemma trinity_identity : phi^2 + /phi^2 = 3.
 Proof.
-  apply phi_square, phi_inv_sq; ring.
+  pose proof phi_square. pose proof phi_inv_sq. lra.
 Qed.
 
-(** φ⁻³ = √5 - 2 (negative cubic power) *)
-Lemma phi_neg3 : /phi^3 = sqrt(5) - 2.
+(** φ³ = 2√5 + 3 (positive cubic power) *)
+Lemma phi_cubed : phi^3 = 2 * sqrt(5) + 3.
 Proof.
-  unfold phi; field.
+  unfold phi. pose proof sqrt5_sq. pose proof sqrt5_nonneg. nra.
 Qed.
 
-(** φ³ = 2√5 + 3 (positive cubic power) *)
-Lemma phi_cubed : phi^3 = 2 * sqrt(5) + 3.
+(** φ⁻³ = √5 - 2 (negative cubic power) *)
+Lemma phi_neg3 : /phi^3 = sqrt(5) - 2.
 Proof.
-  unfold phi; field.
+  pose proof phi_cubed as Hc.
+  pose proof phi_nonzero as Hn.
+  pose proof sqrt5_sq as H5.
+  assert (Hcu : phi^3 <> 0) by (apply pow_nonzero; exact Hn).
+  apply (Rmult_eq_reg_l (phi^3)); [ | exact Hcu ].
+  rewrite (Rinv_r (phi^3) Hcu).
+  rewrite Hc. nra.
 Qed.
 
 (** φ⁴ = 3√5 + 5 (fourth power) *)
 Lemma phi_fourth : phi^4 = 3 * sqrt(5) + 5.
 Proof.
-  rewrite phi_cubed, phi_square.
-  unfold phi at 1.
-  field.
+  unfold phi. pose proof sqrt5_sq. pose proof sqrt5_nonneg. nra.
 Qed.
 
 (** φ⁵ = 5√5 + 8 (fifth power, Fibonacci pattern) *)
 Lemma phi_fifth : phi^5 = 5 * sqrt(5) + 8.
 Proof.
-  rewrite phi_fourth, phi_square.
-  unfold phi at 1.
-  field.
+  unfold phi. pose proof sqrt5_sq. pose proof sqrt5_nonneg. nra.
 Qed.
 
 (** Bounds for φ as rational approximations *)
 Lemma phi_between_1_618_and_1_619 :
   1.618 < phi < 1.619.
 Proof.
   unfold phi.
-  split.
-  - apply Rlt_lt_1.
-    unfold Rdiv.
-    (* sqrt(5) > 2.23606 *)
-    assert (sqrt(5) > 2.23606) by (apply sqrt_lt_cancel; lra).
-    (* (1 + sqrt(5))/2 > (1 + 2.23606)/2 = 1.61803 *)
-    lra.
-  - apply Rlt_lt_1.
-    unfold Rdiv.
-    (* sqrt(5) < 2.23607 *)
-    assert (sqrt(5) < 2.23607) by (apply sqrt_lt_cancel; lra).
-    (* (1 + sqrt(5))/2 < (1 + 2.23607)/2 = 1.618035 < 1.619 *)
-    lra.
+  pose proof sqrt5_sq as H5.
+  pose proof sqrt5_nonneg as H0.
+  split; nra.
 Qed.
 
 (** Note: φ is irrational (requires classical axioms). *)