The formal layer
Nine of this edition’s twelve results carry a proof-kernel certificate. This page is what that means, row by row, assembled from CONCORDANCE.json and the release log — it states no fact those files do not.
What the kernel said
release_verify --source: ALL CLEAN (source rebuild + verifier + clean-triple axioms)
Quoted from the release log, which is the artifact the certification cites. A result counts as kernel-certified only when its axiom base is exactly propext, Classical.choice, Quot.sound: the three standard axioms of Lean's kernel — propositional extensionality, the axiom of choice and quotient soundness — the base every Mathlib proof shares; a certificate is clean when these three are all it needs — with no sorryAx and no custom axiom.
The certified results
| result | Lean declaration | axioms measured |
|---|---|---|
| A0a-01-clause-i U^ev = N^ev is an A_t-subalgebra of U. | HybridQuantumLean.A1.GL1Newton.clause_iSandbox/A1/GL1/GOALv0a.lean | the clean triple |
| A0a-02-clause-ii The Harish–Chandra projection restricts to an isomorphism of A_t-algebras HC : Z(U^ev) → (N^ev)^W, and this isomorphism is the identity map of N^ev. | HybridQuantumLean.A1.GL1Newton.clause_iiSandbox/A1/GL1/GOALv0a.lean | the clean triple |
| A0a-03-clause-iii N^ev = S = Σ_{u∈Z} Σ_{r≥0} A_t · Y̌^u ν_r(Y̌) — the even Newton lattice is exactly the A_t-span of the shifted divided classes. | HybridQuantumLean.A1.GL1Newton.Nev_eq_spanSandbox/A1/GL1/NewtonUnivSpan.lean | the clean triple |
| A0a-04-lemma-grid For all m ∈ Z and r ≥ 0, B_r(m) = ν_r(q^m) ∈ Z[q^{±1}] — the grid values of the divided classes are integral, including at negative nodes. | HybridQuantumLean.A1.GL1Newton.Az_nuGridSandbox/A1/GL1/NewtonUnivGrid.lean | the clean triple |
| A0a-05-lemma-fwd For every u ∈ Z and r ≥ 0, Y̌^u ν_r(Y̌) ∈ N^ev; hence S ⊆ N^ev. | HybridQuantumLean.A1.GL1Newton.Newton_nuGenSandbox/A1/GL1/NewtonUnivGrid.lean | the clean triple |
| A0a-06-lemma-rev If g ∈ N^ev is an even toral POLYNOMIAL of degree ≤ d, then g = Σ_{r≤d} c_r ν_r(Y̌) with all c_r ∈ A_t. The windowed reverse inclusion. | HybridQuantumLean.A1.GL1Newton.mem_span_of_NewtonSandbox/A1/GL1/NewtonUnivSpan.lean | the clean triple |
| A0a-07-definition-1-presented U is the F_t-algebra on invertible pairwise commuting K_{n,±} with K_{0,±}=1, K_{m+n,±}=K_{m,±}K_{n,±}, K_{n,+}K_{n,−}=t^n; and the monomials (T^+)^w, | HybridQuantumLean.A1.GL1Newton.Presentation.equivTorusSandbox/A1/GL1/PresentedU.lean | the clean triple |
| A0a-08-nondegeneracy Clause (iii) is not vacuously true of a degenerate object: A_t[Ycheck^{±1}] ⊊ N^ev ⊊ K_1[Ycheck^{±1}] — strictly, on both sides, with K_1 = Frac(A_t) | HybridQuantumLean.A1.GL1Newton.clause_iii_nondegenerateSandbox/A1/GL1/NonDegeneracy.lean | the clean triple |
| A0a-09-kz-bridge Enlarging the ambient coefficient RING from F_t = Q(v)[t^{±1}] (not a field) to K_1 = Frac(A_t) = Q(v,t) adds no new Newton elements: the two readings | HybridQuantumLean.A1.GL1Newton.KzBridge.Newton_mem_KzAmbientSandbox/A1/GL1/KzBridge.lean | the clean triple |
The sources
7 files, shipped as they were built. They are Lean source: a browser shows them as text, which is what they are.
FamilyField1.leanGOALv0a.leanKzBridge.leanNewtonUnivGrid.leanNewtonUnivSpan.leanNonDegeneracy.leanPresentedU.lean
What a certificate does not say
The kernel certifies the formal statement. Whether that statement is faithful to the informal one is a separate question, and this edition answers it separately — see the embedding note, and the one ink-warranted row in the concordance.