Quantization and certificates
Compare exact quantization criteria for H=S(U(2)×U(3)), closed spin-four periods, a conditional parent transfer and a joint U(2) example.
Control names are kept as they appear in the application. Start with a reference, change one input at a time, and retain the assumptions with your result.
What this tool is for
Use this independent diagnostic before interpreting a polynomial cancellation as a globally quantized action. The global quotient correlates apparently separate coefficients. Closed spin-four periods ask a different question from universal degree-four cohomology. The panel makes this distinction visible and supplies exact witnesses rather than a single undifferentiated consistency label.
First steps
- Run the Demo, then compare C/2, C/36 and A+B.
- Enter exact fractions. Inspect the detecting cocharacter or spin manifold when a criterion fails.
- Change integer tensor pairings and inspect the unchanged residue class.
- Export JSON and open the certificate catalogue to replay the appropriate Lean or numerical check.
Controls and inputs
| Control | Meaning | Try this |
|---|---|---|
| α, β, γ | Rational coefficients in the centered SU(2), SU(3) and Y² convention. | Choose C/2; change γ to 1/4. |
| p, q, r | Integral lattice pairings for ordinary Green–Schwarz sources. | Change p from zero to one. |
| K₂, K₃, K₁ | Integer axion couplings with α=−K₂, β=−K₃, γ=K₁/72. | Use (0,1,12), then K₁=13. |
| b₀, b₁ | Integer U(2) coefficients; the accompanying Lean criterion also treats a common rational denominator. | Compare (1,6) with (1,5). |
| Exact figures / SVG | Select a lattice point to set alpha and delta at fixed beta; select a heat-map cell to read its exact U(2) period. | Compare b1=6 with b1=5; inspect (m,n)=(1,0), then export SVG and JSON. |
Reading the results
| Result | Meaning |
|---|---|
| Criteria and witnesses | Read α,β,δ and α,β,2δ separately. The shown counterexample is an exact nonintegral evaluation. |
| Conditional transfer | The annihilator ℓ(x,y,z)=x+y+2z vanishes on both columns of the parent map. Its nonzero value excludes matching only under the listed source and spectrum assumptions. |
| JSON / Lean | JSON retains every input, witness, source and limit. The catalogue includes five Lean files with 59 theorem declarations and their replay evidence. |
| Lattices and cocharacter fingerprint | Diamonds satisfy both criteria; rings satisfy spin periods only, in the displayed fixed-beta slice. Each heat cell shows Q modulo one; its exact Q is available on selection. Both plots and JSON use gqModel.figures, without fitted or invented samples. |
Passing a restricted arithmetic criterion does not establish a global action or a complete anomaly-free model. The modulo-three response class is conditional; it is not an identified global Z3 anomaly.
Worked example
Same polynomial, different background test
- Choose C/2 and read both rows.
- Universal integrality fails at the cocharacter (1,0,−1,0,0).
- Closed spin-four periods pass because the Y² period is even.
What to expect: These outcomes are compatible: the tests quantify over different backgrounds. Neither determines the orbifold background category.
Formulas and conventions
Q = α(A − C/4) + β(B − C/3) + γC; δ = γ − α/4 − β/3
Change from centered roots to integral characteristic classes.
Universal: α, β, δ integral; closed spin-4: α, β, 2δ integral
Ordinary bundles, with Wu parity supplying the spin restriction externally to Lean.
18K₂ + 24K₃ + K₁ = 0 mod 36
Known q=6 axion criterion; no identification with the GHU Higgs.
6ℓ(v) = 16 − 3p − 3q − 6r = 1 mod 3
Integer obstruction under fixed spectrum and ordinary parent responses.
Q(m,n) = b₀(m−n)²/4 + b₁(m+n)²/8
Joint integrality iff b₀ is integral and b₁+2b₀ is divisible by eight.
tₐ² = −1; Uₐ = −i tₐ; Uₐ² = +1
Representation involution differs from an ordinary Spin(20) isotropy lift.
Scope and limitations
- The global action on all fields, including bosonic Omega, and the admissible orbifold bundles remain open.
- The wall SU(2) divisibility criterion is known. No claim of new mathematics or full anomaly cancellation is made.
- Lean formalizes arithmetic. Characteristic-class topology, Wu parity and physical translations are external assumptions. The 3290 lift checks are exact computational checks, not Lean theorems.
- The 81 cocharacters are a finite visualization, not a universal proof. Values outside the lattice window are explicitly reported; only pixel coordinates are approximate.
If something is unclear
The input is rejected.
Use an integer or n/d with nonzero positive denominator. Tensor, axion and U(2) controls require integers. The last valid state is retained.
The result passes but model consistency is not checked.
Read the scope: a restricted quantization criterion is one necessary ingredient of a full action, not a certification of the remaining ingredients.
Terms used here
Sources and attribution
Current instrument guide. Archived editions retain their own scope.
Back to top