[itakura-hidetoshi]

GK5BQ／Qi v4.36 — 形式証明記録・README・ROADMAP同期（文書専用）

両定理PRとも MERGED。新規3文書のappend-only差分のみで、既存Lean定理・公開集約を変更しません。

独立GK5BQ #3076: exact-source head 4ea15719bf4e8c2ef716e6c8d6a8a4b79ffc6e0a、squash e02876c5f937414cfd2ed54d944f14ff93d1bded。source/test-merge/squash tree bdb1e44c4e051af997181caa8261de730592e2aa一致。CI #41765361678：Strict Lean 9,290/9,290・Governance 30/30 SUCCESS、新規10定理公理監査sorryAxなし、変更Lean warning/error 0/0。

Qi v4.36 #3077: exact-source head a5ffb48a3a4e1419d6bfc1b4ed7f5b258cd0af42、test-merge f52cd0a21a3a9096aea80a3fd4440bd096a5ceb7、squash e32a0b8f6a3fd4c5b698a2ce3b512e2ceb590155。三者tree 8ba1a1b56a025b14fd297712753019ce5d48e7bb一致。CI #41766217786：Strict Lean 10,217/10,217・Governance 30/30 SUCCESS、新規11定理公理監査sorryAxなし、変更Lean warning/error 0/0。

数学的内容: 真正 descPochhammer(Int,k) の係数s(k,j)が固定mathlib Nat.stirlingFirst の符号付き整数像に等しい。生整数観測v:Nat→Intだけから整数分子N_(d,j)(v)=∑(d!/k!)Δ^k v(0)s(k,j)を構成し、d!·coeff(Newton_d(v),j)=N_(d,j)(v)、Int[X] 原像存在と全j≤dの整除条件d!∣N_(d,j)(v)を必要十分として形式化。GK5BL Lagrange補間にも同値。真正北C60 primitive／double inverse＋F55右単位／二つのP92Bループの2!／3!証明書も検証済み。元F55 Type値証拠、P77商類同一性、P94A四セル、GK5AY全域seam、無条件P89反射は新たに構成していない。

ファイル: 新規 docs/formal/GK5BQ-Qi-v4_36-signed-stirling-factorial-divisibility-certificates.md、README末尾追記、ROADMAP末尾追記（次GK5BR：素冪ごとの局所合同・局所から全体整除の条件付き合成）。

strict 空／独立Kuu→Qi、真正F54二Nat・二圏・Blocks／F55 Type履歴、公開root107、Lean v4.30.0-rc2／mathlib 5450b53e5ddc75d46418fabb605edbf36bd0beb6、保護PR #1558 Draft/OPEN未マージを保持。

文書専用CIゲート: Governance/Core Autonomy SUCCESS、Strict Lean SKIPPED（正常）、source/test-merge Git tree一致。検証済みHEADを指定してsquashマージ。