[itakura-hidetoshi]

GK5BP / Qi v4.35 — exact-source formal proof receipt (docs only)

Both Lean theorem PRs MERGED:

• Independent #3073: verified head 42a0fd10d4c0179f370fec9265b0d3e480954e1f, test-merge 1ebad306e340c7f70fd7e677995083d220bacc64, squash b5520efd3c0b03d489e1b299f4cc12fbb08a91e9, all Git tree 53175a0b80c64eec58ba0a5f191404342758f602. CI #41752699168: Strict Lean 9,288/9,288, Governance 30/30 SUCCESS, new 10 axioms audits, no sorryAx and no changed Lean errors/warnings.
• Genuine north Qi v4.35 #3074: verified head cdb2eac4f9668297972e882168b0fb87cc2549fc, test-merge 56f22c5b6c6c0776647e9279184e6041d7ab3ac3, squash 407bab8643ccece147b22ed4a74e995890ae6e65, all Git tree d95397f7a6ae7d643f71cfb955616577d0ab2dd5. CI #41753489564: Strict Lean 10,215/10,215, Governance 30/30 SUCCESS, 9 new axiom audits without sorryAx or changed-file errors/warnings.

Mathematics: from true raw observation values v(0),...,v(d), construct exact rational Newton polynomial with Mathlib forward differences and true falling factorial basis. Prove full observation recovery, degree bound, equality with existing GK5BL genuine Lagrange interpolant, and a finite necessary/sufficient signed-Stirling coefficient-integrality criterion for actual Int[X] polynomial lift. General integer-valued data are not claimed to imply integer monomial coefficients. Genuine original north F55 proof / original F55-P77 quotient descended polynomial VALUES, true primitive, double inverse and selected P92B endo loops receive the finite raw-observation certificates on canonical {0,1,2} and new {0,1,2,3}. No Type source identification, source P77 quotient equality, new P94A four-cell, or original-phi seam inference.

Proof boundary: signed first-kind Stirling coefficients are defined by actual integer coefficients of pinned Mathlib falling factorial descPochhammer Int, with Rat cast verified; the explicit identification with Nat.stirlingFirst recurrence is a future GK5BQ candidate, not an audited theorem in this PR.

Exactly 3 docs files: new docs/formal/GK5BP-Qi-v4_35-raw-newton-signed-stirling-certificates.md, README append, ROADMAP append. Existing Lean proofs untouched. Strict 空 / independent Kuu→Qi, original F54 two Nat/two categories/Blocks and F55 Type histories, public root107, #1558 Draft/OPEN/unmerged, fixed Lean v4.30.0-rc2 and mathlib 5450b53e5ddc75d46418fabb605edbf36bd0beb6.

Required docs-only validation: Governance and Core Autonomy SUCCESS, Strict Lean SKIPPED normally, source/test-merge Git tree equality. Squash merge only expected verified HEAD.