Quantum and Circuits · Lean source
QuantumFourierRefutation.lean
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
quantum_fresh_20261026/fresh/QuantumFourierRefutation.lean18 lines
Original source path
verification/quantum_fresh_20261026/fresh/QuantumFourierRefutation.leanSkip declarations and read code
1 import QuantumArithmeticBridge
2 open Komorebi.QuantumArithmetic
3
4 -- Extract one coefficient from the checked full Fourier table.
5 theorem ramanujan_mode_one_eq_twelve :
6 dft12 ramanujanCVector 1 = cRat 12 := by
7 have h := congrArg (fun xs : List Cyclo12 => xs.getD 1 cZero) ramanujan_dft_table
8 change dft12 ramanujanCVector 1 = cRat 12 at h
9 exact h
10
11 -- Establish mathematical falsity independently of the historical negative test's evaluator.
12 theorem ramanujan_mode_one_ne_zero :
13 dft12 ramanujanCVector 1 ≠ cRat 0 := by
14 rw [ramanujan_mode_one_eq_twelve]
15 decide +kernel
16
17 #print axioms ramanujan_mode_one_eq_twelve
18 #print axioms ramanujan_mode_one_ne_zero
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: b5a6b6e4729b369311dc80b28fa327fb522a8e737b6486eecf6147e7ba4576de