diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml index a172c711c2..fe88a2a087 100644 --- a/.github/workflows/coq-proofs.yml +++ b/.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 diff --git a/docs/now/2026-09-06-make-the-coq-job-report-all-thirteen-files-not-the-first-err.md b/docs/now/2026-09-06-make-the-coq-job-report-all-thirteen-files-not-the-first-err.md new file mode 100644 index 0000000000..3cbbd976cd --- /dev/null +++ b/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. diff --git a/docs/now/2026-09-06-zero-of-thirteen-the-trinity-coq-proofs-have-never-compiled.md b/docs/now/2026-09-06-zero-of-thirteen-the-trinity-coq-proofs-have-never-compiled.md new file mode 100644 index 0000000000..1d40342928 --- /dev/null +++ b/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. diff --git a/proofs/trinity/CorePhi.v b/proofs/trinity/CorePhi.v index 7519f58533..bbcb9a7896 100644 --- a/proofs/trinity/CorePhi.v +++ b/proofs/trinity/CorePhi.v @@ -1,88 +1,110 @@ (* 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 *) @@ -90,19 +112,9 @@ 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). *)