diff --git a/proofs/trinity/Bounds_QuarkMasses.v b/proofs/trinity/Bounds_QuarkMasses.v index 5373302a..c7b0322c 100644 --- a/proofs/trinity/Bounds_QuarkMasses.v +++ b/proofs/trinity/Bounds_QuarkMasses.v @@ -3,6 +3,7 @@ Require Import Reals.Reals. Require Import Interval.Tactic. +Require Import Lra. Open Scope R_scope. Require Import CorePhi. @@ -22,21 +23,49 @@ Definition tolerance_SG : R := 10 / 10000. (* 0.01% for smoking guns *) Definition Q03_theoretical : R := (phi ^ 4) * PI / (exp 1 ^ 2). Definition Q03_experimental : R := 171.5. +(* R8 falsification — PDG 2024: m_c/m_d ~ 171.5. + Numerical: phi^4 * pi / e^2 ~= (3 sqrt 5 + 5) * pi / e^2 + ~= 6.854 * 3.142 / 7.389 + ~= 2.914 + |2.914 - 171.5| / 171.5 ~= 0.983 + tolerance_V = 1/100, so 0.983 > 0.01. FALSIFIED. *) +Theorem Q03_falsified_by_PDG : + Rabs (Q03_theoretical - Q03_experimental) / Q03_experimental > tolerance_V. +Proof. + unfold Q03_theoretical, Q03_experimental, tolerance_V. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + Theorem Q03_within_tolerance : - Rabs (Q03_theoretical - Q03_experimental) / Q03_experimental < tolerance_V. + ~ Rabs (Q03_theoretical - Q03_experimental) / Q03_experimental < tolerance_V. +Proof. + pose proof Q03_falsified_by_PDG as Hf. intros Hlt. lra. +Qed. + +(* The monomial form would require: (i) a witness monomial m whose eval + equals Q03_theoretical, and (ii) the within-tolerance bound on m. + By Q03_falsified_by_PDG, condition (ii) is impossible for any such m + (substituting eval_monomial m = Q03_theoretical into the within-bound + gives the same Rabs > tolerance_V). Therefore the existential is + FALSE; we prove its negation. *) +Theorem Q03_monomial_form_falsified : + ~ (exists m : monomial, + eval_monomial m = Q03_theoretical + /\ Rabs (eval_monomial m - Q03_experimental) / Q03_experimental < tolerance_V). Proof. - (* TODO: Q03 formula does not match experimental value (98% error) *) - admit. -Admitted. + intros [m [Heq Hlt]]. + pose proof Q03_falsified_by_PDG as Hf. + rewrite Heq in Hlt. lra. +Qed. +(* Restated theorem name (kept for downstream references) — its content + is now the negation; proved trivially from Q03_monomial_form_falsified. *) Theorem Q03_monomial_form : - exists m : monomial, - eval_monomial m = Q03_theoretical - /\ Rabs (eval_monomial m - Q03_experimental) / Q03_experimental < tolerance_V. -Proof. - (* TODO: Depends on admitted eval_monomial for Rocq 9.x compatibility *) - admit. -Admitted. + ~ (exists m : monomial, + eval_monomial m = Q03_theoretical + /\ Rabs (eval_monomial m - Q03_experimental) / Q03_experimental < tolerance_V). +Proof. exact Q03_monomial_form_falsified. Qed. (** ====================================================================== *) (** Q05: m_b/m_s = 48·e²/φ⁴ ≈ 52.3 [IMPROVED via Chimera] *) @@ -48,22 +77,39 @@ Admitted. Definition Q05_theoretical : R := 48 * (exp 1 ^ 2) / (phi ^ 4). Definition Q05_experimental : R := 52.3. +(* R8 falsification (BARELY) — Q05 candidate from Chimera v1.0: + 48 e^2 / phi^4 ~= 48 * 7.389 / 6.854 ~= 51.747 + |51.747 - 52.3| / 52.3 ~= 0.01058 + tolerance_V = 1/100 = 0.01. 0.01058 > 0.01 -> falsified by ~6 ppt. *) +Theorem Q05_falsified_by_PDG : + Rabs (Q05_theoretical - Q05_experimental) / Q05_experimental > tolerance_V. +Proof. + unfold Q05_theoretical, Q05_experimental, tolerance_V. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + Theorem Q05_within_tolerance : - Rabs (Q05_theoretical - Q05_experimental) / Q05_experimental < tolerance_V. + ~ Rabs (Q05_theoretical - Q05_experimental) / Q05_experimental < tolerance_V. +Proof. + pose proof Q05_falsified_by_PDG as Hf. intros Hlt. lra. +Qed. + +Theorem Q05_monomial_form_falsified : + ~ (exists m : monomial, + eval_monomial m = Q05_theoretical + /\ Rabs (eval_monomial m - Q05_experimental) / Q05_experimental < tolerance_V). Proof. - (* TODO: Q05 is a CANDIDATE formula (Δ≈1%, outside 0.1% tolerance) *) - (* Chimera v1.0 result: 48·e²/φ⁴ = 51.75 vs experimental 52.3 *) - admit. -Admitted. + intros [m [Heq Hlt]]. + pose proof Q05_falsified_by_PDG as Hf. + rewrite Heq in Hlt. lra. +Qed. Theorem Q05_monomial_form : - exists m : monomial, - eval_monomial m = Q05_theoretical - /\ Rabs (eval_monomial m - Q05_experimental) / Q05_experimental < tolerance_V. -Proof. - (* TODO: Depends on admitted eval_monomial for Rocq 9.x compatibility *) - admit. -Admitted. + ~ (exists m : monomial, + eval_monomial m = Q05_theoretical + /\ Rabs (eval_monomial m - Q05_experimental) / Q05_experimental < tolerance_V). +Proof. exact Q05_monomial_form_falsified. Qed. (** ====================================================================== *) (** Q06: m_b/m_d = Q05 × Q07 = 1034.93 [CHAIN VERIFIED] *) diff --git a/proofs/trinity/ConsistencyChecks.v b/proofs/trinity/ConsistencyChecks.v index 4385e4a1..a9e86e07 100644 --- a/proofs/trinity/ConsistencyChecks.v +++ b/proofs/trinity/ConsistencyChecks.v @@ -3,6 +3,7 @@ Require Import Reals.Reals. Require Import Interval.Tactic. +Require Import Lra. Open Scope R_scope. Require Import CorePhi. @@ -25,17 +26,22 @@ Definition tolerance_SG : R := 10 / 10000. (* 0.01% for smoking guns *) Definition alpha_from_G01 : R := 1 / (4 * 9 * /PI * phi * (exp 1 ^ 2)). -Theorem alpha_consistency_check : - Rabs (alpha_from_G01 - alpha_phi) / alpha_phi < tolerance_SG. +(* R8 falsification — numerical: + 1/G01 = pi/(36 phi e^2) ~= 0.007299 + alpha_phi = (sqrt 5 - 2)/2 ~= 0.118034 + |0.007299 - 0.118034| / 0.118034 ~= 0.938 >> 1e-3 = tolerance_SG. + The two definitions disagree by ~94% — they cannot both hold. *) +Theorem alpha_consistency_falsified : + Rabs (alpha_from_G01 - alpha_phi) / alpha_phi > tolerance_SG. Proof. unfold alpha_from_G01, alpha_phi, tolerance_SG. - (* α_φ = 1/G01 should hold exactly if formulas are consistent *) - (* G01 = 4·9·π⁻¹·φ·e² = 36φe²/π *) - (* α_φ = 1/G01 = π/(36φe²) *) - (* α_φ = (√5-2)/2 from definition *) - (* TODO: Verify numerically with higher precision *) - admit. -Admitted. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +Theorem alpha_consistency_check : + ~ Rabs (alpha_from_G01 - alpha_phi) / alpha_phi < tolerance_SG. +Proof. pose proof alpha_consistency_falsified. intros Hlt. lra. Qed. (** ====================================================================== *) (** Quark Mass Chain Relations *) @@ -46,38 +52,39 @@ Admitted. (* Q07 × Q01⁻¹ should ≈ Q02 *) (* Note: Q02 is m_s/m_u, Q01 is m_u/m_d, so: Q07 / Q01 = Q02 *) -Theorem quark_mass_chain_Q07_Q01_Q02 : - Rabs ((Q07_theoretical / Q01_theoretical) - Q02_theoretical) / Q02_theoretical < tolerance_L. +(* R8 falsification — Q07/Q01 = 216 phi^2 e^2 / pi^2 ~= 423.4, + Q02 = 4 phi^2 / pi ~= 3.33, rel err ~= 126 (12600%). + Chain relation with current candidate formulas is fundamentally + broken — see file footer FAILING checks list. *) +Theorem quark_mass_chain_Q07_Q01_Q02_falsified : + Rabs ((Q07_theoretical / Q01_theoretical) - Q02_theoretical) / Q02_theoretical > tolerance_L. Proof. unfold Q07_theoretical, Q01_theoretical, Q02_theoretical, tolerance_L. - (* Q07 = 8·3·π⁻¹·φ² = 24φ²/π *) - (* Q01 = π/(9·e²) *) - (* Q02 = 4·φ²/π *) - (* Q07 / Q01 = (24φ²/π) / (π/(9e²)) = 24φ²/π · 9e²/π = 216φ²e²/π² *) - (* Q02 = 4φ²/π *) - (* Check: 216φ²e²/π² ≈ 4φ²/π *) - (* This would require 54e²/π ≈ 1, which is false *) - (* So the chain relation suggests these formulas may need revision *) - admit. -Admitted. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +Theorem quark_mass_chain_Q07_Q01_Q02 : + ~ Rabs ((Q07_theoretical / Q01_theoretical) - Q02_theoretical) / Q02_theoretical < tolerance_L. +Proof. pose proof quark_mass_chain_Q07_Q01_Q02_falsified. intros H'. lra. Qed. (* Chain 2: (m_b/m_s) × (m_s/m_d) = m_b/m_d *) (* Q05 × Q07 = Q06 [VERIFIED via Chimera v1.0] *) (* Q05 = 48·e²/φ⁴, Q07 = 24φ²/π, Q06 = Q05 × Q07 = 1034.93 *) (* Error: 0.01% - chain relation VERIFIED! *) +(* PROVEN — exact by definition: Q06_theoretical := Q05 * Q07, + so the difference is identically 0 and Rabs 0 / x = 0 < tolerance_SG. *) Theorem quark_mass_chain_Q05_Q07_Q06 : Rabs ((Q05_theoretical * Q07_theoretical) - Q06_theoretical) / Q06_theoretical < tolerance_SG. Proof. - unfold Q05_theoretical, Q07_theoretical, Q06_theoretical, tolerance_SG. - (* With Chimera v1.0 formulas: *) - (* Q05 = 48·e²/φ⁴ *) - (* Q07 = 8·3·π⁻¹·φ² = 24φ²/π *) - (* Q06 = Q05 × Q07 (chain definition) *) - (* This should be exact by definition in Bounds_QuarkMasses.v *) - (* But we verify numerically for robustness *) - admit. -Admitted. + unfold Q06_theoretical at 1, tolerance_SG. + replace (Q05_theoretical * Q07_theoretical - Q05_theoretical * Q07_theoretical) + with 0 by lra. + rewrite Rabs_R0. + unfold Rdiv. rewrite Rmult_0_l. + lra. +Qed. Theorem quark_mass_chain_Q05_Q07_Q06_exact : (* Exact chain relation: Q06 is defined as Q05 × Q07 *) @@ -125,17 +132,20 @@ Qed. (* Note: H01_H02_H03_chain is a conceptual relation, not a Coq definition *) -Theorem gauge_mass_chain_check : - Rabs ((H02_theoretical * 0.881) - H03_theoretical) / H03_theoretical < tolerance_V. +(* R8 falsification — H02 * 0.881 ~= 15.50 vs H03 ~= 7.12, + |15.50 - 7.12| / 7.12 ~= 1.18 >> 0.01. Chain relation does not hold; + m_W/m_Z is not the simple ratio assumed in the original theorem. *) +Theorem gauge_mass_chain_falsified : + Rabs ((H02_theoretical * 0.881) - H03_theoretical) / H03_theoretical > tolerance_V. Proof. unfold H02_theoretical, H03_theoretical, tolerance_V. - (* H02 = 4φe ≈ 4 × 1.618 × 2.718 ≈ 17.59 *) - (* H03 = φ²e ≈ 2.618 × 2.718 ≈ 7.12 *) - (* H02 × 0.881 ≈ 17.59 × 0.881 ≈ 15.50 *) - (* This doesn't equal 7.12 - chain relation fails *) - (* This suggests m_W/m_Z is not given by simple ratio *) - admit. -Admitted. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +Theorem gauge_mass_chain_check : + ~ Rabs ((H02_theoretical * 0.881) - H03_theoretical) / H03_theoretical < tolerance_V. +Proof. pose proof gauge_mass_chain_falsified. intros H'. lra. Qed. (** ====================================================================== *) (** CKM Unitarity Consistency *) @@ -153,23 +163,35 @@ Definition V_ud_from_unitarity_trinity := Definition V_ud_experimental : R := 0.974. +(* PROVEN — sqrt(1 - C01^2 - C03^2) ~= 0.97433, exp = 0.974, + rel err ~= 0.00034 < 0.01. Pure interval arithmetic. *) Theorem V_ud_unitarity_check : Rabs (V_ud_from_unitarity_trinity - V_ud_experimental) / V_ud_experimental < tolerance_V. Proof. - unfold V_ud_from_unitarity_trinity, V_ud_experimental, tolerance_V, C01_theoretical, C03_theoretical. - (* Compute: sqrt(1 - (2·3⁻²·π⁻³·φ³·e²)² - (4·3⁻⁴·π⁻³·φ·e²)²) *) - (* TODO: C01 and C03 formulas need Chimera search *) - admit. -Admitted. + unfold V_ud_from_unitarity_trinity, V_ud_experimental, tolerance_V, + C01_theoretical, C03_theoretical. + unfold phi. + interval with (i_bisect, i_bits). +Qed. +(* PROVEN — by Rsqr_sqrt : 0 <= x -> sqrt x ^ 2 = x, + the LHS reduces to Rabs 0 = 0 < 1e-6. *) Theorem CKM_row_unitarity_sum : Rabs (V_ud_from_unitarity_trinity^2 + C01_theoretical^2 + C03_theoretical^2 - 1) < 1e-6. Proof. - unfold V_ud_from_unitarity_trinity, C01_theoretical, C03_theoretical. - (* This should be exact by definition *) - (* V_ud = sqrt(1 - C01^2 - C03^2), so V_ud^2 + C01^2 + C03^2 = 1 *) - admit. -Admitted. + unfold V_ud_from_unitarity_trinity. + (* Show 1 - C01^2 - C03^2 >= 0 so sqrt^2 collapses cleanly. *) + assert (Hpos : 0 <= 1 - C01_theoretical^2 - C03_theoretical^2). + { unfold C01_theoretical, C03_theoretical. unfold phi. + interval with (i_bisect, i_bits). } + assert (Hsq : (sqrt (1 - C01_theoretical^2 - C03_theoretical^2))^2 + = 1 - C01_theoretical^2 - C03_theoretical^2). + { rewrite <- Rsqr_pow2. rewrite Rsqr_sqrt by exact Hpos. reflexivity. } + rewrite Hsq. + replace (1 - C01_theoretical^2 - C03_theoretical^2 + C01_theoretical^2 + + C03_theoretical^2 - 1) with 0 by lra. + rewrite Rabs_R0. lra. +Qed. (** ====================================================================== *) (** PMNS Unitarity Consistency *) @@ -185,15 +207,26 @@ Admitted. Definition PM2_sin2_theta13 : R := 3 * PI / (phi ^ 3) / 100. (* Note: PM2 formula needs verification *) -Theorem PMNS_sum_to_one : - Rabs (N01_theoretical + PM2_sin2_theta13 + (1 - N03_theoretical) - 1) < tolerance_V. +(* R8 falsification — numerical: + N01 = 8 pi / (phi^5 e^2) ~= 0.30670 + PM2 = 3 pi / (100 phi^3) ~= 0.02225 + 1 - N03 = 1 - 2 pi / phi^4 ~= 0.08330 + sum ~= 0.41225 (vs 1.0) + |sum - 1| ~= 0.58775 >> 0.01. + Source of failure is the candidate N03 formula (gives 0.917 vs + experimental 0.548) — already flagged in file footer. PMNS row-sum + identity does NOT hold under current Chimera v1.0 formulas. *) +Theorem PMNS_sum_to_one_falsified : + Rabs (N01_theoretical + PM2_sin2_theta13 + (1 - N03_theoretical) - 1) > tolerance_V. Proof. unfold N01_theoretical, N03_theoretical, PM2_sin2_theta13, tolerance_V. - (* PMNS unitarity: sin²(θ_12) + sin²(θ_13) + cos²(θ_23) = 1 *) - (* Using N03 = sin²(θ_23), so cos²(θ_23) = 1 - N03 *) - (* TODO: N03 formula needs Chimera search *) - admit. -Admitted. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +Theorem PMNS_sum_to_one : + ~ Rabs (N01_theoretical + PM2_sin2_theta13 + (1 - N03_theoretical) - 1) < tolerance_V. +Proof. pose proof PMNS_sum_to_one_falsified. intros H'. lra. Qed. (** ====================================================================== *) (** Cross-Sector Consistency: α_s Running *) diff --git a/proofs/trinity/ExactIdentities.v b/proofs/trinity/ExactIdentities.v index c991d3b2..d819f8b1 100644 --- a/proofs/trinity/ExactIdentities.v +++ b/proofs/trinity/ExactIdentities.v @@ -1,13 +1,106 @@ (* ExactIdentities.v - Exact Algebraic Identities and Number Theory *) (* Part of Trinity S3AI Coq Proof Base for v0.9 Framework *) +(* L-COQ47 sweep-1 (issue #549): 7 Admitted → Proven, 4 blocked with R8 witnesses *) +(* Anchor: φ² + φ⁻² = 3 · DOI 10.5281/zenodo.19227877 *) Require Import Reals.Reals. Require Import ZArith. Require Import Arith. +Require Import Lra. +Require Import Lia. Open Scope R_scope. Require Import CorePhi. +(** ====================================================================== *) +(** Local helpers — inlined to avoid depending on un-CI-tested CorePhi aux *) +(** ====================================================================== *) + +(* witness: sqrt 5 * sqrt 5 = 5 by Coq.Reals.sqrt_sqrt with 0 ≤ 5 *) +Lemma exid_sqrt5_sq : sqrt 5 * sqrt 5 = 5. +Proof. apply sqrt_sqrt; lra. Qed. + +(* witness: phi^2 = phi + 1 derived independently of CorePhi.phi_square *) +Lemma exid_phi_sq : phi^2 = phi + 1. +Proof. + unfold phi, pow. rewrite Rmult_1_r. + pose proof exid_sqrt5_sq. field_simplify. nra. +Qed. + +(* witness: phi > 0 (since sqrt 5 ≥ 0 ⟹ (1+sqrt 5)/2 ≥ 1/2 > 0) *) +Lemma exid_phi_pos : 0 < phi. +Proof. unfold phi. pose proof (sqrt_pos 5). lra. Qed. + +(* witness: phi ≠ 0 (consequence of phi > 0) *) +Lemma exid_phi_nz : phi <> 0. +Proof. pose proof exid_phi_pos. lra. Qed. + +(* witness: /phi = phi - 1 (from phi^2 = phi+1 and phi≠0) *) +Lemma exid_phi_inv : / phi = phi - 1. +Proof. + apply (Rmult_eq_reg_l phi); [| exact exid_phi_nz]. + rewrite Rinv_r by exact exid_phi_nz. + pose proof exid_phi_sq. unfold pow in *. rewrite Rmult_1_r in *. nra. +Qed. + +(* witness: phi^2 ≠ 0 (phi>0 ⟹ phi*phi>0) *) +Lemma exid_phi_sq_nz : phi^2 <> 0. +Proof. unfold pow. rewrite Rmult_1_r. pose proof exid_phi_pos. nra. Qed. + +(* witness: /phi^2 = 2 - phi by (/phi^2)*phi^2 = 1 and phi^2=phi+1 *) +Lemma exid_phi_inv_sq : / phi^2 = 2 - phi. +Proof. + apply (Rmult_eq_reg_l (phi^2)); [| exact exid_phi_sq_nz]. + rewrite Rinv_r by exact exid_phi_sq_nz. + rewrite exid_phi_sq. + unfold phi. pose proof exid_sqrt5_sq. field_simplify. nra. +Qed. + +(* witness: phi^2 + /phi^2 = (phi+1) + (2-phi) = 3 — Trinity anchor *) +Lemma exid_trinity_identity : phi^2 + / phi^2 = 3. +Proof. pose proof exid_phi_sq. pose proof exid_phi_inv_sq. lra. Qed. + +(* witness: phi^3 = phi * phi^2 = phi*(phi+1) = 2*phi+1 = 2*((1+√5)/2)+1 = 2+√5 *) +Lemma exid_phi_cubed : phi^3 = 2 + sqrt 5. +Proof. + assert (H : phi^3 = phi * phi^2) by (unfold pow; ring). + rewrite H, exid_phi_sq. + unfold phi. pose proof exid_sqrt5_sq. field_simplify. nra. +Qed. + +(* witness: /phi^3 = sqrt 5 - 2 since (2+√5)(√5-2) = 5 - 4 = 1 *) +Lemma exid_phi_neg3 : / phi^3 = sqrt 5 - 2. +Proof. + apply (Rmult_eq_reg_l (phi^3)). + - rewrite Rinv_r. + + rewrite exid_phi_cubed. pose proof exid_sqrt5_sq. nra. + + rewrite exid_phi_cubed. pose proof (sqrt_pos 5). nra. + - rewrite exid_phi_cubed. pose proof (sqrt_pos 5). nra. +Qed. + +(* witness: phi^4 = phi^2 * phi^2 = (phi+1)^2 = phi^2+2phi+1 = 3*phi+2 *) +Lemma exid_phi_fourth : phi^4 = 3 * phi + 2. +Proof. + assert (H : phi^4 = phi^2 * phi^2) by (unfold pow; ring). + rewrite H. pose proof exid_phi_sq. nra. +Qed. + +(* witness: phi^4 ≠ 0 *) +Lemma exid_phi_4_nz : phi^4 <> 0. +Proof. + assert (H : phi^4 = phi^2 * phi^2) by (unfold pow; ring). + rewrite H. apply Rmult_integral_contrapositive. + split; exact exid_phi_sq_nz. +Qed. + +(* witness: /phi^4 = 5 - 3*phi since (3*phi+2)(5-3*phi) ... simplify via phi^2=phi+1 *) +Lemma exid_phi_inv_4 : / phi^4 = 5 - 3 * phi. +Proof. + apply (Rmult_eq_reg_l (phi^4)); [| exact exid_phi_4_nz]. + rewrite Rinv_r by exact exid_phi_4_nz. + rewrite exid_phi_fourth. pose proof exid_phi_sq. nra. +Qed. + (** ====================================================================== *) (** Lucas Closure Theorem *) (** Statement: For all n ∈ ℕ, φ^(2n) + φ^(-2n) is an integer *) @@ -20,59 +113,172 @@ Definition lucas_phi (n : nat) : R := (** Base cases for induction *) +(* witness: phi^0 = 1, /1 = 1, 1 + 1 = 2 (by Coq.Reals pow_O and Rinv_1) *) Lemma lucas_phi_0 : lucas_phi 0 = 2. Proof. - unfold lucas_phi. - simpl. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + unfold lucas_phi, pow. rewrite Rinv_1. lra. +Qed. + +(** DELETED per queen ruling on #549 (issuecomment-4405990351): the claim + `lucas_phi 1 = 3` is FALSE AS STATED (actual value = sqrt 5, because + /phi = -psi inverts the sign on odd powers). No anchor-aligned restatement + preserves the intended Lucas interpretation without redefining `lucas_phi` + (see R8 witness in git history commit 2929dbdb for the full falsification). + The PhD monograph relies on `lucas_sqrt5_integer` and `lucas_closure_even_powers` + (both Qed in this file), neither of which references the odd-index lemmas. + R5 §honest-status: REMOVE > paper over with Admitted. *) + +(** Queen-ratified restatement (verdict on #549): the original claim + `lucas_phi 2 = IZR 7` was numerically wrong (7 is L_4, not L_2) AND + actively contradicted the Trinity anchor φ² + φ⁻² = 3 on which the + entire framework rests. Restated to `= 3` per queen decision during + Rehearsal #2. The pre-sweep text is archived in git history for audit. *) + +(* witness: phi^2 + /phi^2 = (phi+1) + (2-phi) = 3 via exid_trinity_identity. + Falsification witness for the OLD `= 7` claim: exid_sqrt5_sq gives + sqrt 5 * sqrt 5 = 5, so phi^2 = (1+√5)^2/4 = (6+2√5)/4 = (3+√5)/2, + /phi^2 = 2 - phi = (3 - √5)/2, sum = 3 ≠ 7. Anchor: φ² + φ⁻² = 3. *) +Lemma lucas_phi_2 : lucas_phi 2 = 3. +Proof. + unfold lucas_phi. exact exid_trinity_identity. +Qed. + +(** L_4 = 7: φ⁴ + φ⁻⁴ = 7 — TRUE: (3*phi+2) + (5-3*phi) = 7. *) -Lemma lucas_phi_1 : lucas_phi 1 = 3. +(* witness: phi^4 + /phi^4 = (3*phi+2) + (5-3*phi) = 7 *) +Lemma lucas_phi_4 : lucas_phi 4 = 7. Proof. unfold lucas_phi. - simpl. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + pose proof exid_phi_fourth. pose proof exid_phi_inv_4. lra. +Qed. + +(** DELETED per queen ruling on #549 (issuecomment-4405990351): the recurrence + `lucas_phi (n + 2) = lucas_phi (S n) + lucas_phi n` is FALSE AS STATED + (counter-witness n=0: lp(2)=3, lp(1)+lp(0)=sqrt 5 + 2, and 3 ≠ sqrt 5 + 2). + The Lucas recurrence holds for L_n = phi^n + psi^n, which equals + `lucas_phi n = phi^n + /phi^n` only on EVEN n (/phi = -psi inverts sign on + odd powers). Even-index closure is already proven by `lucas_closure_even_powers`; + general-index recurrence requires redefining `lucas_phi` via signed Binet, + which is structural change out of scope. R8 witness preserved in commit 2929dbdb. *) -Lemma lucas_phi_2 : lucas_phi 2 = IZR 7. +(** ====================================================================== *) +(** Lucas Closure: Even powers of φ sum to integers *) +(** ====================================================================== *) + +(* Define ψ = (1 - √5) / 2 = 1 - φ = -1/φ for use in the Binet proof *) +Definition psi : R := (1 - sqrt 5) / 2. + +(* witness: psi also satisfies x^2 = x + 1, by direct expansion using sqrt 5 * sqrt 5 = 5 *) +Lemma exid_psi_sq : psi^2 = psi + 1. Proof. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + unfold psi, pow. rewrite Rmult_1_r. + pose proof exid_sqrt5_sq. field_simplify. nra. +Qed. -(** L_4 = 7: φ⁴ + φ⁻⁴ = 7 *) +(* witness: phi*psi = ((1+√5)/2) * ((1-√5)/2) = (1-5)/4 = -1 *) +Lemma exid_phi_psi_prod : phi * psi = -1. +Proof. + unfold phi, psi. pose proof exid_sqrt5_sq. field_simplify. nra. +Qed. -Lemma lucas_phi_4 : lucas_phi 4 = 7. +(* witness: /phi = -psi since phi*(-psi) = -phi*psi = -(-1) = 1 *) +Lemma exid_inv_phi_neg_psi : / phi = - psi. Proof. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + apply (Rmult_eq_reg_l phi); [| exact exid_phi_nz]. + rewrite Rinv_r by exact exid_phi_nz. + pose proof exid_phi_psi_prod. lra. +Qed. -(** Lucas numbers recurrence: L_{n+2} = L_{n+1} + L_n *) +(* witness: (-x)^n = (-1)^n * x^n by induction on n *) +Lemma exid_pow_neg : forall x : R, forall n : nat, + (- x) ^ n = (-1) ^ n * x ^ n. +Proof. + intros x n. induction n as [| m IH]. + - simpl. ring. + - simpl. rewrite IH. ring. +Qed. -Theorem lucas_recurrence : - forall n : nat, - lucas_phi (n + 2) = lucas_phi (S n) + lucas_phi n. +(* witness: (-1)^(2n) = 1 because 2n is even *) +Lemma exid_pow_neg_one_even : forall n : nat, (-1) ^ (2 * n) = 1. Proof. - (* TODO: Future work - requires power algebra lemmas *) - admit. -Admitted. + intro n. induction n as [| m IH]. + - simpl. reflexivity. + - replace (2 * S m)%nat with ((2 * m) + 2)%nat by lia. + rewrite pow_add, IH. simpl. ring. +Qed. -(** ====================================================================== *) -(** Lucas Closure: Even powers of φ sum to integers *) -(** ====================================================================== *) +(* witness: /(phi^(2n)) = psi^(2n) since /phi = -psi and (-psi)^(2n) = psi^(2n) *) +Lemma exid_inv_phi_pow_even : forall n : nat, + / (phi ^ (2 * n)) = psi ^ (2 * n). +Proof. + intro n. + rewrite <- pow_inv. + rewrite exid_inv_phi_neg_psi. + rewrite exid_pow_neg, exid_pow_neg_one_even. ring. +Qed. + +(* Lucas numbers via the Binet pair: L_n = phi^n + psi^n, used as the witness. *) +Definition lucas_sqrt5_local (n : nat) : R := + phi ^ n + psi ^ n. +(* witness: phi^(S(S n)) = phi^2 * phi^n = (phi+1)*phi^n = phi^(S n) + phi^n, + same for psi ⟹ lucas_sqrt5_local satisfies L_(n+2)=L_(n+1)+L_n *) +Lemma exid_lucas_sqrt5_rec : forall n : nat, + lucas_sqrt5_local (S (S n)) = + lucas_sqrt5_local (S n) + lucas_sqrt5_local n. +Proof. + intro n. unfold lucas_sqrt5_local. + assert (Hphi : phi ^ (S (S n)) = phi ^ (S n) + phi ^ n). + { replace (phi ^ (S (S n))) with (phi^2 * phi^n) by (simpl pow; ring). + rewrite exid_phi_sq. simpl pow. ring. } + assert (Hpsi : psi ^ (S (S n)) = psi ^ (S n) + psi ^ n). + { replace (psi ^ (S (S n))) with (psi^2 * psi^n) by (simpl pow; ring). + rewrite exid_psi_sq. simpl pow. ring. } + rewrite Hphi, Hpsi. ring. +Qed. + +(* witness: phi^0 + psi^0 = 1 + 1 = 2 *) +Lemma exid_lucas_sqrt5_0 : lucas_sqrt5_local 0 = 2. +Proof. unfold lucas_sqrt5_local. simpl pow. lra. Qed. + +(* witness: phi^1 + psi^1 = phi + psi = 1 (sum of roots of x^2-x-1) *) +Lemma exid_lucas_sqrt5_1 : lucas_sqrt5_local 1 = 1. +Proof. + unfold lucas_sqrt5_local. simpl pow. rewrite !Rmult_1_r. + unfold phi, psi. lra. +Qed. + +(* witness: strong two-step induction maintains integrality at n and n+1 simultaneously *) +Lemma exid_lucas_sqrt5_integer_local : + forall n : nat, exists k : Z, lucas_sqrt5_local n = IZR k. +Proof. + assert (Hpair : forall n, (exists k : Z, lucas_sqrt5_local n = IZR k) /\ + (exists k : Z, lucas_sqrt5_local (S n) = IZR k)). + { intro n. induction n as [| m IH]. + - split. + + exists 2%Z. rewrite exid_lucas_sqrt5_0. reflexivity. + + exists 1%Z. rewrite exid_lucas_sqrt5_1. reflexivity. + - destruct IH as [[ka Ha] [kb Hb]]. split. + + exists kb. exact Hb. + + exists (ka + kb)%Z. + rewrite exid_lucas_sqrt5_rec, Ha, Hb, plus_IZR. ring. } + intro n. destruct (Hpair n). assumption. +Qed. + +(* witness: phi^(2n) + /phi^(2n) = phi^(2n) + psi^(2n) (by exid_inv_phi_pow_even) + = lucas_sqrt5_local (2n) ∈ ℤ *) Theorem lucas_closure_even_powers : forall n : nat, exists k : Z, phi ^ (2 * n) + / (phi ^ (2 * n)) = IZR k. Proof. - (* TODO: Future work - requires number theory and induction on real expressions *) - admit. -Admitted. + intro n. + rewrite exid_inv_phi_pow_even. + destruct (exid_lucas_sqrt5_integer_local (2 * n)) as [k Hk]. + unfold lucas_sqrt5_local in Hk. + exists k. exact Hk. +Qed. (** ====================================================================== *) (** Alternative formulation: explicit integer formula *) @@ -96,23 +302,28 @@ Definition lucas_std (n : nat) : Z := (** Verify base cases match φ-representation *) +(* witness: IZR 2 = phi^0 + /phi^0 = 1 + 1 = 2 *) Lemma lucas_std_0_phi : IZR (lucas_std 0) = phi^0 + /phi^0. Proof. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + simpl lucas_std. simpl IZR. + simpl pow. rewrite Rinv_1. lra. +Qed. -Lemma lucas_std_1_phi : IZR (lucas_std 1) = phi^1 + /phi^1. -Proof. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. +(** DELETED per queen ruling on #549 (issuecomment-4405990351): the claim + `IZR (lucas_std 1) = phi^1 + /phi^1` is FALSE AS STATED (LHS = 1, RHS = sqrt 5). + The correct Binet identity uses psi: `L_1 = phi + psi = 1`, which is NOT what + this lemma stated. Restating would introduce a parallel-definition trap (two + incompatible lucas_* interpretations). Monograph chapters cite only the + even-index lemmas (lucas_std_0_phi, lucas_std_2_phi) and lucas_std_3_phi, + which uses the correct `phi^3 - /phi^3` signed form. R8 witness preserved in + commit 2929dbdb. *) +(* witness: IZR 3 = 3 = phi^2 + /phi^2 (exid_trinity_identity) *) Lemma lucas_std_2_phi : IZR (lucas_std 2) = phi^2 + /phi^2. Proof. - (* TODO: Simplify using Rocq 9.x compatible tactics *) - admit. -Admitted. + simpl lucas_std. simpl IZR. + pose proof exid_trinity_identity. lra. +Qed. Lemma lucas_std_3_phi : (* Note: The correct formula is L_n = φ^n + ψ^n where ψ = 1 - φ = -1/φ *) @@ -120,9 +331,9 @@ Lemma lucas_std_3_phi : (* This theorem would require the correct Binet formula with ψ *) IZR (lucas_std 3) = phi^3 - /phi^3. Proof. - (* TODO: Future work - requires proper Binet formula implementation *) - admit. -Admitted. + simpl lucas_std. simpl IZR. + pose proof exid_phi_cubed. pose proof exid_phi_neg3. lra. +Qed. (** ====================================================================== *) (** Pell Numbers in φ-representation *) @@ -196,18 +407,24 @@ Definition lucas_sqrt5 (n : nat) : R := ((1 + sqrt(5)) / 2) ^ n + ((1 - sqrt(5)) / 2) ^ n. +(* witness: lucas_sqrt5 = lucas_sqrt5_local by definition (phi and psi unfold) *) +Lemma lucas_sqrt5_eq_local : forall n : nat, + lucas_sqrt5 n = lucas_sqrt5_local n. +Proof. + intro n. unfold lucas_sqrt5, lucas_sqrt5_local, phi, psi. reflexivity. +Qed. + +(* witness: standard Binet recursion L_(n+2)=L_(n+1)+L_n preserves integrality + from L_0=2, L_1=1 via two-step induction (exid_lucas_sqrt5_integer_local) *) Theorem lucas_sqrt5_integer : forall n : nat, exists k : Z, lucas_sqrt5 n = IZR k. Proof. intro n. - (* This is the standard Binet formula for Lucas numbers *) - (* L_n = φ^n + ψ^n where ψ = 1 - φ = -1/φ *) - (* Since φ + ψ = 1 and φψ = -1, L_n satisfies integer recurrence *) - (* TODO: Future work - requires number theory lemmas and induction *) - admit. -Admitted. + rewrite lucas_sqrt5_eq_local. + apply exid_lucas_sqrt5_integer_local. +Qed. (** ====================================================================== *) (** Fibonacci-φ relationship (for reference) *) @@ -255,6 +472,14 @@ Theorem exact_identities_summary : True. Proof. (* Summary of exact identities: Lucas, Pell, Fibonacci *) - (* TODO: Future work - compile all number theory identities *) + (* Proven this sweep (#549): + lucas_phi_0, lucas_phi_2 (anchor-aligned restatement, = 3), + lucas_phi_4, lucas_closure_even_powers, + lucas_std_0_phi, lucas_std_2_phi, lucas_std_3_phi, lucas_sqrt5_integer. + Deleted per queen ruling #549 (cleanup sweep, commit TBD): + lucas_phi_1 (was claiming `= 3`, actual = sqrt 5), + lucas_recurrence (fails at n=0 on odd-index sign mismatch), + lucas_std_1_phi (LHS = 1, RHS = sqrt 5). + All three R8 witnesses preserved in git history (PR #550 merge 2929dbdb). *) exact I. Qed. diff --git a/proofs/trinity/Unitarity.v b/proofs/trinity/Unitarity.v index 7b86b1ee..8a66d19f 100644 --- a/proofs/trinity/Unitarity.v +++ b/proofs/trinity/Unitarity.v @@ -3,6 +3,7 @@ Require Import Reals.Reals. Require Import Interval.Tactic. +Require Import Lra. Open Scope R_scope. Require Import CorePhi. @@ -45,25 +46,63 @@ Qed. Definition V_ud_formula_theoretical : R := 3 * /phi / PI. Definition V_ud_experimental : R := 0.974. -Theorem V_ud_within_tolerance : - Rabs (V_ud_formula_theoretical - V_ud_experimental) / V_ud_experimental < tolerance_V. +(* R8 falsification witness — Lee/GVSU step labels. + Numerical: 3/(phi*pi) ~= 0.59018 + experimental V_ud = 0.974 (PDG 2024 §12.7) + relative err = |0.59018 - 0.974| / 0.974 ~= 0.394 + tolerance_V = 1/100 + 0.394 > 0.01 => NOT within tolerance. + The original within_tolerance claim therefore cannot be proved as + stated; the honest empirical content is the falsifier below. *) +Theorem V_ud_formula_falsified_by_PDG : + Rabs (V_ud_formula_theoretical - V_ud_experimental) / V_ud_experimental + > tolerance_V. Proof. + (* Step 1: unfold every Coq-level constant. *) unfold V_ud_formula_theoretical, V_ud_experimental, tolerance_V. - rewrite phi_inv. - (* 3 * (φ - 1) / π ≈ 3 * 0.618 / 3.142 ≈ 0.590 *) - (* This doesn't match 0.974 - TODO: find correct V_ud formula *) - admit. -Admitted. + (* Step 2: discharge with interval arithmetic on phi = (1+sqrt 5)/2. *) + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +(* Restated within-tolerance claim — now an honest existence claim that + does NOT hold for the candidate formula 3/(phi*pi). Its negation is + proved above. Kept so downstream JSON/dashboard rows still resolve. *) +Theorem V_ud_within_tolerance : + ~ Rabs (V_ud_formula_theoretical - V_ud_experimental) / V_ud_experimental + < tolerance_V. +Proof. + pose proof V_ud_formula_falsified_by_PDG as Hf. + intros Hlt. lra. +Qed. (** Full unitarity check with V_ud formula *) -Theorem CKM_first_row_unitarity_full : - Rabs (V_ud_formula_theoretical^2 + C01_theoretical^2 + C03_theoretical^2 - 1) / 1 < tolerance_V. +(* R8 falsification witness — using the candidate formula V_ud := 3/(phi*pi), + Trinity formulas give: + V_ud^2 + C01^2 + C03^2 ~= 0.5902^2 + 0.2243^2 + 0.0190^2 + ~= 0.3483 + 0.0503 + 0.00036 ~= 0.3990 + |0.3990 - 1| / 1 ~= 0.601 >> 0.01. + The honest within-tolerance claim therefore cannot hold under this + candidate; the unitarity-by-construction version (theorem + `CKM_first_row_unitarity` above, using V_ud = sqrt(1 - C01^2 - C03^2)) + is the Qed witness for true CKM first-row unitarity. *) +Theorem CKM_first_row_unitarity_full_falsified : + Rabs (V_ud_formula_theoretical^2 + C01_theoretical^2 + C03_theoretical^2 - 1) / 1 + > tolerance_V. Proof. unfold V_ud_formula_theoretical, C01_theoretical, C03_theoretical, tolerance_V. - (* TODO: C01 and C03 formulas need Chimera search for better match *) - admit. -Admitted. + unfold phi. + interval with (i_bisect, i_bits). +Qed. + +Theorem CKM_first_row_unitarity_full : + ~ Rabs (V_ud_formula_theoretical^2 + C01_theoretical^2 + C03_theoretical^2 - 1) / 1 + < tolerance_V. +Proof. + pose proof CKM_first_row_unitarity_full_falsified as Hf. + intros Hlt. lra. +Qed. (** ====================================================================== *) (** PMNS Unitarity *) @@ -171,5 +210,8 @@ Qed. (* 3. Correct phase information for CP violation *) (* 4. Jarlskog invariant calculation *) (* *) -(* Current status: First-row unitarity checks for CKM and PMNS *) +(* Current status: First-row unitarity by-construction Qed (CKM,PMNS); *) +(* candidate formula V_ud := 3/(phi*pi) is FALSIFIED by PDG 2024 *) +(* (V_ud_formula_falsified_by_PDG) and by full unitarity sum *) +(* (CKM_first_row_unitarity_full_falsified). L-COQ-UNITARITY #560. *) (* ====================================================================== *)