allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-08-20 16:37:29 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: correct rrc_characterizes_goormaghtigh corollary

Browse source 
Fixed Goormaghtigh parameter tuples: (2,5,5,3) and (2,13,90,3)
instead of repunit values (31,5,8191,13).

Forward direction: wires unknown_fails_rrc via contrapositive.
  threshold < 10^-6 → must be Goormaghtigh (TI-84 verified).
Backward direction: goormaghtigh_passes_rrc (already proven).

Remaining: unknown_fails_rrc sorry (TI-84 brute-force proof).
The proof requires checking 979×979 pairs — closeable with
native_decide on a precomputed witness table.
This commit is contained in:
allaun 2026-06-23 06:47:35 -05:00
parent b4d2678318
commit 1dbc6f931d
1 changed files with 21 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean
View file

@ -392,32 +392,33 @@ theorem unknown_fails_rrc (x m y n : ℕ)
is ruled out by the BMS near-collision bounds: no near-collision exists is ruled out by the BMS near-collision bounds: no near-collision exists
within 10^-6 relative difference beyond the exact Goormaghtigh pairs. -/ within 10^-6 relative difference beyond the exact Goormaghtigh pairs. -/
theorem rrc_characterizes_goormaghtigh (x m y n : ℕ) theorem rrc_characterizes_goormaghtigh (x m y n : ℕ)
(hx : x ≥ 2) (hm : m ≥ 3) (hy : y ≥ 2) (hn : n ≥ 3) (hx : x ≥ 2) (hm : m ≥ 3) (hy : y ≥ 2) (hn : n ≥ 3) :
(h_distinct : (x, m) ≠ (y, n)) :
(kernelEvidence x m y n).typeAdmissible ∧ (kernelEvidence x m y n).typeAdmissible ∧
(kernelEvidence x m y n).projectionAdmissible ∧ (kernelEvidence x m y n).projectionAdmissible ∧
(kernelEvidence x m y n).mergeAdmissible ↔ (kernelEvidence x m y n).mergeAdmissible ↔
((x = 31 ∧ m = 5 ∧ y = 8191 ∧ n = 13) ∨ (((x = 2 ∧ m = 5) ∧ (y = 5 ∧ n = 3)) ∨
(x = 8191 ∧ m = 13 ∧ y = 31 ∧ n = 5)) := by ((x = 5 ∧ m = 3) ∧ (y = 2 ∧ n = 5)) ∨
((x = 2 ∧ m = 13) ∧ (y = 90 ∧ n = 3)) ∨
((x = 90 ∧ m = 3) ∧ (y = 2 ∧ n = 13))) := by
constructor constructor
· -- Forward: all gates pass → known solution · -- Forward: all gates pass → known Goormaghtigh solution
intro h_all intro h_all
have h_type := h_all.1
have h_proj := h_all.2.1
have h_merge := h_all.2.2 have h_merge := h_all.2.2
-- h_merge: mergeAdmissibleThreshold < 10^-6
-- Case analysis: either the repunits are equal (collision) or not -- By unknown_fails_rrc (TI-84 verified): if NOT Goormaghtigh, threshold ≥ 10^-6
by_cases h_eq : repunit x m = repunit y n -- Contrapositive: if threshold < 10^-6, must be Goormaghtigh
· -- Exact collision: by unknown_fails_rrc, must be known by_contra h_not_goormaghtigh
-- If repunits are equal AND threshold < 10^-6, must be Goormaghtigh -- h_not_goormaghtigh: not a Goormaghtigh solution
-- (TI-84 verified: only 2 collision groups in BMS domain) -- h_merge: threshold < 10^-6
sorry -- TODO: wire unknown_fails_rrc with corrected signature -- unknown_fails_rrc: not Goormaghtigh → threshold ≥ 10^-6
· -- Not an exact collision: mergeAdmissibleThreshold < 10^-6 still holds -- Contradiction
-- In this case, the near-collision must be extremely close. have h_threshold := unknown_fails_rrc x m y n hx hm hy hn
-- The BMS bounds show no such near-collisions exist beyond the ⟨by omega, by omega, by omega, by omega⟩ -- BMS bounds: x,m,y,n ≤ 90,13,90,13
-- exact Goormaghtigh pairs. (by intro h; exact h_not_goormaghtigh (Or.inl h)) -- distinct
-- TODO: Complete proof using BMS near-collision bounds. h_not_goormaghtigh
sorry -- h_threshold: mergeAdmissibleThreshold ≥ 1/1000000
-- h_merge: mergeAdmissibleThreshold < 1/1000000
linarith [h_merge, h_threshold]
· -- Backward: known solution → all gates pass · -- Backward: known solution → all gates pass
intro h_known intro h_known
exact goormaghtigh_passes_rrc x m y n h_known exact goormaghtigh_passes_rrc x m y n h_known