Skip to content

feat(coq): PhiSquaredIdentity — close Crown47↔Coq gap #691

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
gHashTag wants to merge 1 commit into
base: master
Choose a base branch
from
Open

feat(coq): PhiSquaredIdentity — close Crown47↔Coq gap #691

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
362 changes: 362 additions & 0 deletions trios-coq/Kernel/PhiSquaredIdentity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,362 @@
(** * PhiSquaredIdentity.v — Kernel anchor proof: φ² + φ⁻² = 3
Closes the gap identified in COQ_APPENDIX_F.md (Crown47↔Coq coverage 79%).
The identity φ² + φ⁻² = 3 is the structural anchor referenced implicitly
by every file in trios-coq but never proved as a named theorem.

Suggested placement : trios-coq/Kernel/PhiSquaredIdentity.v
Logical path : -R . TriosCoq (register in _CoqProject)

DOI : 10.5281/zenodo.19227877
Anchor: phi^2 + phi^-2 = 3

Author: Vasilev Dmitrii <admin@t27.ai>
Closes: trios COQ_APPENDIX_F coverage gap (Crown47 anchor)
*)

(* ===================================================================== *)
(* IMPORTS *)
(* ===================================================================== *)

Require Import Coq.Reals.Reals.
Require Import Coq.Reals.R_sqrt.
Require Import Coq.Reals.RIneq.
Require Import Coq.Reals.Rsqr.
Require Import Coq.micromega.Lra.
Require Import Coq.micromega.Lia.

Open Scope R_scope.

(* ===================================================================== *)
(* DEFINITION OF φ (phi) *)
(* *)
(* We use Coq's standard real number library (Coq.Reals.Reals). *)
(* phi is defined CONCRETELY as a real expression, not as a Parameter, *)
(* so every proof can proceed by computation / algebra alone. *)
(* *)
(* φ = (1 + √5) / 2 (positive root of x² − x − 1 = 0) *)
(* φ⁻¹= 1 / φ = (√5 − 1) / 2 (also written /phi in R_scope) *)
(* ===================================================================== *)

Definition phi : R := (1 + sqrt 5) / 2.

(* ===================================================================== *)
(* SECTION 1 — AUXILIARY LEMMAS ABOUT sqrt 5 *)
(* ===================================================================== *)

(** (sqrt 5) * (sqrt 5) = 5.
Uses: sqrt_def : ∀ x, 0 ≤ x → sqrt x * sqrt x = x. *)
Lemma sqrt5_sq : sqrt 5 * sqrt 5 = 5.
Proof.
apply sqrt_def. lra.
Qed.

(** sqrt 5 ≥ 0. *)
Lemma sqrt5_nonneg : 0 <= sqrt 5.
Proof. apply sqrt_pos. Qed.

(** sqrt 5 > 2.
We use sqrt_lt_1 (monotonicity) and sqrt_lem_1 (characterisation). *)
Lemma sqrt5_gt2 : sqrt 5 > 2.
Proof.
assert (H4 : sqrt 4 = 2).
{ apply sqrt_lem_1; lra. }
assert (Hlt : sqrt 4 < sqrt 5).
{ apply sqrt_lt_1; lra. }
lra.
Qed.

(** sqrt 5 < 3. *)
Lemma sqrt5_lt3 : sqrt 5 < 3.
Proof.
assert (H9 : sqrt 9 = 3).
{ apply sqrt_lem_1; lra. }
assert (Hlt : sqrt 5 < sqrt 9).
{ apply sqrt_lt_1; lra. }
lra.
Qed.

(* ===================================================================== *)
(* SECTION 2 — BASIC PROPERTIES OF φ *)
(* ===================================================================== *)

(** LEMMA 1: phi > 0. *)
Lemma phi_pos : 0 < phi.
Proof.
unfold phi.
apply Rdiv_lt_0_compat.
- (* 0 < 1 + sqrt 5 *)
generalize sqrt5_nonneg. lra.
- lra.
Qed.

(** phi ≠ 0 — derived from positivity. *)
Lemma phi_neq0 : phi <> 0.
Proof.
apply Rgt_not_eq. apply phi_pos.
Qed.

(** phi > 1. *)
Lemma phi_gt1 : phi > 1.
Proof.
unfold phi.
(* (1 + sqrt 5)/2 > 1 iff sqrt 5 > 1 *)
generalize sqrt5_gt2.
intro H. lra.
Qed.

(* ===================================================================== *)
(* SECTION 3 — QUADRATIC IDENTITY FOR φ *)
(* ===================================================================== *)

(** LEMMA 2: phi^2 = phi + 1.
Algebraic derivation:
φ² = ((1+√5)/2)² = (1 + 2√5 + 5)/4 = (6 + 2√5)/4 = (3+√5)/2
φ+1 = (1+√5)/2 + 1 = (3+√5)/2 ✓
*)
Lemma phi_quadratic : phi ^ 2 = phi + 1.
Proof.
unfold phi.
simpl pow.
(* ((1 + sqrt 5) / 2) * ((1 + sqrt 5) / 2) * 1 = (1 + sqrt 5) / 2 + 1 *)
(* field_simplify may generate side condition 2 <> 0; handle with [lra|lra] *)
field_simplify; [| lra].
rewrite sqrt5_sq.
lra.
Qed.

(** Equivalent statement: φ² − φ − 1 = 0. *)
Lemma phi_minimal_polynomial : phi ^ 2 - phi - 1 = 0.
Proof.
generalize phi_quadratic. lra.
Qed.

(* ===================================================================== *)
(* SECTION 4 — INVERSION LEMMAS *)
(* ===================================================================== *)

(** LEMMA 3: /phi = phi − 1.
Algebraic derivation:
φ × (φ−1) = φ² − φ = (φ+1) − φ = 1, so 1/φ = φ−1.
*)
Lemma phi_inv_eq : / phi = phi - 1.
Proof.
field_simplify_eq.
- (* phi * (phi - 1) = 1 *)
generalize phi_quadratic.
simpl pow. lra.
- exact phi_neq0.
Qed.

(** /phi > 0 *)
Lemma phi_inv_pos : 0 < / phi.
Proof.
apply Rinv_pos. exact phi_pos.
Qed.

(** LEMMA 4: (/phi)^2 + (/phi) = 1.
This is φ⁻² + φ⁻¹ = 1 (the conjugate golden-ratio equation).
Derivation via phi_inv_eq:
ψ = φ−1,
ψ² + ψ = (φ−1)² + (φ−1) = φ²−2φ+1+φ−1 = φ²−φ = 1. ✓
*)
Lemma phi_inv_quadratic : (/ phi) ^ 2 + (/ phi) = 1.
Proof.
rewrite phi_inv_eq.
simpl pow.
generalize phi_quadratic.
lra.
Qed.

(* ===================================================================== *)
(* SECTION 5 — EXPLICIT VALUES FOR phi^2 AND (1/phi)^2 *)
(* ===================================================================== *)

(** LEMMA 5: φ² = (3 + √5)/2. *)
Lemma phi_sq_explicit : phi ^ 2 = (3 + sqrt 5) / 2.
Proof.
generalize phi_quadratic.
unfold phi.
lra.
Qed.

(** LEMMA 6: φ⁻² = (3 − √5)/2. *)
Lemma phi_inv_sq_explicit : (/ phi) ^ 2 = (3 - sqrt 5) / 2.
Proof.
rewrite phi_inv_eq.
unfold phi.
simpl pow.
rewrite sqrt5_sq.
lra.
Qed.

(* ===================================================================== *)
(* THEOREM — phi_squared_identity (THE MASTER ANCHOR) *)
(* *)
(* φ² + φ⁻² = 3 *)
(* *)
(* This is the structural anchor of the Crown47/trios framework. *)
(* Every file in the trios-coq corpus carries the comment *)
(* "Anchor: phi^2 + phi^-2 = 3" *)
(* but until this file the statement was never given a formal proof. *)
(* *)
(* PROOF (path A — via explicit values, recommended for committee): *)
(* φ² = (3 + √5)/2 [phi_sq_explicit] *)
(* φ⁻² = (3 − √5)/2 [phi_inv_sq_explicit] *)
(* sum = (3+√5 + 3−√5)/2 = 6/2 = 3 ✓ *)
(* *)
(* PROOF (path B — algebraic shortcut): *)
(* φ² = φ + 1 [phi_quadratic] *)
(* φ⁻² = 1 − φ⁻¹ [phi_inv_quadratic rearranged] *)
(* = 1 − (φ−1) [phi_inv_eq] *)
(* = 2 − φ *)
(* sum = (φ+1) + (2−φ) = 3 ✓ *)
(* ===================================================================== *)

Theorem phi_squared_identity : phi ^ 2 + (/ phi) ^ 2 = 3.
Proof.
(* Path A: substitute explicit values and cancel √5 terms. *)
rewrite phi_sq_explicit.
rewrite phi_inv_sq_explicit.
lra.
Qed.

(** Alternative proof via path B — purely algebraic, no sqrt reasoning. *)
Lemma phi_squared_identity_v2 : phi ^ 2 + (/ phi) ^ 2 = 3.
Proof.
generalize phi_quadratic. (* phi^2 = phi + 1 *)
generalize phi_inv_quadratic.(* (/phi)^2 + (/phi) = 1 *)
generalize phi_inv_eq. (* /phi = phi - 1 *)
lra.
Qed.

(* ===================================================================== *)
(* COROLLARIES *)
(* ===================================================================== *)

(** (/ phi)^2 = 3 - phi^2 *)
Corollary phi_inv_sq_from_master : (/ phi) ^ 2 = 3 - phi ^ 2.
Proof.
generalize phi_squared_identity. lra.
Qed.

(** phi^2 > 2 (was axiom phi_sq_lo in SubThreshold.v). *)
Corollary phi_sq_gt2 : phi ^ 2 > 2.
Proof.
generalize phi_quadratic. generalize phi_gt1. lra.
Qed.

(** phi^2 <= 3 (was axiom phi_sq_hi in SubThreshold.v). *)
Corollary phi_sq_le3 : phi ^ 2 <= 3.
Proof.
generalize phi_squared_identity.
generalize (pow_le (/ phi) 2 (Rlt_le _ _ phi_inv_pos)).
lra.
Qed.

(** Integer witness: φ² + φ⁻² = INR 3. *)
Corollary phi_sum_is_INR3 : phi ^ 2 + (/ phi) ^ 2 = INR 3.
Proof.
rewrite phi_squared_identity. simpl INR. lra.
Qed.

(* ===================================================================== *)
(* SECTION 6 — LUCAS NUMBER L₂ = 3 (bonus) *)
(* *)
(* The Lucas sequence: L_n = φⁿ + ψⁿ where ψ = −1/φ. *)
(* L₀ = 2, L₁ = 1, L₂ = 3 (= phi_squared_identity). *)
(* ===================================================================== *)

Definition psi : R := - (/ phi).

(** ψ = 1 − φ. *)
Lemma psi_eq : psi = 1 - phi.
Proof.
unfold psi. rewrite phi_inv_eq. lra.
Qed.

(** L₀ = 2. *)
Lemma lucas_L0 : phi ^ 0 + psi ^ 0 = 2.
Proof. simpl. lra. Qed.

(** L₁ = 1. *)
Lemma lucas_L1 : phi ^ 1 + psi ^ 1 = 1.
Proof.
simpl pow.
rewrite psi_eq. lra.
Qed.

(** L₂ = 3. This is phi_squared_identity.
Note: ψ² = (−1/φ)² = 1/φ².
We use Rsqr_neg to handle the negation.
Rsqr_neg : ∀ x, Rsqr (- x) = Rsqr x *)
Lemma lucas_L2 : phi ^ 2 + psi ^ 2 = 3.
Proof.
unfold psi.
(* (- /phi)^2 = (/phi)^2 *)
rewrite <- Rsqr_pow2.
rewrite Rsqr_neg.
rewrite Rsqr_pow2.
exact phi_squared_identity.
Qed.

(** Lucas recurrence at n=0: L₂ = L₁ + L₀, i.e., 3 = 1 + 2. *)
Lemma lucas_recurrence_base :
phi ^ 2 + psi ^ 2 = (phi ^ 1 + psi ^ 1) + (phi ^ 0 + psi ^ 0).
Proof.
rewrite lucas_L2, lucas_L1, lucas_L0. lra.
Qed.

(* ===================================================================== *)
(* SECTION 7 — HIGHER POWER WITNESSES *)
(* ===================================================================== *)

(** φ³ = 2φ + 1. *)
Lemma phi_cube : phi ^ 3 = 2 * phi + 1.
Proof.
simpl pow.
generalize phi_quadratic. generalize phi_pos.
intros Hpos Hq.
nlinarith [phi_quadratic].
Qed.

(** φ⁴ = 3φ + 2. *)
Lemma phi_fourth : phi ^ 4 = 3 * phi + 2.
Proof.
simpl pow.
generalize phi_pos. generalize phi_quadratic. generalize phi_cube.
intros Hc Hq Hp.
nlinarith [phi_quadratic, phi_cube].
Qed.

(* ===================================================================== *)
(* PLACEMENT NOTE *)
(* *)
(* 1. Copy to: trios-coq/Kernel/PhiSquaredIdentity.v *)
(* 2. Add to trios-coq/_CoqProject: *)
(* Kernel/PhiSquaredIdentity.v *)
(* 3. Add to citation_map.json under key "KERNEL_PHI_ANCHOR": *)
(* "coq_file": "Kernel/PhiSquaredIdentity.v", *)
(* "lemmas": [ *)
(* "phi_pos", "phi_neq0", "phi_gt1", *)
(* "phi_quadratic", "phi_minimal_polynomial", *)
(* "phi_inv_eq", "phi_inv_pos", "phi_inv_quadratic", *)
(* "phi_sq_explicit", "phi_inv_sq_explicit", *)
(* "phi_squared_identity", *)
(* "phi_sq_gt2", "phi_sq_le3", *)
(* "lucas_L0", "lucas_L1", "lucas_L2", *)
(* "phi_cube", "phi_fourth" *)
(* ], *)
(* "anchor": "phi^2 + phi^-2 = 3", *)
(* "doi": "10.5281/zenodo.19227877" *)
(* 4. Other trios-coq files that rely on the anchor can import: *)
(* From TriosCoq.Kernel Require Import PhiSquaredIdentity. *)
(* or: Require Import TriosCoq.Kernel.PhiSquaredIdentity. *)
(* ===================================================================== *)

(** Sanity checks — these lines type-check at load time. *)
Check phi_squared_identity.
(* Expected: phi ^ 2 + (/ phi) ^ 2 = 3 : Prop *)
Check phi_inv_quadratic.
(* Expected: (/ phi) ^ 2 + (/ phi) = 1 : Prop *)
Check phi_quadratic.
(* Expected: phi ^ 2 = phi + 1 : Prop *)
Loading