[GamingPuzzled]

This is numerical / compiler-precision headroom only, with zero economic gain. The complete #5413 caller is
unchanged: the word, B/F packets, controller, invoice (regenerated byte-identically), paid and target profiles,
reserve 10⁻¹², compiler tuple and BIT stock are all the same. The raw moment is identical. Only the strict compiler gap
moves, along with the height carrier recomputed from it.

	κ (conditional)	tested	gap	j	H
#5413	.003027288235	.003027288245	1/7·10¹¹	55099	38569300000000000
#5462 (ours)	.0030272882389	.0030272882489	1/7·10¹¹	55099	38569300000000000
this PR	.0030272882489783	.0030272882489784	1/7·10¹⁶	72096	5046720000000000000000

This is +1.00783 × 10⁻¹¹ over #5462 and +1.39783 × 10⁻¹¹ over #5413. κ stays below #5409's fixed-profile ceiling
U = .00302728825.

What was pinned and why it can move

• The pin was a literal. Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's funding engine already derives the least height grid from any unit gap: the least
  j with (H+1)¹⁰⁰⁰ < 2ʲ, where H = j·den(gap). Its precision checker pinned the gap to 1/7·10¹¹ in one line. Its
  conjunction pinned the κ, tested, gap, gain, H and j literals and the hash of the accepted written proof.

• The written proof does not depend on the value. V16-APPLICATION-PROOF-v3.md is symbolic in N = 2^H and
  M = F16(N). The carrier appears only as recorded values at four sites:

  • the H line in §5;
  • the gap line in §5;
  • the §6 non-claim "H·gap = j, H·r0 = j/10 < log₂D0", which stays true for j = 72096 < 1048576;
  • the funded (K, C) pair in §8.

  §6–§7 never absorb anything at the fixed carrier.

• Only the alpha reserve binds. The 54+4 outer margins scale with the gap (the minimum strict margin is gap/10),
  so they stay positive for every positive unit gap. The binding constraint is funded_alpha_reserve, which caps the
  tested saving in (.003027288248978444, .003027288248978445). There is therefore no finest admissible gap. The
  package certifies the 1/7·10¹⁶ point in full. Its sweep funds every gap 1/(7·10^m), m = 12…18, in arithmetic; at
  m = 18 that gives κ = .003027288248978443.

What research/gap-parametric-precision-r15/gap_endpoint.py checks (about 5 s)

1. It authenticates Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's 63 capsule files and regenerates the invoice byte-identically. Funding passes at the new
   pair, and j and H are recomputed independently (least grid; the preceding grid point fails).

2. It generalises the precision checker. The one pinned line becomes "positive unit gap"; nothing else changes.

   • On Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's own manifest, the generalised checker reproduces Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's expected receipt, so the change is
     conservative.
   • At the new carrier, the receipt differs only in carrier_H, carrier_j, carrier_gap, expanded.N,
     expanded.M and proof_sha256.

3. It instantiates the written proof by exactly four literal substitutions, stored as
   V16-APPLICATION-PROOF-v3-R15.md. diff against Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's proof shows four changed lines.

4. It runs Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's conjunction with only endpoint/carrier literals moved: 25/25 PASS, with the same premise names.

5. Controls, all rejecting:

   • Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's pinned-gap precision checker rejects the new funding;
   • Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413's unsubstituted conjunction rejects it;
   • the generalised checker rejects the old H/j combined with the new gap;
   • the generalised checker rejects a non-unit gap;
   • tested .00302728825 and .0030272882489785 fail funded_alpha_reserve;
   • a non-unit gap fails the engine's grid.

   The script also checks the raw-root and reserve brackets.

Checks. --check-only gives PASS_PACKAGE_METADATA_AND_PINS, and check_research_commit gives
PASS_RESEARCH_COMMIT_BYTES. On macOS, #5413's own verify.py (the dependency command) passes runs 0–5. Run 6 stops at
RLIMIT_AS, which Darwin cannot lower; that command is meant for Linux CI. Transcripts are in logs/*.txt.

Assumptions. κ is conditional on exactly #5413's five retained premises:

• native all-column operation;
• owned erasure;
• the compiler contract;
• precision/tape;
• analytic recovery.

The instantiated proof is #5413's proof with its carrier literals replaced; it adds no new argument. No unconditional
theorem, formal acceptance or κ-maximality is claimed. Further gains at this profile are below 1.5 × 10⁻¹⁶. Anything
real must change the paid or target profile.

Credit

• Chris R (Clear1nsight) supplied Complete coupled-output caller: conditional κ = 0.003027288235 (+5e-12 over #5400) #5413 (caller, funding engine, precision checker, written proof and conjunction),
  Independently validate κ = 0.00302728823 for the direct backward caller #5400, Independently audit the coupled provider and conditional closure budget (no new κ) #5407 and Independently verify PR5413 neutrality, necessary pricing and source application #5414.
• Ali Romman (aliromman) supplied Conditional κ = 0.00302235 (+5.742e-7 over #4610): one owned helper relation #5377, Conditional κ = 0.00302666 (+4.31e-6 over #5377): eight joint helper relations #5383, Conditional κ = 0.00302725 (+5.75235e-7 over #5387): owned circuit transposition #5392 and Conditional κ = 0.00302728823 (+3.823e-8 over #5392): direct backward caller #5398.
• Dillon Amburgey (dillona) supplied Preserve all 632 native inputs in an eight-mode coupled helper provider #5402.
• zxv supplied the precision/compiler machinery.
• Dugongue, Cao Yifan (intqwq), Cinna Davis and Jacob Alan Sussman supplied the reserve refinements, the Conditional κ = 0.0030217758: joint helper interfaces and Lean compiler tightening #4610 word,
  the controller/helpers and the integer flow.
• Our Conditional κ = 0.0030272882389 (+3.9e-12 over #5413, numerical headroom only); exact owned-relation optimum closes the relation lever #5462 is the pinned-gap predecessor of this PR.

Prepared by Joel Pulikkan (GamingPuzzled). AI disclosure: Claude Opus 5.5 (Anthropic) via Claude Code, directed by
Joel Pulikkan (GamingPuzzled).

🤖 Generated with Claude Code

Stacked on #5462 (this branch contains #5462's commits; the new material is only research/gap-parametric-precision-r15/).