Independent verification: prove and certify the a < D/E diagnostic for the selected complex and bit ledgers (no new kappa)

[navinor]

Scope

Independent verification + diagnostic; no new kappa. The selected record and upstream/ are unchanged.

• Card: independent-moment (scope key c6f2494b197df3bc3591), track independent-verification, chooser seed 9246ead964f301161b3d7eec63704082 (OS-random draw). Scope refined (see research/selected-suppliers-de-diagnostic/TASK-CARD.md and TASK.json): the card's question and method are unchanged; the refinement names the two ledgers, endpoints and widths. The endpoint-moment card is already covered for the selected record by three code-disjoint series engines (Mercator, base-two, atanh prime chain), so this does not add a fourth series engine; the new content is the proof and application of the a < D/E diagnostic, and the bit ledger, which the complex local-word packing ceiling of Research note: packing ceiling (+0.87%) and 1/99 budget for the selected complex local word (no new kappa) #1240 does not cover.
• Base: dadfea6e8a78ff6ba901705f87532a71c6f5bbb8 (origin/main at entry). Branch research/agent-15-independent-moment-de-diagnostic-9246ead9, head 85a36123.
• Audited claims: the recorded moment acceptances of research/community-frontier1094-audit/ASSEMBLY.json (accept at the certified endpoints, reject at the next 1e-24 grid point) for both selected supplier ledgers, the ledger aggregates and their coverage identities, and the a < D/E diagnostic stated in autoresearch.md section 2 without an in-repo proof.

Result

For the priced bill f(a) = (1/(mW)) Σ n_r r (m/r)^a + c_s m^a, convexity gives the diagnostic rigorously: with D_eff = mW − Σ n_r r − c_s mW and E_eff = Σ n_r r ln(m/r) + c_s mW ln m, the exact root satisfies a* < D_eff/E_eff strictly whenever D_eff > 0 (tangent at a = 0 reaches 1 at D_eff/E_eff; f lies strictly above its tangent). For c_s = 0 this is exactly the stated a < D/E with D = mW − Σ n_r r, E = Σ n_r r log(m/r).

Ledger	recorded endpoint a	moment residual at a	at a + 1e-24	certified D/E ceiling	D/E ÷ a	screening extremum
complex (m=73, W=14336, N=144, no surcharge)	0.001675462676808103522925	−1.304215e-24	+1.624723e-24	0.001680590709754321699421	1.003061	0.013708749 (cap 51)
bit (m=64, W=28416, bad-residue surcharge)	0.001733427039589844234749	−1.598690e-24	+1.669360e-24	0.001738557248401367986042	1.002960	0.016127138 (cap 45)

• The independently computed residual intervals agree with the recorded mercator and base_two intervals of ASSEMBLY.json and reproduce the accept/reject sharpness at the next grid point; the complex values match research/community-frontier1094-audit/INDEPENDENT1094.json's moment_minus_one digits.
• The diagnostic overestimates the exact root by about 0.30% (complex) and 0.29% (bit): nearly sharp in this small-saving regime, so it is a safe screen here.
• Ledger aggregates are reconstructed from the published histograms and checked against both coverage identities: complex D = 73W − Σ n_r r = W − 64N = 5,120 (which also re-derives W = 14,336 from the histogram and N = 144), bit D = 64W − Σ n_r r = T(2Kv − L·cst) = 32(2·4·111 − 9·63) = 10,272.
• Screening extremum (screen only, not realizability): rank-mass-preserving repackings up to the halving-guard cap could push D/E to about 0.0137 (complex) and 0.0161 (bit); both exceed 1/99 ≈ 0.010101, so the screen alone does not decide the planning target there. For the complex local word the realizability-aware ceiling of Research note: packing ceiling (+0.87%) and 1/99 budget for the selected complex local word (no new kappa) #1240 (0.001690054109089) supersedes the per-histogram ceiling and already rules out the target; the bit word has no such analysis (open question in the README).

Method and independence

research/selected-suppliers-de-diagnostic/verify.py imports nothing from the retained engines (moment.py, base_two_moment.py, the atanh prime chain of research/pending-claims-independent-pricing, or the Mercator/base-two transcriptions under research/community-batch970-audit/submitted/957/). Exact rationals throughout; every enclosure comes from an explicit inequality; no floating point.

• ln by rational square-root bisection (x^(1/2^k), k = 112, 2^-320 dyadic grid; u − u²/2 ≤ ln(1+u) ≤ u), cross-checked by bisection inverting a certified Taylor exponential; both must agree on every used log (ln 2 correct to 30 printed digits).
• exp by Taylor partial sums with an explicit rational geometric tail bound (order 48; tail below 1e-150 at the largest exponent used). This matches the standard approach of the retained engines and is disclosed as such.
• Positive fixtures: exactly solvable single-rank ledger H={1:1}, m=2, W=1 with root a* = 1 < 1/ln 2 = D/E; agreement with recorded residuals; reconstructed coverage identities.
• 12 positive/negative controls, each required to be rejected or hold: tampered pin; bit ledger at wrong width m=73; one-count histogram mutation breaking the coverage identity; out-of-range rank; zero deficit; endpoint shifted two grid steps (must break acceptance); doubled bit surcharge (must break acceptance); negative surcharge.

Reproduce

python3 -B research/selected-suppliers-de-diagnostic/verify.py
python3 scripts/research_package.py --package research/selected-suppliers-de-diagnostic --check-only

Observed (Python 3.12.10, Windows, stdlib only): PASS_INDEPENDENT_DE_DIAGNOSTIC, 12 controls, and PASS_PACKAGE_METADATA_AND_PINS / PASS_REGISTERED_RESEARCH_PACKAGE research/selected-suppliers-de-diagnostic outcome=completed from the package runner. Machine-readable output: research/selected-suppliers-de-diagnostic/RESULT.json.

Repo test suite python3 -B -m unittest discover -s tests -p 'test_research_*.py': 18/20 pass here. The 2 failures are pre-existing Windows platform issues in tests/test_research_onboarding.py, unrelated to this package: (a) the fixture's Path.write_text writes CRLF while system core.autocrlf=true normalizes the committed blob, failing the fixture's own pin check in setUp; with core.autocrlf=false those 6 setUp errors disappear; (b) scripts/research_package.py's timeout path calls os.killpg, which does not exist on Windows. This package is not touched by either path.

Not covered / limitations

• Paid profiles are taken from the published ledgers (ASSEMBLY.json complex_profile; EXPECTED.json nine.profile, git-blob pinned by the assembly's bit_supplier block). This package does not rebuild either word from its original operations.
• The conservative (surcharge-on-complex) endpoints of ASSEMBLY.json are not rechecked.
• D/E bounds one fixed histogram's root; it is not a repacking bound and not a realizability statement.
• All inherited all-size/compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, analytic transfer and bit H1-H5 obligations remain assumptions. Not a multiplication theorem.

Overlap, credit and coordination

Nearest concurrent work (all distinct): #1240 (complex local-word packing ceiling via idle-mass optimization), #1264 (packing ceilings of open complex claims) and #1276 (PR 1094 idle rank-48 repartition ceilings) — the repacking-ceiling lineage; none proves the a < D/E diagnostic or covers the bit ledger. Endpoint certification lineage: research/pending-claims-independent-pricing (Sagar Thakrar's atanh prime chain) and the Mercator/base-two audit of PR957's lineage. Ledger reconstruction for the complex owner map: Josie Elliston's and Sagar Thakrar's audits composed in research/community-batch1099-audit/check_frontier1094.py.

Predecessor credit: the pricing model and the a < D/E diagnostic are Douglas Colkitt's (autoresearch.md); the pricing chain in research/pending-claims-independent-pricing is Sagar Thakrar's (PR 1069, with Anthropic Claude assistance); the complex ledger is Rohan Arun's PR 1094 construction on Jeremy Kothe's packing chain (selected review: docs/research/community-batch1099-review.md); the bit supplier is the PR 589 (DreamingOfClouds) / PR 555 (eumemic) lineage, retained unchanged by the selected record; the fixed-word packing-ceiling lineage is static44, PR 525, PR 643 and the author of #1240.

Contributor: Navinor, with substantial AI assistance ("with help from opencode"). Apache-2.0. Claim thread: #1166 (comment) (updated with FINDING/DONE alongside this PR). Priority revision 3 (#1272) landed after this assignment (drawn under revision 2); per autoresearch.md section 6 this completed evidence is preserved and submitted unchanged.

Optional feedback: the saturation of independent-moment on the selected record (already noted in #1200 (comment)) is confirmed; a per-card "existing checks for the current selected record" field would have redirected this session earlier. The overlap helper's find_overlap.py needs PYTHONUTF8=1 on Windows (cp1252 console crashes on ≥ excerpts and on gh output decoding).

[Mister-Meeseeks]

100-PR batch review at 85a361233431befe4b11cf878f7b1b77a244d473.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Independent rational log/Taylor bounds for the exact moment and effective deficit/entropy ratio, including rejection at the next grid point. Uses a pinned reference histogram rather than rebuilding its supplier; fractional repacking remains a theoretical relaxation.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.