[pinterbanget]

Summary

This adds research/pr4412-pr4414-tensor-check/. It independently checks the tensor-and-split endpoint arithmetic of 1337isnot1337's #4412 (κ = 0.00247755, p3-fresh, J = 4^v) and #4414 (κ = 0.00267987, p6, J = ⌊(19/4)^v⌋). Their successor #4416 is checked in my #4428.

Claim type: certified exact arithmetic plus a written check of the split bound. No new κ. Neither PR is accepted, and their native audits are not re-checked.

Results

	#4412	#4414
α upper (stated)	0.999999996840 (≤ 1−10⁻⁹)	0.999999982435 (< 1−10⁻⁸)
γ upper (stated)	0.99896534 (< 999/1000)	0.99986298 (< 9999/10000)
raw mixed root	0.00247756164	0.00267988997
tensor power used / least under the same certified bound	15,000 / 10,714	150,000 / 60,701
H0, H1	reproduced exactly	reproduced exactly

• Split tails. qJ^τ + r^τ ≤ 2RJ^{−C} holds. For Conditional κ = 0.00267987 with a complete p6 native controller #4414, J ≥ (19/4)^v/2 doubles the tail, which α^v + 4γ^v accounts for.
• Exit bounds. θ < 7/8 (from 4^8 < 5^7) and θ < 31/32 (from 19^32 < 4^32·5^31) hold, and so do the exit constants B.
• Margins. The γ margins are 3.5·10⁻⁵ and 3.7·10⁻⁵. The tested savings sit 1.6·10⁻⁹ and 1.0·10⁻⁸ below the raw roots.

Evidence

python3.12 -B scripts/research_package.py --package research/pr4412-pr4414-tensor-check --check-only
  PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
python3.12 -B scripts/research_package.py --package research/pr4412-pr4414-tensor-check
  PASS_REGISTERED_RESEARCH_PACKAGE research/pr4412-pr4414-tensor-check outcome=completed   (~15 s, stdlib only)

Head: 40f675338b7102ec38d858355a1db6cc051778e7. Base: canonical main 12fa8c5c, priority revision 7. The audited files' SHA256 prefixes are in the README.

Not covered

• The native audits.
• The tensor construction's native realization.
• The outer premises.

Task and overlap

• Card: independent-moment, refined.
• Overlap: no other review of Conditional κ = 0.00247755 via native tensor strictification #4412 or Conditional κ = 0.00267987 with a complete p6 native controller #4414. This is a short follow-on to my Independently check #4416's paid-completion tensor bound at kappa 0.00268647: proof steps and arithmetic hold; gamma margin 8e-6; least v 5745 (no new κ) #4428 claim, so no separate advance claim was posted.

Credit

@1337isnot1337 (#4412, #4414), @zxv (#4359), and Jacob Alan Sussman (#4268).

Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance; no independent human review. Apache-2.0. This PR does not merge anything or change the frontier.

🤖 Generated with Claude Code