Formalize and finalize TaxingWomen: revisions from Claude Opus 4.7 review

models/We-Would-Like-In-Econ-ARK.ipynb

@@ -824,7 +824,7 @@
    }
   },
   "kernelspec": {
-   "display_name": "Python 3",
+   "display_name": ".venv-darwin-arm64",
    "language": "python",
    "name": "python3"
   },
@@ -838,7 +838,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.7.1"
+   "version": "3.12.7"
   },
   "varInspector": {
    "cols": {

models/We-Would-Like-In-Econ-ARK/TaxingWomen/AGENTS.md

@@ -0,0 +1,58 @@
+# Ballpark entry: Guner, Kaygusuz, and Ventura (2012)
+
+> Structured brief for coding agents (Claude Code, Cursor, etc.). Human-facing content lives in [`index.md`](index.md).
+
+## Paper
+
+- **Citation:** Nezih Guner, Remzi Kaygusuz, and Gustavo Ventura (2012), "Taxing Women: A Macroeconomic Analysis," *Journal of Monetary Economics* 59(1), 111–128.
+- **DOI:** [10.1016/j.jmoneco.2011.10.002](https://doi.org/10.1016/j.jmoneco.2011.10.002)
+- **Core model:** Stationary OLG with singles and married households. States are $(a, h, x, z, q, b, j)$ with $a$ assets, $h$ wife's human capital, $j$ age, and $(z, x, q, b)$ **permanent types drawn once** at birth or marriage (no within-period shocks). Controls are own labor for singles, $(l_m, l_f)$ for married households, and next-period assets $a'$. The wife's human capital evolves through a participation indicator $\chi(l) = \mathbf{1}\{l > 0\}$ (not hours). Preferences are additively separable log utility; the married-household objective is unitary with a **single** $\ln c$. Closure: revenue-neutral stationary equilibrium with log-progressive tax $\tau(\tilde y) = \zeta_1 + \zeta_2 \ln \tilde y$ whose $(\zeta_1, \zeta_2)$ switch on filing-status × presence-of-young-children (GKV 2012 Table 2).
+- **Why in-ballpark:** A serious structural evaluation of a specific policy conjecture (lower marginal tax rates on married women) that produces a sharp, counter-intuitive quantitative result — gender-based taxation is welfare-improving, but a gender-**neutral** proportional income tax dominates both the status-quo joint-filing system and gender-based taxation. The model admits a clean modular-DDSL decomposition whose `consumption_savings` stage is EGM-amenable under log utility, making it a tractable REMARK candidate.
+
+## If a user asks to work on this item
+
+1. **Read first:** [`bellman-excerpt-SMD-polished.md`](bellman-excerpt-SMD-polished.md). This is the authoritative SolvingMicroDSOPs-style statement of the within-period problem, with symbol table, per-stage perch tables (arrival / decision / continuation), the paper↔stage Rosetta Stone, stage composition proof, per-stage EGM-amenability column, and restrictions of the decomposition to singles and the retired leg. The terse Bellman equations are in [`bellman-excerpt.md`](bellman-excerpt.md); the YAML encoding is in [`dolo-plus-draft.yaml`](dolo-plus-draft.yaml). The paper's primitives in exposition form are in [`TaxingWomen_Summary.ipynb`](TaxingWomen_Summary.ipynb) §II.0.
+2. **Paper source for AI ingestion:** no `TaxingWomen.mmd` is committed yet. Link: <https://doi.org/10.1016/j.jmoneco.2011.10.002>. Before any serious re-formalization pass, fetch a Pandoc-converted `.mmd` and commit it.
+3. **Matsya thread:** `topics2026-TaxingWomen` (see [`matsya-session.txt`](matsya-session.txt)). Continue the existing thread rather than starting a new one; the permanent-types-vs-within-period-shocks correction has already been re-litigated there and need not be repeated.
+
+## Formalization status
+
+- Explicit recursive formulation: **present in `TaxingWomen_Summary.ipynb` §II**. Cell sequence: §II.0 Primitives (preferences, tax function, HC law of motion, permanent-types structure, terminal condition, equilibrium concept) → §II.1 Single male Bellman → §II.2 Single female Bellman → §II.3 Married household Bellman.
+- [`bellman-excerpt.md`](bellman-excerpt.md): **committed**. Symbol table + three Bellman equations + terse perch decomposition statement with $\mathbb{T} = \mathbb{I} \circ \mathbb{B}$ and degenerate arrival mover.
+- [`bellman-excerpt-SMD-polished.md`](bellman-excerpt-SMD-polished.md): **committed**. SMD §§12–13 style; per-stage perch tables, Rosetta Stone, composition proof, EGM-amenability by stage, singles and retired restrictions, provenance.
+- [`dolo-plus-draft.yaml`](dolo-plus-draft.yaml): **committed**. Four stages (`female_labor`, `male_labor`, `consumption_savings`, `disc`) with inline `# workaround:`, `# unresolved:`, and `# paper-verify:` flags.
+- [`verification.md`](verification.md): **committed**. Six sections: Accepted (paper-verified, GKV §2.1–§2.4 anchored); Edited (log utility per eq. (3), single $\ln c$ for unitary married objective, Tables 2 and 3); Rejected (Matsya's `ShockRealization` stage); Edited (decomposition, superseded branching variant); Unverified (DDSL-side conventions); Paper-verify pending ($\dagger$ items).
+- [`matsya-session.txt`](matsya-session.txt): **committed**; contains `topics2026-TaxingWomen`.
+- [`AGENTS.md`](AGENTS.md): this file.
+- [`index.md`](index.md): **committed** with `tier: formalized`, `has_formalization_layer: true`, and `{include}` directives for the four exposition notebooks in order.
+
+Gap against the Formalized tier: no `TaxingWomen.mmd` is committed yet; the intro notebook carries a DOI pointer as the alternative.
+
+## Known model features requiring attention in a formalization pass
+
+- **Permanent types, not shocks.** `(z, x, q, b)` are drawn once at birth/marriage; there is no Markov process on $z$ and no i.i.d. period draw on $q$. The arrival-to-decision mover is the identity on every stage and $\mathbb{T} = \mathbb{I} \circ \mathbb{B}$ with degenerate $\mathbb{I}$. Matsya's first pass (before the current thread's turn-6 clarification) invented a spurious within-period `ShockRealization` stage; it was removed, and the retraction is recorded in `verification.md`. Do not re-introduce.
+- **Two functional-form items pending paper-verification.** (i) The additive channel $(l_f + k_y\kappa)$ through which the wife's young-child time cost enters her disutility; (ii) the additive form $q\,\chi(l_f)$ of the wife's participation cost in the married-household objective. Both are consistent with the calibration in GKV 2012 Table 3 and with the authors' thread notes, but should be cross-checked against GKV 2012 eq. (3) before being treated as paper-verified. Flagged $\dagger$ in `TaxingWomen_Summary.ipynb` §II.0, in the `bellman-excerpt.md` symbol table, and as `# paper-verify:` in `dolo-plus-draft.yaml`.
+- **Married-household objective is unitary with a single $\ln c$**, not $u_f + u_m$ with $\ln c$ appearing twice. This was edited down in `verification.md` ("Edited" line) and is enforced consistently across `TaxingWomen_Summary.ipynb` §II.0, `bellman-excerpt.md`, `bellman-excerpt-SMD-polished.md`, and `dolo-plus-draft.yaml`.
+- **Tax function $\tau(\tilde y) = \zeta_1 + \zeta_2 \ln(I/\bar I)$ is singular as $I \to 0$.** Low-asset retiree grid points and zero-labor corners must be guarded. Implemented in `dolo-plus-draft.yaml` as `I_guard = max(I_total, eps_I)`. Do not drop the guard.
+- **$(\zeta_1, \zeta_2)$ parameter switching** on (filing status × young-children indicator) has no canonical dolo-plus syntax for state-computed indicators. `dolo-plus-draft.yaml` handles this by instantiating the `consumption_savings` stage four times, one per (filing, kids) cell. This is a workaround; a canonical mechanism is unresolved.
+- **Labor FOCs are implicit under the log-progressive tax.** Neither `female_labor` nor `male_labor` admits EGM inversion — the tax wedge $\zeta_2 \ln(I/\bar I)$ makes the first-order conditions implicit in the labor variable. Both stages carry `solver_hint: root_find_in_l_f` / `root_find_in_l_m` in the YAML. Only `consumption_savings` is EGM-amenable, with closed form $c = 1/(\beta\, v'_\succ)$ from log utility; this is why the YAML orders the two labor stages before the consumption-savings stage.
+- **Human-capital law of motion depends on the participation indicator $\chi(l) = \mathbf{1}\{l > 0\}$, not hours.** $h'$ moves discontinuously at the extensive margin. The single-female and married-household stages carry this transition through `consumption_savings`; the single-male problem drops $h$ entirely.
+- **Final-period continuation perch at $j = J$ is degenerate.** No bequest motive; $V_{J+1} \equiv 0$. The YAML connector's `terminal` key encodes this. Label the connector at age $J$ accordingly if the solver interface distinguishes terminal connectors.
+- **Extensive margin at $l_f = 0$ treated as a corner of the continuous optimization**, not as a branching stage on wife's $d \in \{\text{work}, \text{home}\}$. This Kuhn–Tucker treatment is the decomposition now actually in `bellman-excerpt-SMD-polished.md`; an earlier branching draft was superseded and is documented in `verification.md` (fourth line). The two formulations are mathematically equivalent when the tax function is smooth within each (filing, kids) cell.
+- **Calibration parameters** (Frisch elasticity $\gamma$, labor-disutility scale $\varphi$, $\kappa$, $\delta = 0.02$, grids for $z \in \{1,2,3,4\}$ and $x \in \{1,2,3,4\}$, Gamma parameters for $q$, the `zeta_table[filing, kids]`, $a_j^x$ profile, $d(s)$ child-care schedule, $\varpi_m(z, j)$, pensions) are partly listed as named tables in `dolo-plus-draft.yaml` and partly referenced by name in `verification.md` ("Accepted" line). They have not yet been migrated to a single committed `calibration.yaml`. The paper-anchored source is GKV 2012 Table 3.
+
+## Common next tasks (grounded)
+
+1. **Fetch `TaxingWomen.mmd`** (Pandoc-converted markdown of the paper) and commit it at the directory root. Currently only the DOI pointer in `TaxingWomen_Intro.ipynb` satisfies the paper-source requirement; the `.mmd` is preferable for AI ingestion.
+2. **Cross-verify the two `†`-flagged functional-form items** against GKV 2012 eq. (3) and the text around Table 3: (a) the additive $(l_f + k_y\kappa)$ channel and (b) the additive $q\,\chi(l_f)$ form. Update `TaxingWomen_Summary.ipynb` §II.0, `bellman-excerpt.md` symbol table, `verification.md` "Paper-verify pending" line, and `dolo-plus-draft.yaml` `# paper-verify:` block once confirmed.
+3. **Migrate calibration to `calibration.yaml`** at the directory root. Populate `phi`, `gamma`, `kappa`, `delta_h`, the `zeta_table` entries per GKV 2012 Table 2, the `a_profile` grid per Table 3, the `d_child` schedule, $\varpi_m(z, j)$, the Gamma parameters for $q \mid z$, and pensions $p_m^S, p_f^S, p^M$. Reference this file from `dolo-plus-draft.yaml` rather than keeping the parameters as free-text tables.
+4. **Expand the `singles_and_retired` block in `dolo-plus-draft.yaml`** to full stage definitions rather than the summary form currently present. Mirror the married-household structure: `male_labor → consumption_savings → disc` for single males; `female_labor → consumption_savings → disc` for single females; `consumption_savings → disc` for retired. Use the same `# workaround:` / `# unresolved:` conventions.
+5. **Write a smoke-test solver** that implements the four-stage backward sweep on a coarse grid for one permanent type and one age. Goal is not calibration-matching but stage-wiring verification: that the $\mathbb{T} = \mathbb{I} \circ \mathbb{B}$ composition reproduces the paper's single-maximization result within numerical tolerance on a toy problem.
+6. **Resolve the parameter-switching `# unresolved:` item** by proposing a canonical dolo-plus syntax for stage-level parameter switching conditional on a state-computed indicator. This is a framework-level contribution and should probably be raised as an issue upstream rather than worked around per-item forever.
+
+## Workflow reminders
+
+- **Matsya session:** continue `topics2026-TaxingWomen` (see `matsya-session.txt`). Do not re-litigate the permanent-types-vs-within-period-shocks question; it is settled.
+- **Paper verification:** Matsya output must be checked against GKV 2012 itself, not only against `TaxingWomen_Summary.ipynb`. In particular the two `†`-flagged functional-form specifics in the *Known model features* section should be independently confirmed against GKV 2012 eq. (3) before being treated as paper-verified.
+- **When flagging workarounds in YAML:** use inline `# workaround:`, `# unresolved:`, or `# paper-verify:` comments rather than silently fudging non-canonical syntax. The three known workarounds (branching-free corner treatment of the extensive margin, `I_guard` for the $\ln(I)$ singularity, stage-instantiation for $(\zeta_1, \zeta_2)$ parameter switching) are already flagged; preserve them.
+- **Single-log(c) invariant:** the unitary married-household objective uses a single $\ln c$, not $u_f + u_m$. Any edit that reintroduces a two-$\ln c$ form contradicts `verification.md` and `TaxingWomen_Summary.ipynb` §II.0 and should be rejected.