[pinterbanget]

Summary

This adds research/pr4100-chirp-odometer-tariff/. It audits the cost claims in Cinna Davis's #4100 PROOF.md section "Chirp tables: eliminating another d-factor scan". #4320 audited the chirp identity and listed this tariff as its open question 2.

Why it matters. #4100's ledger charges cached phases at power 0. A leftover per-record d factor would cost power ε = 1−10^-30 > 1−κ, and #4100's own composition-controls.json rejects exactly that route (old_per_record_d_chirp = (1−κ)−ε; the verifier checks this equality). The tariff is new in #4100 and has no lineage audit.

Claim type: a scoped proof audit (written amortization with explicit constants), checked against a literal four-tape head-movement count. No new κ.

Result

The tariff holds, under the factor-two radix premise PROOF.md states (t_i ∈ {r, r/2}):

1. Table-tape head travel: ≤ TP(1 + 12(t_max+1)/t_min) ≤ 31·TP, uniformly in d. Each step is charged by where its carry stops, and returns are included.
2. Cache tape: ≤ 30·TP + O(d²P).
3. Counter tape: ≤ 4T.
4. Products: exactly Σ_(k≤d−2) T/Π_(i<k) t_i < 2T. PROOF.md's bound of Σ(j+1)/2^j = 4 per record is valid but looser.
5. Rounding: with toward-zero rounding every value stays in the unit disk, and |π̃_0−π_0| ≤ (2d−1)√2·2^(−P).

At the caller (P = Θ(p), t_min ≥ 2) this gives O(V) head travel and O(V log p) arithmetic, matching the ledger's power-0 row.

Evidence

verify.py uses only the standard library and takes about 1.4 seconds.

• Literal head counts: 36 cases, d up to 12, radices 2 to 8. Every case lies within its written per-case bounds. Table travel per TP settles at 6.997 (radix 2) and 4.333 (radix 4), flat in d.
• Rounding: 4,820 records at d = 2..10, P = 16..32, against a 60-digit reference. The worst error is 0.754 of the bound.
• Controls, each of which must fail:
  • A per-record d-scan grows linearly, up to 66 TP at d=12.
  • Skewed radices (2,512) violate the factor-two premise and reach 258.5 TP, so the premise is load-bearing.
  • Round-to-nearest leaves the unit disk in 112 entries.
  • A unit-ratio running product drifts to 965× the error bound.

Commands run locally (macOS, CPython 3.12):

python3.12 -B scripts/research_package.py --package research/pr4100-chirp-odometer-tariff --check-only
  PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
python3.12 -B scripts/research_package.py --package research/pr4100-chirp-odometer-tariff
  PASS_REGISTERED_RESEARCH_PACKAGE research/pr4100-chirp-odometer-tariff outcome=completed
python3.12 -B scripts/check_research_commit.py --package research/pr4100-chirp-odometer-tariff --check-source-history
  PASS_RESEARCH_COMMIT_BYTES {... "files": 7, ...}

Not covered

• Table setup cost, which PROOF.md charges as o(V).
• The multiplier's own tapes.
• Interleaving with the polynomial-record payload layout.
• The 2^-4p precision constant.
• The model is a unit-cell multitape count of the stated layout, not a finite-state transition table. There is no proof-kernel check.

Task and overlap

• Card: uniform-transfer-audit, refined to this fixed-tape cost implication (recorded in TASK.json), priority revision 7.
• Base: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244. Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 is pinned at 337d04939571a637aeab54a0f58f54fde811663a.
• Advance claim.
• Overlap was refreshed at 08:26 UTC. No other PR or claim covers this tariff. Implement the complete physical Gaussian tensor transform #3935 (jmbarrancoml) is a related physical chirp transform for an earlier family and is not audited here.

Credit

The construction and the audited claims are Cinna Davis's #4100 (OpenAI Codex assistance). This audit and simulator were prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

🤖 Generated with Claude Code