[MaxGhenis]

This PR covers Max's d1802 for the rules lane: G part 2 and R2 part (b). It applies Act 203(a)(4)'s deductions before the family-maximum reduction, which removes R2's deduction_before_reduction_part_b refusal. It also adopts SSA's operational reading of the 1972 saving clause, per Max's d1338, with the literal reading behind a switch. It also fixes #530's round-14 low finding. The work is statutory conformance on invented cases and SSA's published examples only, with no population claim.

Status: draft, waiting on Sol's seventh review of fbe491d4. GPT-6 Astra reviewed the first round, and GPT-6.1 Sol reviewed rounds 2 and 3. Each round below lists what that review found. #562 (insured status) and this PR touch _provenance.py, the shared schema and audit fixtures, and the tier files. Whichever merges second will merge master and recount. The coordinator's slot order after #574 is #562, #563, #565.

What changes

Deductions before reduction (G)

Act 203(a)(4); GN 02603.020, .040, .050, .090.

• The entry point. family_benefits_after_deductions, and its household form, take declared monthly deductions and apply the reduction for the maximum after them.
• Permanent deductions. Non-deductees share PTAP / (TOTOB − deductees' OBs), capped at OB and dime-floored, with deductees' payables and age reductions reserved (GN 02603.050C).
• Temporary deductions. They leave separate-household beneficiaries unchanged until the deduction is permanent (GN 02603.050D).
• Supported deductions. An auxiliary's or survivor's own earnings-test deduction (full or partial, permanent or estimated), no child in care, and Parisi. Parisi results through the new path are identical to before.
• Refused by name: workers' compensation, prisoner and drug-addiction suspensions, foreign work, penalty, maritime and election-certificate events, and the unsettled interaction of number-holder reservations with age reductions.
• Empty deductions change nothing. With no deductions, results equal ordinary G exactly, for families and households, and a differential property tests it.

403(a)(5): the saving clause (G)

• The switch. SavingsClauseReading on SavingsClauseGuard: SSA_OPERATIONAL is the default (RS 00630.400, RS 00615.801B.2), and LITERAL_REFUSAL keeps the earlier behaviour. Existing tests that pin the literal guard select it explicitly.
• What starts a protection. A protection starts only when a PIA increase lowers the total, the month is reduced for the maximum, and a beneficiary is age-reduced. A departure, or any other fall without a PIA increase, starts none. A COLA alone starts one only with an age-reduced beneficiary, which addresses the dime-rounding case from Track B G v2: close #495, compute five refused configurations, one contract across G, R2 and R3 #530's round 11.
• What a protection does. It protects the payment, not the formula maximum, and carries while the formula maximum stays smaller.
• Refused by name. Membership changes while a protection is active, and concurrent age-factor or maximum changes that leave the cause unsettled.

R2 part (b)

• Family context. Monthly RETFamilyMonth context lets an auxiliary's own deduction release maximum room to the others through the new G entry point (RS 02501.155–.160).
• Downstream effects. Final deductions flow to R3, and a delayed household increase creates no own-work credit.
• New refusal. Missing family facts refuse as deduction_readjustment_requires_family_context.

Fixes from #530's review

• Deleting a refusal's exception notes works again in all four layers; that was Track B G v2: close #495, compute five refused configurations, one contract across G, R2 and R3 #530's round-14 low finding.
• Stateful guard constructors register their declared enums before the first call.

Invariants

Each is a Hypothesis property:

• Exactness. Empty deductions give exactly ordinary G, and permanent rates follow the GN 02603.050C formula.
• Bounds. No rate exceeds its OB, and the counted total stays within the maximum.
• Temporary deductions. These leave a separate-household beneficiary at its ordinary rate.
• Reserved slack. Number-holder reservations never release existing maximum slack.
• Order and determinism. Results are deterministic and independent of beneficiary order.
• Input errors. Invalid inputs fail before any refusal, and every named refusal stays in the denominator.
• Saving-clause readings. Each reading starts exactly on its stated conditions, and a protection never inflates from deduction history.
• R2 accounting. Gross equals net plus deduction, both provisionally and finally. Unused G context leaves R2's earlier outputs unchanged.
• Refusal notes. Deleting a refusal's notes preserves provenance and the denominator.

One invariant is qualified, not absolute. Adding a deduction does not always keep the others' rates from falling: GN 02603.050A.1 disregards age reduction for a single full permanent deduction only when "no other deduction is involved", and GN 02603.050C reserves the age reduction otherwise. A minimized case is pinned (PIA $48, maximum $78): the children's rates fall from $10 to $9.90 when a second, $0.10, deduction appears. The property therefore covers adding the first deduction.

Examples and differentials

• Reproduced exactly:

  • GN 02603.060 A.1, A.2, B.1, C.1 and C.2, plus A.5, A.8, A.9 and B.2 through the new path;
  • RS 02501.130B (the children's $83.50);
  • RS 02501.160 examples 1 and 2 (the separate-household timing);
  • RS 02501.155A.3–4.

  These are eight new registry examples. A.6 and A.7 need combined maximums and stay refused, as do the workers' compensation examples.

• Source discrepancies, both sides pinned. GN 02603.060 A.2's narrative omits the OB cap. RS 02501.160 and .130 quote OBs a dime above G's post-1982 floor.

• Cross-head differential (scripts/track_b_r2_cross_head.py). 240 previously supported R2 results, and their 240 downstream R3 results, are byte-identical to master. The six invented rows R2 used to refuse as deduction_before_reduction_part_b now compute, with no other refusal in their place.

• Conformance report. The 356,400-row G lattice is unchanged. A separate 16-row deduction denominator is added, and every one of G's 37 refusal reasons has an executed witness.

• Mutation checks. Thirteen one-line mutations were caught and reverted (docs/design/track_b_g2_r2b_mutations.json).

Source readings taken (session, under Max's 2026-10-20 delegation)

Both are logged in ~/reviews/us-hub/source-conflicts/RULINGS.md and marked at their decision lines:

• us:oasdi-ret-temporary-partial-deduction. GN 02603.050D.2 says temporary deductions are never partial, while RS 02501.160's worked example pays a partial one. G follows the example (specific over general). R2 keeps its full-month provisional suspension and refuses a provisional partial path by name.
• us:oasdi-saving-clause-operational-rate-rounding. RS 00630.400 says "rounded" without a direction, and Act 203(a)(5) requires the smallest amount that keeps the total from falling. So protected equal rates round up to the least sufficient dime (P1). LITERAL_REFUSAL remains the alternative.

The rest of the build report's judgment items are refusals by name, not readings, so none needs Max.

Round 7 (after the sixth review)

Sol's review of 3212f823 found three mediums, and all three reproduced. The session read each one against its capture before changing the rule. Two lost a lawful row by comparing a rate with an amount the declaration had already put in doubt. One kept a row no filling can make lawful.

• A declared history reaches past an omitted cohort. An omitted cohort keeps today's formula, but a declared OWN_RIB_HISTORY_BEFORE_1978 or REDUCED_BENEFIT_HISTORY_BEFORE_1978 says RS 00615.005C.2's money reduction set the amount, and that reduction can exceed today's fraction. PIA $123.40 at RF 8 in December 1977, every captured COLA through 1999 and an upward recomputation to PIA $333.30 give $318.50 on all sixteen rounding paths, against $318.40 today. That declaration raised and lost its row. It now keeps its reason and weight 7, in both directions, for an old-age benefit with a positive PIA and a remaining reduction, in a cohort before 1916 or none. Cohort 1916 keeps the cap, and a DIB keeps its PIA as its cap. Round 6's claim that only finality lifts a cap was wrong, and the note says so.
• Every test of an actual own RIB shares the carryover. Act 202(g)(1)(C) compares a mother's or father's actual own RIB, and RS 00209.001 a parent's. Round 6 opened the carryover for widow(er)s alone. A mother with own PIA $400 and a prior WIB on PIA $300 carries $359.10 against an ordinary $373.30, and the threshold of $360 sits between them. That declaration raised and lost its row. It now keeps dual_entitlement_sequence, in a pre-FRA year too. A spouse's raw own-PIA test and a child's lack of one stay settled.
• Age rules out a prior reduced benefit. RS 00615.010 says "DIB is not reduced unless there was prior entitlement to reduced RIB (or WIB prior to 1/90)", and RS 00615.005 starts those benefits no earlier than age 50. A DIB of $404.90 on PIA $405 for cohort 1975 in 2024 counted as a refusal. It now raises before evaluate_ret and leaves no row. A rate at the PIA keeps its named refusal. Workers' compensation and finality need no prior benefit, so each keeps a young row, even beside a dual declaration.

The session extended the same classes past the findings. F6 reads the same own RIB as F3, so a declared history now opens it too. REDUCED_BENEFIT_HISTORY_BEFORE_1978 opens F6 in the carryover scope, because it carries through the rule that already opened F3. The age floor covers all five holds that work through a prior reduced benefit.

One choice for the reviewer to check: the floor takes the earliest age on any route, 50, even for DIB_AFTER_REDUCED_RIB, which names a RIB that starts at 62. The schema has no separate declaration for a DIB after a reduced WIB under 404.411(b)(2), so that row stays a named refusal from 50 through 61. The direction rule decides this, and no money moves either way.

What stayed:

• An undated input with no history hold keeps today's formula. 404.411(c)(2) reduces an own RIB "by the larger of the following", so the carryover only lowers it.
• G still takes entitlement as declared, so an RIB below age 62 computes with no hold, as it did before this round, and keeps a named refusal under a carryover hold. An entitlement-age check would reach every record, so it sits outside this fix.

Sol's needs_max items each keep a standing ruling or resolve inside these fixes, so none reaches Max.

New invariants:

• History scope. Under a declared pre-1978 history, every rate on an old-age benefit with a positive PIA and a remaining reduction, in a cohort before 1916 or none, keeps its row. Past that scope, a reduction-only hold keeps the cap.
• Own-RIB tests. F6 opens under a carryover hold for exactly the roles whose test reads an actual own RIB, for cohorts before 1928 or none, and stays settled at a zero PIA. A table written out in the test checks this against G.
• Age floor. For cohort Y, F2 stays settled below the PIA in every month before January of year Y + 50, under every prior-reduced-benefit hold, and no age limits a hold that needs no such benefit. A table written out in the test checks this too.
• Young DIB. Before that floor, a DIB rate equals its PIA or raises, and it leaves no row.

Local checks at the tree that became fbe491d4: all 14,032 Track B tests pass and 7 skip in a session process. Black and ruff pass, the conformance report regenerates byte-identically, the cross-head comparison matches master, and 42 fresh mutations each failed a named test. Against 3212f823, 44 of the new module's 158 tests fail. A first mutation pass killed 39 of 43: one survivor showed a redundant month comparison, so the rule now compares years, and three exposed test gaps that each gained a test.

Round 6 (after the fifth review)

Sol's review of a135519f found three mediums, and all three reproduced. Each came from a fact table that treated a fact as wholly open or wholly settled, where the sources settle one direction of it.

• A widow's DRC clause doesn't reach a child's original rate. RS 00615.712 says "The child's original rate is $300" on a PIA that stays $400, and the clause protects the adjusted cash. A $300.10 original against OB $300 counted as a refusal. It now raises under a declared clause and under unknown history, as it does with no clause. A widow(er)'s own OB stays open, because the same page gives her $400 and, with DRCs, $410.
• A prior reduced WIB can lower an NH's own RIB. 20 CFR 404.411(c)(2) keeps the carryover before cohort 1928 and reaches someone with no current WIB. Round 5 opened this for another person's own RIB and missed the NH's. PIA $400, deceased PIA $300, WIB at 60 and RIB at 64 gives $359.10 against an ordinary $373.30. That declaration raised and lost its row. It now keeps dual_entitlement_sequence, weight kept. Cohort 1928 stays settled: "There is no further reduction."
• A reducing hold keeps its cap. A prior reduced RIB or workers' compensation can lower a DIB and can't raise it, yet a DIB of $4.10 on PIA $4 counted as a refusal. It now raises. Every reduction-only hold leaves equality open below the rate and keeps the rate as a cap. Only administrative finality lifts a cap.

The session extended the same class past the findings. Sol's exploratory probe of a DIB after a reduced WIB didn't enter its verdict, but it reproduces: $398.10 on PIA $400 raised under dual_entitlement_sequence. 404.411(b) reduces that DIB, and the schema omits the onset that scopes it, so the row now stays in every cohort. The two pre-1978 history reasons open the same comparison before cohort 1928 only, because a later cohort reached age 50 after 1977.

Protected cash stays a refusal. A child paid $300.10 on OB $300, and a deduction above that OB, keep the named refusal, because the capture states no cap on protected cash. A stricter proof could drop those rows, and no amount moves either way.

Sol's three new needs_max items are these fixes, and Sol called each source-settled, so none reaches Max.

New invariants:

• Direction. Under a reduction-only hold, an NH rate above its ordinary rate raises, and a rate at or below it keeps its row and refusal. Only finality lifts the cap.
• Carryover reach. Every rate 404.411(c)(2)(ii) can reach stays a counted refusal, with the preflight removed or not.
• Original rates. A nonwidow's OB stays settled under widow DRC protection or unknown history.
• Every reason. Each UnsupportedReason classifies a lower DIB, a lower RIB and a rate above the cap against an expectation written out in the test, not read from G's table.

Two existing assertions moved, and each now states both sides. test_protected_widow_cannot_be_excluded_from_unknown_drc_history asserts the input error and the finality refusal on the matching child. The round 4 property keeps an input error for a DIB above the PIA under workers' compensation.

Local checks at the tree that became 3212f823: all 13,874 Track B tests pass and 7 skip in a session process. Black and ruff pass, the conformance report regenerates byte-identically, the cross-head comparison matches master, and 38 fresh mutations each failed a named test. Against a135519f, 50 of the new module's 224 tests fail.

Round 5 (after the fourth review)

Sol's review of e3315baf confirmed round 3's three counterexamples, the $175 and $192.10 corrections and the composition refusal. It found one medium: a held refusal still masked contradictions in RIB gross, auxiliary original rates and widow eligibility. Reproducing that showed round 4 had already gone too far the other way, so the fix reverses part of the finding.

• The problem. RS 00615.754A.3's first example under administrative finality (PIA $750, MAX $1,312.50, NH rate $1,000, child $375.50) raised InvalidFamilyInput at e3315baf, and at 1ce508e5 it refused by name. The capture says "the rate to the NH is protected by administrative finality and cannot be changed", so a protected rate rests on a PIA other than the declared one.
• The rule. A preflight compares a fact before a held refusal only when nothing declared on the record or that beneficiary can lawfully change it. A wrong input error drops a lawful row, and a wrong refusal counts a row that shouldn't exist.
• The table. _PREFLIGHT_FACT_UNSETTLERS classifies every RecordCondition, BeneficiaryCondition and UnsupportedReason against six facts: NH original, DIB gross, RIB gross, auxiliary original, spouse raw own-PIA eligibility and other own-benefit entitlement. A new enum member fails a test until someone classifies it. Each deferred reason applies only within its own person, role, record kind and payment period.
• The check. _check_settled_family_facts compares settled facts through G's validated helpers and catches only FamilyConfigurationUnsupported. The path with the preflight removed gives the same valid outcomes and refusals.
• The deduction bound. The ordinary OB bound follows the same table, because a protected rate isn't bounded by correct-PIA OB. Strict withholding of actual gross still runs after G.

Readings this round:

• us:oasdi-finality-protected-rates-before-coverage: under finality, a rate that differs from the declared PIA stays administrative_finality, one row, weight kept. This is the session's single reading under Max's 10/20 delegation, logged in RULINGS.md.
• RS 00615.010's sole-survivor alternative can exceed ordinary OB, so a declared legacy widow's $4.10 against OB $4 keeps its historical refusal. A child's cap stays exact.
• An unresolved parent count keeps the one-parent 82.5% upper bound, because 75% and 82.5% are the only ordinary shares.

Invented examples:

• PIA $1,000, gross $800, DIB_AFTER_REDUCED_RIB: dib_after_reduced_rib, one row, weight kept. The same gross under a maximum-only hold: InvalidFamilyInput, no row.
• PIA $4, widow original and gross $3.30: eligibility_before_1983 in January 1972, because RS 00615.005A.2 set 82 1/2%. InvalidFamilyInput in January 1973, because A.5 set 100%.

Nine tests under round 4's reading split into a protected case with its exact refusal, row and weight, and a settled case that keeps the input error. No money moves: the cross-head comparison keeps all 240 R2 and 240 R3 rows, and G's conformance artifact stays byte-identical.

New invariants:

• Preflight neutrality. Removing the preflight changes no valid outcome and no refusal.
• Table completeness. Every condition and held reason has an explicit classification.
• Scope. A protection reaches only its beneficiary, month and declared conditions.

Local checks at a135519f: all 13,650 Track B tests pass and 7 skip in a session process. Black and ruff pass, the cross-head comparison matches master, and the lane's 30 mutations each failed a named test.

Round 4 (after the third review)

Sol's review of 1ce508e5 confirmed all three round-3 fixes and found three new mediums, plus a question on how two POMS exceptions compose. e3315baf fixes all four.

• Outside deductions. A divorced spouse sits outside the family maximum, but that spouse's deduction still counted as an "other deduction" under GN 02603.050A.1, so a governed child got $175 rather than $200. Act 203(a)(3)(C) and GN 02603.020B keep outside people out of the governed decision, so every decision now reads subject events only. Outside events still apply to their own cash.
• NH reservations. The same audit found an outside event was what activated a subject's NH reservation. A reservation now reduces cash with or without an event, and it still refuses with a subject's age reduction.
• Entitlement before held refusals. apply_ret_year compares declared NH entitlement with RET before it computes any G money, in both directions, so a held refusal can no longer mask a contradiction. One helper now serves G and RET. The lane's audit of the whole loop added the same preflight for spouse eligibility under the raw own-PIA test, NH original rates and DIB gross rates. The checks that need G's money stay after it.
• One cohort per person. RecordYear now rejects two known cohorts for one person, across months and across record and own-benefit fields. A missing cohort adds no constraint.
• A new refusal. GN 02603.050A.1 and A.2 don't settle how a sole full permanent deduction composes with a zero-rate dual row. sole_full_deduction_zero_dual_composition refuses only where the two readings pay differently, and the rule computes where they agree. RULINGS logs this as us:oasdi-sole-full-deduction-zero-dual-composition.

Invented examples:

• PIA $400, MAX $600, spouse RF36, child, outside divorced spouse RF60, full deductions on both: the child gets $200, and the record pays $600.
• Survivor PIA $400, MAX $600, widow, three children, outside surviving divorced spouse: each child gets $200, not $192.10.
• PIA $400, MAX $600, spouse RF36, child and zero-dual child: A.1 pays $175 and A.2-first pays $200, so the rule refuses by name, one row, weight kept.

New invariants:

• Outside independence. Outside events leave every governed payment unchanged, in any order, for all three record kinds.
• NH-only cash. It equals ordinary cash less the reservation, and outside facts can't activate a deduction.
• Composition. The refusal fires exactly when the two exact payments differ.
• Preflight. No held condition masks an NH, spouse or direct-rate contradiction, and every monthly declaration validates before the first G computation.
• Cohort. One identity has one known cohort across all month and field pairs.

Local checks at e3315baf: all 13,341 tests across the 104 Track B modules pass (7 skip), and black and ruff pass on the round's Python files. The lane's 11 new mutations were all caught. The conformance report changes only for the new reason, and 240 R2 and 240 R3 cross-head results stay unchanged. One existing test moved its reason count from 37 to 38. The tier files add this round's 637 unit tests; the coordinator's slot recount replaces them.

Round 3 (after the second review)

Sol's review of bbcdf7f4 kept every round-1 fix and reading, and found four mediums. 7fa124e3 and 872cebc7 had already fixed the stale conformance hash. 1ce508e5 fixes the other three.

• FRA against G facts. R2 accepted an FRA declaration that the family's G birth cohort contradicted, which let an own-earnings deduction run after FRA. RecordYear now checks the NH and every auxiliary against the twelve months each cohort allows, and an input error comes before any coverage refusal. Applied own delayed credits prove FRA by the snapshot month. A deceased worker's credits and old age reductions prove nothing about a survivor's age. Act 203(f)(9) and RS 02501.021B.3 apply the old-age FRA to every role, so this needed no ruling.
• Own-work event at the OB bound. A payable plus NH reservation equal to the original benefit means nothing was withheld, so that's now an input error, even on a held record.
• Divorced spouse outside the maximum. An age-reduced divorced spouse could start operational protection for people whose benefits Act 203(a)(3)(C) determines as if that spouse were absent. Operational membership, the age basis, the age trigger and the person count now skip anyone outside the maximum. That person's own rate stays ordinary, and the literal reading doesn't move.

New invariants:

• FRA classification. A declaration passes exactly when some possible birthday satisfies it, checked against an independent birthday enumeration.
• As-if-absent. Adding or removing an outside beneficiary changes no other row, protected total, refusal or guard history, in either order.

Local checks at 1ce508e5: all 12,704 tests across the 102 Track B modules pass (7 skip), and black and ruff pass on the round's Python files. The lane's 11 new mutations were all caught. All 480 literal rows and 240 R2 and 240 R3 cross-head results stay unchanged, and the conformance report regenerates byte for byte. The tier files add this round's 176 unit tests; the coordinator's slot recount replaces them.

Round 2 (after the first review)

• Two-record entitlement. With RETFamilyMonth context, R2 derives it from G's admitted own-benefit facts, for actual and estimated excess. two_record_entitlement is now optional: a value that contradicts G's facts is InvalidFamilyInput, and a consistent one refuses by name.
• No child in care. Act 203(c)(2) and 20 CFR 404.421(a) rule out a deduction from an age-reduced benefit, so NO_CHILD_IN_CARE on such a spouse is InvalidFamilyInput. The rule derives age status from supplied birth facts and delayed credits. BenefitDeduction.under_full_retirement_age is required only when those leave age unknown.
• Saving clause. A qualifying fall with a membership change at the first trigger refuses by name and keeps its denominator row. The rule checks own benefits in both the prior and the current month before it sets or extends a protection. Membership-only declines without a PIA increase stay admitted.
• R1 year. The rule looks up the R1 parameter year before it releases any held G refusal, so an unsupported year stays an input error with no denominator row.
• Zero-amount events. R2 emits only positive events, so every layer rejects a zero-amount own-work event as an input error.
• Notes. The R2 note's step 5 now describes the conditional readjustment through RETFamilyMonth. The G note, the docstring and the refusal notes now call the reservation case deferred coverage.
• Unchanged results, from the lane's ledger docs/design/track_b_g2_r2b_verification.json. All 356,400 G conformance rows are byte-identical, and the cross-head harness shows 240 R2 and 240 R3 results unchanged with the six former refusals computed. Both ran against master 1ec57a5d; the round-2 review reruns them at this head.
• Recovery note. The fix lane finished on 10-25 and left its work uncommitted, and the orchestrator recovered it from Subfleet's salvage ref on 10-31. The lane's full report no longer exists. The committed ledger and docs/design/track_b_g2_r2b_mutations.json keep its results and its 15 new mutations.
• Tiers. The counts at this head come from a three-way sum of the branch's delta and master, not a recount. The coordinator's slot recounts them.
• Local checks at bbcdf7f4. 87 tests pass across the four round-2 modules, and black and ruff pass on the 42 changed Python files. A one-off audit hook over a sample of those modules counted no opens of the barred names. CI and the round-2 review cover the rest.
• Conformance refresh at 872cebc7. CI failed at bbcdf7f4 on the byte test for docs/design/track_b_g_conformance_report.json: round 2 edited the registry YAML after the lane's last conformance run, so the report kept an old registry hash. 7fa124e3 regenerates the report. One line differs and all 356,400 rows match. 872cebc7 records the new hashes in docs/design/track_b_g2_r2b_verification.json. Neither commit changes Python.

Checks (local, at f3b9a719)

Suite	Result
G files, the four-layer notes test and the shared schema file	8,672 passed after correcting the schema file's guard-reader inventory for the new reading property
R2, R3 and birth-evidence	2,403 passed
Tier policy	passed

• Black and ruff are clean, and the conformance report regenerates byte for byte.

• Cost, measured back to back by the lane under load. G regeneration: 152 → 173 CPU seconds. R2 tests: 87 → 114 CPU seconds, for 786 → 818 tests.

• Tiers:

  Tier	Tests
  unit	18,629
  artifact	4,253
  integration_psid	1,450
  reproduction_legacy	520
  oracle_policyengine	308
  Total	25,160

• Protected files are untouched.

axiom: n/a: not a country-model change. G and R2 are Python statutory references per d515, and rulespec-us has no 42 U.S.C. 403 encoding.

🤖 Generated with Claude Code

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
social-security-model	Ready	Preview	Nov 1, 2026 12:26pm UTC