[itakura-hidetoshi]

Qi v4.36 — genuine north C60 integration of independent GK5BQ

Base: canonical main e02876c5f937414cfd2ed54d944f14ff93d1bded after independent GK5BQ #3076 MERGED. Its exact-source CI #41765361678 is Strict Lean 9290/9290, Governance 30/30 SUCCESS, 10 audited theorems no sorryAx, warnings/errors 0/0; matching source/test-merge/squash tree bdb1e44c4e051af997181caa8261de730592e2aa.

New true north Qi v4.36 source file (230 lines / 11 theorem audits), and one appended import at KuuOSFormal. Existing Kuu and Qi proof statements unchanged.

1. Prove true pinned mathlib signed Stirling formula s(k,j)=(-1)^(k-j) * Nat.stirlingFirst k j for j≤k, transferred from GK5BQ.
2. For arbitrary raw integer observations v, transfer the actual necessary-and-sufficient Newton and GK5BL Lagrange coefficient lift criterion ∃Int[X] source ↔ ∀j≤d, d! ∣ N_{d,j}(v), using numerators constructed ONLY from integer observations, their actual Mathlib finite differences, canonical d!/k! ratios, true signed Stirling coefficients. Failing divisibility is a genuine arithmetic obstruction; integer-valued samples do not suffice unconditionally.
3. For every actual Int polynomial P with natDegree≤d, prove its true integer observations automatically satisfy the explicit divisibility. Apply to actual original F54/F55 north Type source via its original P92B depth polynomial and to actual original F55/P77 class's descended polynomial VALUE; do not identify source classes.
4. True north primitive P=1 and genuine double inverse + right F55 identity P=X² on {0,1,2}, and independently chosen actual north P92B loops P=X³+2, Q=2X²+X on {0,1,2,3}: separately prove d!=2 or d!=6 divisibility.
5. Keep genuine fifth-around physical C60 gauge, existing original positive/negative local seams, and conditional original P89 BadPair reflection independent; do not claim new F55 Type sources, P94A four-cells, universal GK5AY seam, GK5BA kit, Gray or W=1→seam.

Pinned: Lean 4.30.0-rc2, mathlib 5450b53e5ddc75d46418fabb605edbf36bd0beb6. Strict 空 authority, independent Kuu→Qi, original F54 two-Nat/two-categories/Blocks/F55 Type history; public root107, protected #1558 Draft/open/unmerged; no new axiom/sorry/admit/native_decide.

Validation gate: exact-source Strict Lean new file + public aggregate, all 11 #print axioms free of sorryAx, Governance 30/30, changed-file Lean warning/error 0/0, source/test-merge Git tree equality. After green squash merge then docs-only formal receipt.