[itakura-hidetoshi]

Independent GK5BQ — exact pinned Mathlib signed Stirling identity and finite factorial divisibility of raw integer observations

Base: canonical main c55696293d8a21e3e49aa4e47f295bed6b1f3e31, GK5BP #3073, Qi v4.35 #3074, docs #3075 all MERGED.

10 axiom-audited Lean4 theorems, one new independent 274-line Kuu module and one appended import in KuuOSFormal.

1. Starting from actual pinned mathlib descPochhammer and Nat.stirlingFirst recursion, prove for every n,j nativeGK5BPSignedFirst n j = (-1:Int)^(n+j) * (Nat.stirlingFirst n j : Int), and the familiar (-1)^(n-j) variant under j≤n. No invented identities or assumptions.
2. On only integer raw observations v:Nat→Int, implement the actual integer-valued Mathlib forward differences; prove the cast relation with GK5BP's rational forward differences.
3. Use actual Nat.factorial_dvd_factorial to construct the integer multiplier d! / k! for all k≤d, and the integer numerator N_{d,j}(v)= ∑_{k=0}^d (d!/k!)·Δ^k v(0)·s(k,j).
4. Show the precise scaling identity (d!:Rat)*coeff(Newton(v),j) = (N_{d,j}(v):Rat), with the numerator also expressed directly through Nat.stirlingFirst.
5. Prove necessary and sufficient finite divisibility ∃ P:Int[X], P.map = Newton(v) ↔ ∀j≤d, (d!:Int) ∣ N_{d,j}(v). Transfer to the actual GK5BL Lagrange interpolation on canonical integer sites; failing coefficient gives a genuine obstruction.

Mathematical authority: integer observations do NOT imply integer monomial coefficients, and coefficient realization does not reconstruct original F55 Type proof, P77 source class, P94A four-cell, P89 source reflection, original-phi seam or global GK5AY seam. Strict 空, independent Kuu→Qi, F54 two Nat/two categories/Blocks and original F55 Type history preserved. Public root107, protected #1558 Draft/OPEN/unmerged. Pinned Lean v4.30.0-rc2 and mathlib 5450b53e5ddc75d46418fabb605edbf36bd0beb6.

Required validation: exact-source Strict Lean with public KuuOSFormal, all 10 #print axioms free of sorryAx, Governance 30/30, no changed Lean warnings/errors, source/test-merge identical tree. Read full new Lean file and pinned mathlib API when repairing CI; do not weaken theorems. After green, squash merge then Qi v4.36 north C60 integration and formal proof receipt.