[itakura-hidetoshi]

Qi v4.35 — independently verified GK5BP → genuine north C60 raw observations

Base: independent GK5BP #3073 MERGED; canonical main b5520efd3c0b03d489e1b299f4cc12fbb08a91e9. Exact-source GK5BP CI #41752699168: Strict Lean 9288/9288, Governance 30/30 SUCCESS, 10 axiom-audited theorems no sorryAx, changed-file warning/error 0/0, source/test-merge tree 53175a0b80c64eec58ba0a5f191404342758f602 identical.

New independent Qi v4.35 module (228 lines, 9 axiom-audited statements + one Prop definition) and exactly one public aggregate import; original Lean files intact.

1. Genuine complete necessary/sufficient arithmetic certificate for ANY raw observation function values:Nat→Rat, using only values(0)...values(d), mathlib actual forward differences and signed falling-factorial coefficients. Equivalent to an actual Int[X] monomial coefficient lift of the constructed Newton polynomial, and also the actual GK5BL Lagrange interpolation on canonical sites.
2. For every true Int polynomial P degree≤d, directly prove the finite raw signed-Stirling arithmetic certificate from its integer sample evaluations. Values on nonnegative grid are proven to coincide with original integer-site evaluation and GK5BL recovery. This is NOT the claim that arbitrary integer observations imply an integer-coefficient polynomial.
3. Apply to each genuine original north F55 source f and actual original F55/P77 quotient q's descended Int[X] polynomial VALUE, without inverse Type-valued witnesses or class equality.
4. Original north primitive P=1 and double inverse plus genuine F55 right unit P=X² at canonical {0,1,2}, and chosen genuine P92B loops A=X³+2, B=2X²+X at NEW canonical {0,1,2,3} (not the earlier {-1,0,1,2} set) acquire separate raw observation certificates.
5. Preserve true C60 physical fifth-around closure, positive/negative original-phi local seam results, and conditional P89 BadPair reflection independently. No new P94A four-cell or global seam.

Strict 空 authority, independent Kuu→Qi, original F54 two Nat/two-category/Blocks and F55 Type history retained, root107. Protected PR #1558 remains Draft/open/unmerged; pinned Lean v4.30.0-rc2 and mathlib 5450b53e5ddc75d46418fabb605edbf36bd0beb6. No new axioms/sorry/admit/native_decide, no Gray/GK5BA/unconditional P89 or W=1→seam. Required: exact-source Strict Lean all changed Lean files + aggregate, 9 #print axioms, Governance 30/30, source/test-merge same tree. After green, squash merge then docs-only formal receipt.