面向代数数域上的二次格、一般 dyadic local fields 与 BONG theory 的 Mathematica/Wolfram Language 计算包。它现在可以从数域
The package is literature-driven: every theorem-level function records a theorem ID, hypotheses, individual condition checks, source status, and the invariants used in the decision.
Implemented:
- exact absolute number fields, algebraic elements, integral bases, discriminants, and signatures using native Wolfram exact algebraic numbers;
- prime ideals above a rational prime via a searched p-maximal integral generator and Dedekind--Kummer factorization, including exact ideal powers, normalized valuations, uniformizers, and residue representatives;
- global quadratic lattices with finitely generated coefficient fractional ideals, localization of pseudo-bases, candidate bad-prime enumeration, and batch local structures;
- automatic exact local-field backends at odd and dyadic finite primes of supported number fields;
- O'Meara-style local-lattice scale, norm, volume, determinant square class, dual, modularity, unimodularity, and quadratic-form scaling;
- dyadic additive lattice norm groups
g(L)=Q(L)+2s(L), norm/weight generators, the weight ideal, and fundamental norm groups/weights obtained from a Jordan filtration; - unified non-dyadic/dyadic Jordan splitting with certified
GL_n(O_F)basis changes, plus dyadic good-BONG construction from the same localized Gram matrix; - exact
Q2andQ2(Sqrt[2])valuation, square classes, relative quadratic defect, Hilbert symbols and norm groups; - validated arbitrary-dyadic-field backends from exact callbacks or complete finite square-class/defect/Hilbert tables;
- O'Meara 63:1--63:10 certificates for the Local Square Theorem, defect spectrum, square-class cardinality, the unramified quadratic class, and quadratic-extension norm groups;
- local quadratic-space isometry and representation;
R_i,alpha_i, truncated defects, good-BONG validation;- certified BONG construction from exact rational Gram matrices;
- certified conversion from a good BONG to scale/norm/volume and abstract Jordan data, together with classical/BONG and Jordan/BONG compatibility certificates;
- Beli lattice classification and representation certificates;
- 1-, n-, and classic n-universality criteria and structured minimal testing sets;
- integral and relative integral spinor-norm square-class groups;
- research-labelled local/global n-ADC and arithmetic-Springer certificates.
Explicitly excluded: GK/EGK invariants, local densities, Siegel series, mass formulae, and primitive representation.
Clone hzldew-git/LocalQuadraticBONG and load the package directly:
Get["path/to/LocalQuadraticBONG/Kernel/LocalQuadraticBONG.m"];
F = Q2Field[];The release also contains Dist/LocalQuadraticBONG.m, a generated single-file distribution:
Get["LocalQuadraticBONG.m"];Each manual documents all 89 public symbols, accepted input forms, return values, typical calls, certificate structure, theorem status, limitations, and reproducibility commands.
Rebuild both PDFs on Windows with the embedded documentation fonts:
python -m pip install -r requirements-docs.txt
python Scripts/build_function_manuals.pyF = Q2Field[];
LocalSquareClass[F, -10]
(* 6 *)
RelativeQuadraticDefect[F, 5]
(* 2 *)
GoodBONGQ[F, {1, -1/4}]
(* True *)
BONGAlphaInvariants[F, {1, -1/4}]
(* {0} *)
UniversalLatticeCertificate[F, {1, -1/4}]["Result"]
(* True *)
bong = FindGoodBONG[F, IdentityMatrix[3]];
bong["Entries"]
(* {1,1,1} *)
LatticeRepresentationCertificate[F, bong, {1,1}]["Result"]
(* True *)
K = Sqrt2DyadicField[];
{LocalValuation[K, 2], RelativeQuadraticDefect[K, 3]}
(* {2,3} *)
DyadicFieldValidationCertificate[K]["Result"]
(* True *)
FindGoodBONG[K, IdentityMatrix[3]]["Entries"]
(* {1,1,1} *)
H = QuadraticLatticeData[F, {{0,1/2},{1/2,0}}];
Lookup[LocalLatticeInvariants[F,H],
{"ScaleExponent","NormExponent","VolumeExponent",
"WeightExponent","ModularQ"}]
(* {-1,0,-2,0,True} *)
Lookup[LocalLatticeNormGroup[F,IdentityMatrix[2]],
{"NormalForm","NormExponent","WeightExponent"}]
(* {"a O_F^2 + b O_F",0,1} *)
J = LocalJordanSplitting[F,H];
{J["Result"], J["BasisChangeCertificate","Result"],
J["FundamentalInvariants","Result"],
Lookup[J["Components"],{"Rank","ScaleExponent"}]}
(* {True,True,True,{{2,-1}}} *)
bH = FindGoodBONG[F,H];
Lookup[BONGLatticeInvariants[F,bH],
{"ScaleExponent","NormExponent","VolumeExponent"}]
(* {-1,0,-2} *)
JordanBONGCompatibilityCertificate[F,J,bH]["Result"]
(* True *)
Clear[x];
NF = AlgebraicNumberFieldData[x^2 - 5, x];
P2 = First@NumberFieldPrimeIdeals[NF, 2];
LF = LocalFieldFromPrime[P2];
Lookup[P2, {"RamificationIndex", "ResidueDegree", "ResidueCardinality"}]
(* {1,2,4} *)
omega = Last[NF["IntegralBasis"]];
L = NumberFieldLatticeData[NF, {{1,0},{0,3}},
"CoefficientIdeals" -> {{2,omega},{1}}];
LocalStructureCertificate[L, P2]["Result"]
(* True *)Certificates are preferred over bare booleans:
cert = LatticeIsometryCertificate[F, {1,1,1}, {1,1,1}];
cert["ConditionChecks"]The self-checking script Examples/quickstart.m runs the same workflow from a fresh checkout:
wolframscript -file Examples/quickstart.m
wolframscript -file Examples/general-dyadic.m
wolframscript -file Examples/table-backend.m
wolframscript -file Examples/number-field-local.mThe backend layer has two exact profiles:
| Profile | Constructor | Input elements | Available computations |
|---|---|---|---|
| Number-field completion | LocalFieldFromPrime[NumberFieldPrimeIdeals[K,p][[i]]] |
exact elements of an absolute algebraic number field | normalized valuation, residue arithmetic, square classes, Hilbert symbols, local-lattice invariants, unified Jordan splitting, and dyadic BONG algorithms |
| Native exact arithmetic | Q2Field[], Sqrt2DyadicField[], or DyadicFieldData[...] |
exact Wolfram expressions understood by the callbacks | all theorem engines; Gram invariants/Jordan, BONG construction, and maximality when ResidueRepresentatives is supplied |
| Finite invariant tables | DyadicFieldFromTables[...] |
DyadicClassElement[F,class,ord] |
valuation, square classes, defect, Hilbert/norm groups, quadratic spaces, BONG invariants, classification, representation, universality and spinor formulas that need only multiplicative data |
For a complete dyadic field with residue cardinality q and e=ord(2), the table constructor requires exactly 4 q^e square classes and 2 q^e unit classes. It validates the elementary abelian square-class group, O'Meara's defect spectrum, the unique unramified quadratic class, and the symmetric nondegenerate bilinear Hilbert pairing before returning a field object.
cert = DyadicFieldValidationCertificate[K];
Select[cert["ConditionChecks"], Not@TrueQ[#1["Passed"]] &]DyadicFieldData[...] is the general native protocol. Its required data are:
Name,Uniformizer,RamificationIndexOf2, andResidueCardinality;- exact
ValuationFunction,SquareClassFunction,RelativeDefectFunction, andHilbertSymbolFunctioncallbacks; - complete
SquareClassRepresentativesandUnitSquareClassRepresentativeslists.
Set "NativeExactArithmetic" -> True when the elements support exact Wolfram arithmetic. Supply one lift of every residue-field element in "ResidueRepresentatives" to enable Gram-matrix algorithms. LocalJordanSplitting, FindBONG, FindGoodBONG, and MaximalIntegralLatticeQ then enumerate projective nonzero residue vectors over O_F/p; they are no longer hard-coded to {0,1} or index 2. The one-step maximality test uses an index-q overlattice, with q=|O_F/p|.
For the convention Q(x)=x.G.x and B(x,y)=x.G.y, the package records local fractional ideals by their normalized exponent with respect to the backend uniformizer pi:
LocalLatticeScale[F,L]:min ord(G[[i,j]]);LocalLatticeNorm[F,L]: the minimum oford(G[[i,i]])andord(2 G[[i,j]])fori<j;LocalLatticeVolume[F,L]:ord(det G)for a regular free lattice;LocalLatticeInvariants[F,L]: the combined data and the valuation checks <= u <= s+e, corresponding tos(L) superset n(L) superset 2 s(L);LocalLatticeNormGenerator[F,L]: a scalarain the dyadic lattice norm group witha O_F=n(L);LocalLatticeWeight[F,L]andLocalLatticeWeightGenerator[F,L]: O'Meara's weight ideal and a generatorb;LocalLatticeNormGroup[F,L]: the additive groupg(L)=Q(L)+2s(L)in the certified normal forma O_F^2+b O_F;LocalLatticeDual[F,L]: Gram matrixInverse[G]and an exact pairing certificate;LocalLatticeModularityCertificate[F,L]: checksL# = s(L)^(-1)Lthrough aGL_n(O_F)comparison andord(v(L)) = rank(L) ord(s(L)).
Here O_F^2 means the set of squares of elements of O_F, not the square of an ideal. This additive lattice norm group is different from LocalNormGroup[F,d], which returns the multiplicative field-extension norm subgroup N(F(Sqrt[d])/F) modulo squares. If m(L) is the largest fractional ideal contained in g(L), then the implementation uses w(L)=p m(L)+2s(L) and O'Meara's effective Section 94 formula
w(L) = Sum_i a d(Q(x_i)/a) + 2s(L).
The return value records every basis contribution, the largest contained ideal, parity-law checks, and the bounds n(L) superset w(L) superset 2s(L). The five norm-group/weight entry points are intentionally dyadic and require exact Gram arithmetic plus relative quadratic defects.
LocalJordanSplitting[F,L] follows the effective successive-splitting pattern in O'Meara Sections 91C and 94. If the norm and scale exponents agree, it splits a unary norm generator. Otherwise, at residue characteristic two it splits a scale-modular binary block. Every projection coefficient is checked integral, the total basis matrix and its inverse are checked integral with unit determinant, and exact Gram reconstruction is mandatory. Equal-scale elementary blocks are grouped into a Jordan component; dyadic binary blocks remain binary and are never reported as a false integral diagonalization. At a dyadic prime, LocalLatticeFundamentalInvariants[F,L] applies the norm-group/weight calculation to every filtration lattice L^(s_i) and the same data are stored under J["FundamentalInvariants"] and on the individual Jordan components.
For a good BONG b={a1,...,an}, BONGLatticeInvariants[F,b] computes the classical ideal exponents from the BONG/Jordan correspondence: the norm exponent is R1, the volume exponent is Total[R], and the scale is recovered from the maximal-norm/Jordan blocks. It also uses Beli's formula ord w(L)=min(R1+alpha1,R1+e) (with the unary convention R1+e) to return the weight, norm/weight generators, largest contained ideal, and additive lattice norm group. BONGJordanStructure[F,b] returns the corresponding rank-one/two maximal-norm blocks and groups equal scales into abstract Jordan components.
The BONG diagonal belongs to an orthogonal basis of the ambient quadratic space; it is not in general an integral basis of the lattice. In particular, never substitute DiagonalMatrix[BONGEntries[b]] for the original lattice Gram matrix. BONGJordanStructure deliberately returns IntegralBasisRealizedQ -> False; use LocalJordanSplitting when an actual GL_n(O_F) basis transformation is required.
ClassicalBONGCompatibilityCertificate[F,L,b] first compares scale, norm, volume, determinant square class, integrality, and modularity. A BONG returned from the same Gram matrix is then checked by exact orthogonalization; an abstract BONG is checked by the full Beli good-BONG classification theorem. JordanBONGCompatibilityCertificate[F,J,b] additionally compares the Jordan ranks and ideal exponents. Per-component determinant square classes are retained as diagnostics only because they can vary with the chosen Jordan splitting. GoodBONGFromJordanSplitting[F,J] constructs a compatible good BONG only when J retains a certified integral Gram realization.
DyadicFieldFromTables[...] requires class/unit labels, valuation parities, distinguished classes for 1, pi, -1, and 2, the complete class-multiplication table, one relative-defect value per class, and the complete Hilbert-symbol matrix. The constructor rejects inconsistent dimensions, group laws, defect spectra, or Hilbert pairings. See Examples/table-backend.m for a complete schema and Examples/general-dyadic.m for the native Q_2(Sqrt[2]) workflow.
AlgebraicNumberFieldData[f,x] constructs an absolute number field. For each rational prime, NumberFieldPrimeIdeals[K,p] searches the integral basis for a primitive integral element whose order is p-maximal, factors its minimal polynomial modulo p, and constructs every prime above p by Dedekind--Kummer. The resulting prime object contains its (e,f,q), an HNF ideal basis, exact ideal-power and valuation callbacks, a uniformizer, and residue lifts.
NumberFieldLatticeData accepts a Gram matrix and optional "CoefficientIdeals"; every coefficient fractional ideal is a finite generator list. LocalizeLatticeAtPrime chooses a generator of minimum prime valuation for each coefficient ideal, scales the two Gram indices, and returns a local QuadraticLattice. LocalStructureCertificate now returns LatticeInvariants and a certified JordanSplitting at every finite prime. At residue characteristic two it additionally exposes LatticeNormGroup, Weight, FundamentalInvariants, GoodBONG, BONGLatticeInvariants, BONGJordanStructure, both cross-compatibility certificates, and the existing maximal-integrality result. See Examples/number-field-local.m.
The implementation is pure Wolfram Language and does not call Sage or Magma at runtime. Scripts/sage-number-field-crosscheck.sage is an optional independent comparison. The current prime-decomposition engine is not a full Montes/round-two implementation: if the bounded search cannot find a p-maximal primitive integral generator (in particular at a common index divisor), it returns Failure["PMaximalGeneratorNotFound",...]. Increase "MaxGeneratorSearch" or supply the local field through the existing callback/table protocol. Large dyadic residue quotients may also require increasing "MaxResidueRingSize". No machine-precision approximation is accepted as evidence for a square class or Hilbert symbol.
References/source-manifest.wl pins the local source versions by SHA-256. PDFs and TeX source documents are not redistributed. References/normalizations.md fixes valuation, Gram-matrix, defect, and representation-direction conventions.
WorkspaceManuscript results are clearly separated from established literature results. A successful certificate never promotes manuscript status to a published theorem.
From PowerShell:
wolframscript -file Scripts/run-tests.mBuild and verify the single-file release:
wolframscript -file Scripts/build-single-file.m
wolframscript -file Scripts/verify-dist.m
wolframscript -file Scripts/verify-sqrt2-hilbert.mThe last command independently reconstructs the four basis norm groups of Q_2(Sqrt[2]) by exact residue enumeration. If SageMath is available, sage Scripts/sage-sqrt2-crosscheck.sage checks the local Hilbert-symbol matrix and sage Scripts/sage-number-field-crosscheck.sage checks prime decomposition and normalized valuations.
Verify the pinned local literature versions without copying them into the repository:
python Scripts/verify_source_manifest.py "D:\path\to\literature"MIT. The license covers this software only, not the source papers named in the manifest.