// Copyright (c) 2012 Vadym Kliuchnikov sqct(dot)software(at)gmail(dot)com, Dmitri Maslov, Michele Mosca
//
// This file is part of SQCT.
//
// SQCT is free software: you can redistribute it and/or modify
// it under the terms of the GNU Lesser General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// SQCT is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with SQCT. If not, see <http://www.gnu.org/licenses/>.
//
#include "theoremverification.h"
#include "rint.h"
#include "resring.h"
#include <vector>
bool is_theorem_true()
{
// rring8 -- ring of integer residues modulo 8
// ri8 -- extension of rring8 using eigth root of unity
typedef ring_int< rring8 > ri8;
std::vector<ri8> g[2][8][8];
int d_conjecture[4] = {0,2,1,1};
for( int x1 = 0; x1 < 8; ++x1 )
for( int x2 = 0; x2 < 8; ++x2 )
for( int x3 = 0; x3 < 8; ++x3 )
for( int x4 = 0; x4 < 8; ++x4 )
{
ri8 x(x1,x2,x3,x4);
auto j = x.abs2().gde();
int a = (int) x.ipxx();
int b = (int) x.ipQxx();
if( j <= 1 )
g[j][a][b].push_back(x);
}
for( int j = 0; j < 2; ++j )
for( int ax = 0; ax < 8; ++ax )
for( int bx = 0; bx < 8; ++bx )
{
int ay = rring8::mod(-ax);
int by = rring8::mod(-bx);
int d_count[4];
for( auto x : g[j][ax][bx] )
for( auto y : g[j][ay][by] )
for( int d = 1; d <=3; ++d )
{
d_count[d] = 0;
for( int k = 0; k < 4; ++k )
{
ri8 t = x + ri8::omega(k) * y;
if ( t.abs2().gde() == d + j )
d_count[d]++;
}
if( d_conjecture[d] != d_count[d] )
return false;
}
}
return true;
}