[MaxGhenis]

What's wrong

gov.irs.deductions.auto_loan_interest.phase_out.start gives a qualifying surviving spouse a $200,000 threshold. The law gives $100,000:

• 26 U.S.C. 163(h)(4)(C)(ii)(I) reduces the deduction "by $200 for each $1,000 (or portion thereof) by which the modified adjusted gross income of the taxpayer for the taxable year exceeds $100,000 ($200,000 in the case of a joint return)".

• 2025 Schedule 1-A, line 26: "Enter $100,000 ($200,000 if married filing jointly)".

• 2025 Form 1040 instructions, page 109 (No Tax on Car Loan Interest): "Married filing jointly—$200,000. All other filing statuses—$100,000."

• 26 CFR 1.163-16(h)(2) (T.D. 10054, 91 FR 57241, applying to 2025-2028): "$100,000 or, in the case of a joint Federal income tax return... $200,000". The preamble says the statute gives "a $100,000 phaseout threshold applicable to all other taxpayers".

A surviving spouse does not file a joint return (section 6013(a) allows one only to a husband and wife). The IRS reads the same wording in sections 224 and 225 and in 24(h)(3) (Schedule 8812 line 9, "All other filing statuses—$200,000") the same way.

The model's tips and overtime thresholds (sections 224 and 225, with the same wording) already give a surviving spouse the single amount. The federal CTC threshold still gives surviving spouses $400,000; that is issue #9703, which PR #10306 fixes.

The other statuses, checked against the same three sources:

• Single, head of household and married filing separately: $100,000 (unchanged).
• Joint: $200,000 (unchanged).
• Section 163(h)(4) has no joint-return requirement, so separate filers may claim.

Changes

• phase_out/start.yaml: SURVIVING_SPOUSE goes from 200,000 to 100,000. The references are now the statute clause and Schedule 1-A line 26 (page 2), and the description says modified AGI, which the formula uses.
• YAML cases for a surviving spouse at $100,000, $100,001, $101,000, $101,001 and $150,000, and at the thresholds for head of household, separate and joint filers. The $100,001 and $101,000 cases show the "(or portion thereof)" rounding up that the formula's np.ceil applies.
• tests/core/test_auto_loan_interest_deduction_properties.py (new) checks:
  1. the model against a restatement of Schedule 1-A lines 24-30 under all five filing statuses;
  2. bounds, and reductions in whole $200 steps;
  3. the rounded-up $1,000 steps across each full phase-out;
  4. that only a joint return has the higher threshold;
  5. monotonicity in income and in interest (Hypothesis).

Invariants

For every filing status s, modified AGI m and qualified interest i ≥ 0:

• 0 ≤ deduction ≤ min(i, 10,000), and min(i, 10,000) − deduction is a multiple of $200 when the deduction is positive.
• deduction = max(min(i, 10,000) − 200 × ceil(max(m − T(s), 0) / 1,000), 0), with T(JOINT) = 200,000 and T(s) = 100,000 otherwise.
• The deduction doesn't rise with m and doesn't fall with i. It stays constant while the rounded-up count of $1,000 increments is unchanged.
• Single, head of household, separate and surviving spouse give the same deduction at every m. A joint return at m gets what a single filer gets at m − 100,000.

Tests and CI cost

• 17 YAML cases. They include 26 CFR 1.163-16(h)(3) Example 2 (single filer, $7,000 of interest, MAGI $124,200, deduction $2,000), the same facts for a surviving spouse, single at $100,001, and a surviving spouse whose reduction passes the interest.
• Why the Python property test: the status-equivalence, joint-shift, monotonicity and piecewise-constancy relations, and the 3,135-unit step walk, can't be written as YAML. Its reference comes from Schedule 1-A literals in integer arithmetic, not from the parameter files. At 764d24f, an independent review ran 14 mutants, and every one failed at least one of the two files. Mutant n (single threshold $100,500) passed every YAML case then; the single filer at $100,001 now catches it. CI's Rest Python core group (shard 2) collects the file.
• Cost, measured locally on macOS at 764d24f: 1.63 s of test time, 22.8 s wall clock and 1.10 GB peak, almost all of it importing the shared system, which the group already pays for. On main's latest push run (c5837fb0), that group took 51:03 with a 10.9 GB peak on Linux CI. 354d6e6 triples the step walk's units; I have not measured that locally. This PR's CI artifact rest-python-test-timings-shard-2 gives the after numbers.
• At 764d24f, all 16 affected test files passed locally through heavy_run: the two above, the 7 state and federal consumer YAML files, and the itemized, backdating, MAGI, parameter-file, scale-threshold and build-metadata Python tests. The local rerun at 354d6e6 was held by a host reservation, so CI is the check at the final head.

Review

• Round 1, at 764d24f, ran on in-session Opus 5.5 agents because the Codex lanes were closed. Law review: APPROVE-WITH-NITS. Code and tests review: APPROVE-WITH-NITS, 14 of 14 mutants killed. 354d6e6 addresses their nits.
• GPT-6.1 Sol at 354d6e6: APPROVE-WITH-NITS, nothing blocking. Its nits were the cost note and durable Axiom evidence, both covered here.

axiom: us:statutes/26/163/h/4/C/ii/I encoded-correct

• At rulespec-us main (2c9154c9), the module gives modified_adjusted_gross_income_phaseout_threshold_joint ($200,000) only when filing_status == 1 (joint). Every other code, including 4 (surviving spouse), gets $100,000. The reduction is 200 * ceil(max(0, MAGI - threshold) / 1000).
• The shipped companion tests cover a single filer at $100,000 and $100,001 and a joint return at $260,000, but no surviving spouse.
• I ran 8 extra companion cases through axiom-encode test on the pinned engine (89571cc2, from rulespec-us .axiom/workflow-toolchain.toml). They cover:
  • a surviving spouse at $100,000, $100,001, $101,000 and $101,001;
  • separate and head-of-household filers at $100,001;
  • a joint return at $200,000 and $200,001.
• All 12 cases passed (the 4 shipped and the 8 new): reductions of 0, 200, 200, 400, 200, 200, 0 and 200.
• Negative control: a case expecting the old $200,000 surviving-spouse threshold fails. The engine gives a threshold of 100,000 and a reduction of 200 at $100,001.
• The companion file is hashed in its signed encoding manifest, so the cases go through the signed encoder: Add companion cases for IRC §163(h)(4)(C)(ii)(I): a surviving spouse, head of household and separate filer use the $100,000 car loan threshold (PE-US #10395) TheAxiomFoundation/rulespec-us#1884 (pe-parity) holds them, verbatim.

Hub microsimulation impact (current head)

A real microsimulation on the default dataset, main at the merge base 3128b7894c against this PR's head 764d24f9c2, for 2025 and 2026. The runs went one at a time under the shared heavy-job lock. Sums are weighted.

Output	2025 change	2026 change	2025 records changed (weighted)	2026 records changed (weighted)
auto_loan_interest_deduction	-1.90M	-2.32M	30 (13,156)	30 (16,746)
state_income_tax	+0	+13,218	5 (0)	5 (2,613)
income_tax	+271,863	+338,828	29 (13,156)	29 (16,746)
household_net_income	-271,905	-363,209	29 (13,156)	29 (16,746)
household_benefits	+0	+0	0 (0)	0 (0)

Comparison files are in fixes/10395-impact/ on the hub host.

These runs were at 764d24f9c2. The one later commit, 354d6e6cb3, changes no computed value: every parameter value is identical and the formula's code is identical apart from its reference tuple (checked by YAML and AST comparison); the rest is tests. The change is confined to surviving spouses with car loan interest and modified AGI between $100,000 and $250,000.

🤖 Generated with Claude Code

[MaxGhenis]

Hand-off to the US + core hub.

• Head: 354d6e6cb3. The PR is ready for review (it just left draft), so CI is starting now.
• Review: GPT-6.1 Sol at 354d6e6, APPROVE-WITH-NITS with nothing blocking (~/reviews/auto-loan-qss-2026-10-22/review-sol-r1.md). The round-1 Opus law review and code/tests review at 764d24f both returned APPROVE-WITH-NITS (review-law-r1.md, review-code-r1.md), and 354d6e6 addresses their nits.
• Passed: at 764d24f, the 16 affected test files locally and 14/14 mutants killed; ruff format and check are clean.
• Pending: CI at 354d6e6. The local final-head rerun was held by the budget-w5-rehearsal reservation, so CI is the check.
• Impact: at 764d24f (fixes/10395-impact/). 354d6e6 computes the same values: parameter values and formula AST are identical.
• Axiom: encoded-correct. Companion cases are queued in Add companion cases for IRC §163(h)(4)(C)(ii)(I): a surviving spouse, head of household and separate filer use the $100,000 car loan threshold (PE-US #10395) TheAxiomFoundation/rulespec-us#1884.
• Depends on nothing. No Max decision. Land on the standard gates.
• Follow-ups: the QBI surviving-spouse threshold (Give surviving spouses the single QBI deduction threshold and phase-in range #10404) and the post-2028 car loan and senior deductions (task_239da288, proposed by the 10397 session).

[MaxGhenis]

US + core hub merge audit, us#10395 at 354d6e6cb3b70d1fac9d0b92fcc472d98b0ab937 (squash): Use the $100,000 car loan interest phase-out threshold for surviving spouses.

• Review: GPT-6.1 Sol r1 APPROVE-WITH-NITS (test runs interrupted), then the shell-backed Sol confirm review reviews-gen/us-10395/review-confirm.md APPROVE at 354d6e6, no blocking findings (17 YAML + 5 property tests passed; three expectations hand-checked; CI 27 passed, 3 skipped). Its methodology flag (surviving spouse uses $100,000) is logged as RULINGS us:car-loan-interest-surviving-spouse-phase-out-start. No human reviewer requested; adopted PR.
• Gates checked live at merge:
  • gh pr checks exits 0;
  • the latest Pull request run at the head concluded success;
  • MERGEABLE;
  • not a draft;
  • no reviewer's latest review requests changes;
  • the semantic-overlap guard;
  • head pinned.
• Impact: Hub microsimulation at 764d24f vs merge base 3128b78, 2025/2026: auto_loan_interest_deduction -$1.90M / -$2.32M (30 records). The only later commit, 354d6e6, changes references, descriptions and comments only (hub re-read its parameter and formula patches), so the measurement applies to the head.
• Axiom: us:statutes/26/163/h/4/C/ii/I encoded-correct