Claims & Theorems
What K4 Forge proves, how strong each guarantee is, and where the proofs live.
Claim classes
Every result in K4 Forge carries a claim class that says exactly how strong the guarantee is. These labels appear throughout the demo and in all run artifacts.
| Class | Meaning | Proof requirement |
|---|---|---|
| [A] | Algebraic exact. Integer identity via SymPy, unconditional | Evaluates to Integer(0). No geometry, no model, no tolerance. |
| [G] | Geometry-dependent exact. Requires regular K4 + named field model | Closed-form derivation with explicit assumptions stated. |
| [G*] | Model-limited. Valid within stated regime only | Same as [G] but with additional regime constraints. |
| [M] | Numerical. Never promoted without a named proof path | Verified to stated tolerance. Not a proof — a measurement. |
| [H] | Heuristic. Engineering guidance, not a proof | Experience-based. No formal guarantee. |
| [C] | Conjectural. Incomplete proof | Evidence exists but proof chain is not closed. |
Authoritative vs Exploratory
k4_frozen — Authoritative
Immutable algebraic core. 182 consistency checks. Contains the truth kernel (M, G, D, C_INT, S matrices), field engine, and Biot-Savart implementation. Never edited without a version bump and full audit.
If k4_frozen and k4_theory disagree, k4_frozen wins.
k4_theory — Exploratory Oracle
Independent theorem mining and proof engine. 47 registered theorems, S4 symmetry miner, candidate discovery. Uses only numpy, sympy, and stdlib — never imports from k4_frozen.
Cross-validated against k4_frozen in tests. The disagreement itself is valuable — it means something needs investigation.
verify_layer1() check in k4_frozen after independent review and explicit version bump.Theorem inventory
47 registered theorems across 6 tiers. Each theorem is machine-verified on every test run.
T0
Integer Exact (DEC & Spectral)[A] Algebraic exact| T0.1 | L0 = 4I₄ − J₄ | Vertex Laplacian spectral decomposition |
| T0.2 | Cᵀ Dᵀ = 0 | DEC chain exactness |
| T0.3 | L1 = 4I₆ | Edge Laplacian is scalar identity |
| T0.4 | D M = 0 | Boundary operator kills cycles |
| T0.6 | D Cᵀ_T = 0 | Boundary of face = 0 |
| T0.7 | Cᵀ Dᵀ = 0 | Transpose DEC chain |
| T0.8 | D_redᵀ = G | Reduced incidence = cut basis |
| T0.12 | Mᵀ(Δ− 2I)G = 0 | Hodge-Sigma orthogonality |
| T0.14 | Mᵀ A_opp G = rank-1 | Opposite-edge coupling structure |
| T0.15 | ‖Mᵀ A_opp G‖²_F = 9 | Frobenius norm of opposite coupling |
INT
Integer Field Structure[A] Algebraic exact| INT.C | C_INT ∈ {-1,0,+1}³ˣ⁶ | Cross-product field matrix is integer |
| INT.CM_eq_neg2S | C_INT·M = −2S | Field-cycle product is twice sign matrix |
| INT.CG_zero | C_INT·G = 0 | Cut annihilation to Integer(0) |
| INT.det_CM_32 | det(C_INT·M) = 32 | Controllability determinant |
| INT.gram_CM | (C_INT·M)ᵀ(C_INT·M) = 4·Gram | Controllability Gram, κ=2 |
| INT.STS_gram | SᵀS = Gram | Sign matrix squared is 4I−J |
| INT.isotropy | S·adj·Sᵀ = 16I | Centroid isotropy via adjugate |
| INT.adj_check | Gram·adj = 16I | Adjugate correctness |
T1
Algebraic Exact (Topology)[A] Algebraic exact| T1.1 | MᵀG = 0 | Hodge orthogonality — cycle ⊥ cut |
| T1.2 | D M = 0 | Kirchhoff compatibility |
| T1.3 | MᵀM = GᵀG = 4I−J | Gram identity |
| T1.4 | det(MᵀM) = 16 | Gram determinant |
| T1.5 | det([M|G]) = ±16 | Full-space determinant |
| T1.6 | M⁺G = G⁺M = 0 | Pseudoinverse orthogonality |
| T1.7 | P_cyc + P_cut = I₆ | Projector completeness |
| T1.8 | P_cyc·P_cut = 0 | Projector orthogonality |
T2
Closed-form (Inductance & Ring-quiet)[G] Geometry-dependent exact| T2.1 | det(G_ring) = 0 | Ring solvability condition |
| T2.2 | null(G_ring) = span{1,1,1} | Ring null space is uniform |
| T2.3 | Ring-quiet ⇔ J1+J2+J3=0 | Balanced cycle condition |
| T2.5 | M_opp = 0 | Opposite edges have zero mutual inductance |
| T2.6 | Mᵀ L G = 0 | Hodge-inductance decoupling |
| T2.7 | L eigenvalue degeneracy | 3-fold degenerate cycle and cut eigenvalues |
T3 / SYM
Parametric (Electromagnetics)[G] Geometry-dependent exact| T3.1 | F·G = 0 | Cut annihilation at centroid (Biot-Savart) |
| T3.2 | det(F·M) ≠ 0 | Controllability determinant nonzero |
| T3.3 | rank(F·M) = 3 | Full 3D B-field control |
| SYM.F0G | F₀·G = 0 | Symbolic cut annihilation (parametric in L) |
| SYM.sign | F₀·M = α·S | Field-cycle factorization |
| SYM.F0M | det(F₀·M), κ=2 | Condition number of field matrix |
Sel
Selection Rules (Multipole)[M] Numerical| Sel.1 | Cut dipole = 0 | Cut currents produce zero dipole moment |
| Sel.2 | Cut quadrupole = 0 | Cut currents produce zero quadrupole moment |
| Sel.3 | Cycle octupole = 0 | Cycle currents produce zero octupole moment |
Anchor theorems
These four theorems form the backbone of the K4 field control story. Together they prove: cut currents cannot produce field at the centroid, cycle currents give full 3D control, and the system is well-conditioned.
Cycle and cut spaces are algebraically orthogonal. This is unconditional — it holds for any K4, any geometry, any field model.
The cross-product field matrix applied to cut currents is exactly zero — verified to Integer(0) via SymPy. No Biot-Savart needed.
The field-cycle product has full rank with integer determinant 32. Three cycle currents control all three field components.
The controllability Gram matrix has condition number 2 — well-conditioned by construction, not by luck.