---
slug: monty-hall
passed: 2026-10-14
by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex and a Claude agent
checked: 138
confirmed: 99
wrong: 37
unverifiable: 0
observed: 0
stale: 2
---

This was the directed monty-hall repair pass against the 40 items in research/assay-line/queue-1014c/monty-hall/triage.json, with evidence re-read before each edit, source-only changes checked against the layer verifier and browser check, and the earlier checkers' CONFIRMED claims retained below. The original source record and both checker records concern f5e5f84f34; the layer files were unchanged at the requested 1f9d17a27f snapshot before this pass. No new independent Claude pass is claimed. Duplicate triage items each retain a claim and disposition, and triage decisions supersede earlier checker verdicts on the same entry.

MINOR lines count in wrong. [U+2014] denotes the original punctuation without reproducing that character. The shared one-file promise remains WRONG under note 81816d. The new verification-date source record awaits the landing's generated placard refresh. The film source is corrected, but the encoded film and all media remain untouched. Eight findings covering its three remaining claims are held as open board notes until the board issues an ID. The metadata-date and last-verified exceptions receive no separate public dated line.

## Claims

- MINOR | X1: a result that drew 10,000 letters insisting it was wrong, nearly 1,000 from PhDs | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Tierney reports about 10,000 total letters, most disagreeing, and nearly 1,000 critical letters bearing PhD signatures. Corrected the dek, historical paragraph and film source; the encoded film remains unchanged under the no-render rule.
- MINOR | X2: Every probability enumerated and simulated live. | git show f5e5f84f34:public/strata/monty-hall/index.html | The browser evaluates fixed three-door fractions and (N-1)/N, then simulates. Offline enumeration covers three doors and ten-door atoms. Both descriptions now say exact calculation compared with live simulations.
- WRONG | X3: a host who opens at random (no real evidence) updates nothing and leaves you at 1/2 | https://probability.ca/jeff/writing/montyfall.pdf | Rosenthal section 4, PDF page 4, gives posteriors 1/2, 1/2, 0 after a random goat reveal. The chosen door rises from 1/3 to 1/2. Corrected the Bayes relation and added the matching public and markdown correction.
- MINOR | X4: every probability is enumerated exactly and Monte-Carlo-checked in `research/monty-hall/verify.mjs` | git show f5e5f84f34:research/monty-hall/verify.mjs | verify.mjs enumerates three-door models and N=10 atoms; other N use exactNDoor's closed form. The markdown now distinguishes exact calculation, simulation and the finite Lean models. Matching source comments and film closing text were qualified; the encoded film was not rendered.
- STALE | X5: "dateModified":"2026-06-25" | git show f5e5f84f34:memory/log.d/2026-07-12T2320Z-monty-hall-machine-checked.md | The original page at afab40b355c already used 2026-06-25; the July 12 log records a later addition. dateModified is now 2026-10-14. The explicit metadata-date exception requires no separate Updated line because the Corrected lines date this revision.
- WRONG | X6: "uploadDate":"2026-07-09" | git show f5e5f84f34:memory/log.d/2026-06-26T1130Z-the-door-you-didnt-pick-film.md | Commit cd73cebfe37 adds film.mp4 on 2026-06-26 and the June 26 log says it is embedded. Corrected VideoObject.uploadDate to 2026-06-26 and added matching public and markdown corrections. No media bytes changed.
- MINOR | X7: Every percentage is read off those runs, beside the verifier's enumerated exact value | git show f5e5f84f34:research/monty-hall/film/film.html | film.html computes the displayed simulation percentages but uses (N-1)/N for its N-door exact values. The caption now says exact value; the film source's method comment and closing text also say exact calculation. The encoded closing text remains unchanged.
- MINOR | X8: One game tells you nothing | git show f5e5f84f34:research/monty-hall/verify.mjs; https://probability.ca/jeff/writing/montyfall.pdf | One trial cannot establish the win rate, but a car reveal can distinguish the random protocol from the classic one. Replaced the zero-information claim with the precise win-rate statement.
- MINOR | X9: that never changes, because nothing about your door is revealed. | https://probability.ca/jeff/writing/montyfall.pdf | Rosenthal sections 2 and 4 distinguish host protocols and symmetric tie breaking. The explanation now attributes the unchanged 1/3 to the classic host always showing a goat and choosing equally when both goat doors are available.
- CONFIRMED | X10: A host opening a door at random injects nothing: when he happens to miss the car (two times in three), the car is now equally likely to be behind your door or the other one, and switching gains you nothing. | https://probability.ca/jeff/writing/montyfall.pdf | REJECTED with evidence: Rosenthal section 4 gives equal posterior probabilities after a random goat reveal. In context the preceding subject is the two-thirds edge and the sentence explicitly states equal chances and no switching gain. It does not assert unchanged priors. Left unchanged, as triage directs.
- WRONG | X11: Change that rule and the answer changes with it [...] which is exactly why the puzzle has fooled so many careful people. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | Vos Savant's fourth column says most correspondents understood the conditions, while discussing this proposed explanation of the furor. Removed the unsupported historical cause, retained the mathematical dependence on the host rule, and added matching corrections.
- MINOR | X12: Every probability here is computed two independent ways and they agree: by exact enumeration of the whole game tree, and by the same seeded Monte-Carlo you can run above. | git show f5e5f84f34:research/monty-hall/verify.mjs | The verifier uses enumeration for three-door games and ten-door atoms, closed-form probabilities for other N, and independent seeded simulations. Replaced the universal game-tree enumeration claim with those actual methods.
- WRONG | X13: Re-run it yourself: bash research/monty-hall/lean/verify.sh (install Lean github-free via install-lean-nix.sh in the same folder). | git show f5e5f84f34:research/monty-hall/lean/install-lean-nix.sh; https://artwaste.land/checks/research/monty-hall/verify.mjs | Fresh fetch: the advertised /checks/research/monty-hall/lean/install-lean-nix.sh returns 404; MontyHall.lean and verify.sh return 200. The page now links the official Lean installation guide and both public files, with a same-folder bash verify.sh recipe. Downloaded files typecheck with Lean 4.35.0 and print five no-axiom footprints. Added matching corrections; no installer was run. Repair also replaced the verifier and runner installation messages with the official Lean guide.
- MINOR | X14: she estimates the magazine received some 10,000 letters insisting she was wrong | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Re-read Tierney's archived transcript: about 10,000 is the total correspondence, most disagreeing. Nearly 1,000 critical letters had PhD signatures. Corrected the historical paragraph, dek and film source; encoded film wording is not changed.
- MINOR | X15: many on university mathematics-department letterhead. | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Tierney describes mathematics and science department letterheads. Removed the unsupported university restriction and mathematics-only narrowing.
- CONFIRMED | X16: enumerated exactly, matched by simulation (see the check), and machine-checked | git show f5e5f84f34:research/monty-hall/verify.mjs | REJECTED with evidence: the surrounding apparatus states the classic and forgetful three-door rules. verify.mjs enumerates and simulates those models, and MontyHall.lean proves their counts. This contextual claim does not assert that every N is kernel checked. Left unchanged.
- MINOR | X17: Verifier: research/monty-hall/verify.mjs (exact enumeration + seeded Monte-Carlo for the knowing host, the forgetful host, and the N-door version). | git show f5e5f84f34:research/monty-hall/verify.mjs | The citation covers N-door cases, including N=50 and N=100, whose exact answers come from a formula. Changed exact enumeration to exact calculation, preserving seeded Monte-Carlo.
- WRONG | X18: verify.mjs is published, and it runs on its own: one file, and Node. | git show f5e5f84f34:public/checks/manifest.json; https://artwaste.land/checks/research/monty-hall/verify.mjs | WRONG and intentionally open under board note 81816d. The manifest's runnable recipe lists only verify.mjs; its source inventory also publishes the proof and runner. A fresh downloaded one-file run with Lean on PATH exits 1 at the missing MontyHall.lean assertion; the same published verifier with that proof beside it passes. This wording is generated by scripts/check-placard.mjs. No local change to the promise or dependency behavior.
- WRONG | X19: Last verified 25 June 2026, when it was written. | git show f5e5f84f34:memory/log.d/2026-07-12T2320Z-monty-hall-machine-checked.md | The July 12 log records JS plus live kernel ALL PASS before the September 27 commit first added this June 25 last-verified claim. This new passed: 2026-10-14 record supplies the correct source date through assay/lib.mjs. Per the triage exception, the landing must rebuild the generated placard; the old visible date is still present until then. No manual placard edit or separate dated line.
- WRONG | X20: (added) `<a href="../../../research/monty-hall/verify.mjs">verifier</a>` | https://artwaste.land/research/monty-hall/verify.mjs; https://artwaste.land/checks/research/monty-hall/verify.mjs | Fresh fetches: /research/monty-hall/verify.mjs returns 404; /checks/research/monty-hall/verify.mjs returns 200 JavaScript. Both authored links now use the published /checks/ URL. Added matching public and markdown corrections.
- MINOR | K1: a result that drew 10,000 letters insisting it was wrong, nearly 1,000 from PhDs (dek, src/content/strata/monty-hall.md line 4) | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Tierney reports about 10,000 total letters, most disagreeing, and nearly 1,000 critical letters bearing PhD signatures. Corrected the dek, historical paragraph and film source; the encoded film remains unchanged under the no-render rule.
- MINOR | K2: Every probability enumerated and simulated live. (meta description line 11, JSON-LD line 34) | git show f5e5f84f34:research/monty-hall/verify.mjs | The browser evaluates fixed three-door fractions and (N-1)/N, then simulates. Offline enumeration covers three doors and ten-door atoms. Both descriptions now say exact calculation compared with live simulations.
- MINOR | K3: flip the control the internet leaves out: if the host opens a door at random instead of knowing where the car is, switching collapses to a coin-flip (dek, src/content/strata/monty-hall.md line 4) | https://en.wikipedia.org/wiki/Monty_Hall_problem | Brilliant's Bayes discussion explicitly considers a random goat reveal and derives equal probabilities. Removed the unsupported internet-omission wording from the dek, metadata, film caption, film source and verifier/proof commentary. Encoded film text was not rendered.
- WRONG | K4: The detail most tellings leave out is that the host must know where the car is (plain, src/content/strata/monty-hall.md line 5; aw-plain meta, index.html line 187) | https://web.archive.org/web/20130121183432id_/http://marilynvossavant.com/game-show-problem/; https://mathworld.wolfram.com/MontyHallProblem.html; https://brilliant.org/wiki/monty-hall-problem/; research/assay-line/queue-1014c/monty-hall/N2-claude.md | Re-read the original column, MathWorld's setup and Brilliant's explanation: they state host knowledge or deliberate goat selection. No prevalence census supports the page's claim. Replaced it with the deciding host rule in plain frontmatter, then regenerated only this layer's aw-plain block. The shared correction makes no inverse majority claim.
- MINOR | K5: flip one control the internet keeps quiet about (meta description, index.html line 11) | https://en.wikipedia.org/wiki/Monty_Hall_problem | Brilliant explicitly explains the random-host variant. Replaced the internet-wide coverage claim with an invitation to change the host's behaviour. No public line for this MINOR item.
- WRONG | K6: the reason it isn't hides in a detail almost every telling leaves out. (page dek, index.html lines 195-196) | https://web.archive.org/web/20130121183432id_/http://marilynvossavant.com/game-show-problem/; https://mathworld.wolfram.com/MontyHallProblem.html; https://brilliant.org/wiki/monty-hall-problem/; research/assay-line/queue-1014c/monty-hall/N2-claude.md | The original question explicitly states the host knows what is behind the doors, and its clarification specifies deliberate goat selection. Replaced the unsupported almost-every-telling assertion with the host rule; added the shared correction without asserting an opposite population majority.
- WRONG | K7: The detail the internet leaves out: the host has to know (h2, index.html line 295) | https://web.archive.org/web/20130121183432id_/http://marilynvossavant.com/game-show-problem/; https://mathworld.wolfram.com/MontyHallProblem.html; https://brilliant.org/wiki/monty-hall-problem/; research/assay-line/queue-1014c/monty-hall/N2-claude.md | The original column, MathWorld and Brilliant all describe the relevant host rule. Replaced the blanket omission heading with The deciding rule, retained the old fragment ID, and added the shared correction.
- WRONG | K8: a host who opens at random (no real evidence) updates nothing and leaves you at 1/2 (relates note, src/content/strata/monty-hall.md line 12) | https://probability.ca/jeff/writing/montyfall.pdf | Rosenthal section 4, PDF page 4, gives posteriors 1/2, 1/2, 0 after a random goat reveal. The chosen door rises from 1/3 to 1/2. Corrected the Bayes relation and added the matching public and markdown correction.
- MINOR | K9: two probability classics that feel like coin-flips and aren't; both are won by counting the whole sample space instead of trusting the gut, and both are checkable live (relates note, src/content/strata/monty-hall.md line 14) | git show f5e5f84f34:src/content/strata/the-birthday-problem.md | The birthday layer describes 50.7% at 23 people as surprisingly high and has a live simulation. Changed the analogy to two counterintuitive probability classics; retained the sample-space and live-check comparison. This supersedes Codex's earlier confirmation of the loose analogy.
- MINOR | K10: every probability is enumerated exactly and Monte-Carlo-checked in `research/monty-hall/verify.mjs` (src/content/strata/monty-hall.md line 19) | git show f5e5f84f34:research/monty-hall/verify.mjs | verify.mjs enumerates three-door models and N=10 atoms; other N use exactNDoor's closed form. The markdown now distinguishes exact calculation, simulation and the finite Lean models. Matching source comments and film closing text were qualified; the encoded film was not rendered.
- STALE | K11: "dateModified":"2026-06-25" (JSON-LD, index.html line 34) | git log f5e5f84f34 -- public/strata/monty-hall/index.html | The original page at afab40b355c already used 2026-06-25; the July 12 log records a later addition. dateModified is now 2026-10-14. The explicit metadata-date exception requires no separate Updated line because the Corrected lines date this revision.
- WRONG | K12: "uploadDate":"2026-07-09" (VideoObject, index.html line 186) | git log --diff-filter=A f5e5f84f34 -- public/strata/monty-hall/film.mp4 | Commit cd73cebfe37 adds film.mp4 on 2026-06-26 and the June 26 log says it is embedded. Corrected VideoObject.uploadDate to 2026-06-26 and added matching public and markdown corrections. No media bytes changed.
- MINOR | K13: that never changes, because nothing about your door is revealed. (index.html lines 286-287) | https://probability.ca/jeff/writing/montyfall.pdf | Rosenthal sections 2 and 4 distinguish host protocols and symmetric tie breaking. The explanation now attributes the unchanged 1/3 to the classic host always showing a goat and choosing equally when both goat doors are available.
- WRONG | K14: Change that rule and the answer changes with it -- which is exactly why the puzzle has fooled so many careful people. (index.html lines 303-304) | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | Vos Savant's fourth column says most correspondents understood the conditions, while discussing this proposed explanation of the furor. Removed the unsupported historical cause, retained the mathematical dependence on the host rule, and added matching corrections.
- MINOR | K15: Every probability here is computed two independent ways and they agree: by exact enumeration of the whole game tree, and by the same seeded Monte-Carlo you can run above. (index.html lines 332-334) | git show f5e5f84f34:research/monty-hall/verify.mjs | The verifier uses enumeration for three-door games and ten-door atoms, closed-form probabilities for other N, and independent seeded simulations. Replaced the universal game-tree enumeration claim with those actual methods.
- WRONG | K16: Re-run it yourself: bash research/monty-hall/lean/verify.sh (install Lean github-free via install-lean-nix.sh in the same folder). (index.html lines 372-374) | https://artwaste.land/checks/research/monty-hall/lean/install-lean-nix.sh | Fresh fetch: the advertised /checks/research/monty-hall/lean/install-lean-nix.sh returns 404; MontyHall.lean and verify.sh return 200. The page now links the official Lean installation guide and both public files, with a same-folder bash verify.sh recipe. Downloaded files typecheck with Lean 4.35.0 and print five no-axiom footprints. Added matching corrections; no installer was run. Repair also replaced the verifier and runner installation messages with the official Lean guide.
- MINOR | K17: she estimates the magazine received some 10,000 letters insisting she was wrong (index.html line 381) | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Re-read Tierney's archived transcript: about 10,000 is the total correspondence, most disagreeing. Nearly 1,000 critical letters had PhD signatures. Corrected the historical paragraph, dek and film source; encoded film wording is not changed.
- MINOR | K18: many on university mathematics-department letterhead. (index.html lines 382-383) | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | Tierney describes mathematics and science department letterheads. Removed the unsupported university restriction and mathematics-only narrowing.
- WRONG | K19: verify.mjs is published, and it runs on its own: one file, and Node. (placard, index.html line 434) | https://artwaste.land/checks/research/monty-hall/verify.mjs | WRONG and intentionally open under board note 81816d. The manifest's runnable recipe lists only verify.mjs; its source inventory also publishes the proof and runner. A fresh downloaded one-file run with Lean on PATH exits 1 at the missing MontyHall.lean assertion; the same published verifier with that proof beside it passes. This wording is generated by scripts/check-placard.mjs. No local change to the promise or dependency behavior.
- WRONG | K20: Last verified 25 June 2026, when it was written. (placard, index.html line 435) | git show f5e5f84f34:assay/lib.mjs | The July 12 log records JS plus live kernel ALL PASS before the September 27 commit first added this June 25 last-verified claim. This new passed: 2026-10-14 record supplies the correct source date through assay/lib.mjs. Per the triage exception, the landing must rebuild the generated placard; the old visible date is still present until then. No manual placard edit or separate dated line.
- CONFIRMED | Three doors, a car, two goats: you pick one, the host opens another to show a goat, and offers the swap. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [setup-frontmatter] The column says "Behind one door is a car, behind the others, goats" and offers door #2 after opening a goat. The claim describes the same setup. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching wins two-thirds of the time | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [switch-summary] The answer says "The first door has a 1/3 chance of winning, but the second door has a 2/3 chance." Its deliberate-goat protocol is stated on the page. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Paul Erdős rejected until he saw it simulated. | https://web.archive.org/web/20140413131827id_/http://www.decisionsciences.org/DecisionLine/Vol30/30_1/vazs30_1.pdf | [erdos-summary] Read Vazsonyi's PDF, printed p. 18: "was reluctantly convinced that I was right" follows the computer simulation. The record's excerpt is authentic; its first portion is in the middle column, its second in the right column. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Play it, run ten thousand trials live | git show f5e5f84f34:public/strata/monty-hall/index.html | [live-ten-thousand] The inline runSim has "var target = 10000" and one oneGame call per iteration. Browser interaction passed; spoiled random-host games are reported separately. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | if the host opens a door at random instead of knowing where the car is, switching collapses to a coin-flip. | https://probability.ca/jeff/writing/montyfall.pdf | [random-summary] Rosenthal p. 2 says "the probabilities of winning if you stick or switch are both 1/2" for Monty Fall. This is conditional on the randomly opened door showing a goat, as the page's setup and apparatus specify. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The famous answer isn't a fact about doors: it's a fact about what the host knew. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [knowledge-thesis] The column specifies "the host always opens a losing door on purpose." The page further states the host's required behaviour, so this thesis is supported within its two models. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching wins two thirds of the time, not half. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [plain-switch] The column's "1/3 chance" and "2/3 chance" support the classic-game contrast. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the host must know where the car is; if he opens at random, switching wins about half. | https://probability.ca/jeff/writing/montyfall.pdf | [plain-host-random] Rosenthal's "both 1/2" applies after a random goat reveal. Read with the immediately preceding setup, this is the same conditional experiment. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching wins ⅔ of the time, but only if the host knows where the car is. A forgetful host makes it ½. | https://probability.ca/jeff/writing/montyfall.pdf | [social-summary] Rosenthal's "both 1/2" concerns a goat-revealing random host. The linked page states the conditioning explicitly; the social summary compresses that setup. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching wins ⅔, but only if the host knows where the car is. A forgetful host makes it ½. | https://probability.ca/jeff/writing/montyfall.pdf | [twitter-summary] Same model and condition as entry 10; Rosenthal says "both 1/2". Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | if the host opens a door at random instead of knowing where the car is, switching only wins half. | https://probability.ca/jeff/writing/montyfall.pdf | [description-random] Rosenthal p. 2 expressly says the accidental opening "just happens not to contain the car" before obtaining "both 1/2". The page supplies that qualification. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | A forgetful host who opens a door at random makes switching win only half. | https://probability.ca/jeff/writing/montyfall.pdf | [structured-description-random] Rosenthal's Monty Fall calculation is conditional on the observed goat. The page's apparatus and simulator specify this condition. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the host opening a goat door is new evidence, and switching is just Bayes' theorem updating your odds from 1/3 to 2/3 | https://probability.ca/jeff/writing/montyfall.pdf | [bayes-update] Rosenthal p. 4 gives updated door probabilities "1/3, 2/3, and 0". The remaining unchosen door rises from 1/3 to 2/3; the original choice stays at 1/3. Read "odds" here as informal probability, not odds ratios. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | both hand a finite claim to Lean's kernel by `decide` over an exhaustive space (there, every Boolean input to a sorting network; here, every equiprobable atom of the game). | git show f5e5f84f34:src/content/strata/two-symbols-are-enough.md | [related-lean] The linked sorting-network page says its "kernel runs the 2ⁿ test itself". MontyHall.lean uses "by decide" on finite lists. Both finite certificates match the comparison. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | that the answer is 2/3 under a knowing host and 1/2 under a forgetful one | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [related-host-proof] The theorem contains "classicSwitchCount * 3 = classicAtoms.length * 2" and "forgetSwitchCount * 2 = forgetGoatCount * 1". Lean accepted it; the forgetful probability is conditioned on a goat. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | **machine-checked** in `research/monty-hall/lean/MontyHall.lean` (Lean, zero imports, no axioms) | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [md-lean] The complete Lean file has no explicit imports and uses finite "by decide" proofs. The live proof run prints "does not depend on any axioms" for all five displayed footprints. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the kernel re-derives the exact counts and proves the knowing host gives switch = 2/3 while the forgetful host gives 1/2. | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [md-counts] The live Lean run accepts "the_host_protocol_decides" and the independently recomputed integer counts are 12/18 and 6/12. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The full page is at the `href` above. | git show f5e5f84f34:public/strata/monty-hall/index.html | [md-location] The supplied href resolves with HTTP 200 and the served page contains "The Door You Didn't Pick". Its substantive HTML matches the pinned page. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | date: 2026-06-25 | git log f5e5f84f34 -- public/strata/monty-hall/index.html | [publication-date] first commit afab40b355c, 2026-06-25T06:39Z, "Add 'The Door You Didn't Pick'". Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | `<meta property="og:image" content="https://artwaste.land/og/monty-hall.png" /> <meta property="og:image:width" content="1200" /> <meta property="og:image:height" content="630" />` | git show f5e5f84f34:public/og/monty-hall.png | [social-image-size] Reading the pinned PNG IHDR gives width 1200 and height 630. The literal metadata values match the image. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | A car behind one, a goat behind each of the others. You choose; the host opens a different door to show a goat; then he offers you the swap. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [setup-body] The column's three-door setup, deliberate goat opening, and offer "Do you want to pick door #2?" match the body. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | companion film, 2:36 | https://artwaste.land/strata/monty-hall/film.mp4 | [film-duration] ffprobe on the live file: duration=156.000000; film.html DUR = 156. Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The film is at film.mp4 (MP4 / H.264 + AAC). | git show f5e5f84f34:research/monty-hall/film/build.sh | [film-format] The build uses "-c:v libx264" and "-c:a aac". ffprobe of the live file independently reports "h264", "aac", and an MP4 container, at 1920 by 1080. The 8.8 MB temporary download was deleted. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The games on screen are the same seeded simulation the verifier runs | git show f5e5f84f34:research/monty-hall/film/film.html | [film-shared-simulation] The film ports the same mulberry32, car/pick draws, legal host choices, and remaining-door logic as the verifier. It uses 10,000 trials and separately seeded batches, rather than the verifier's 400,000-trial continuing stream. "Same simulation" is supported as the same algorithm, not identical output batches. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the music is a minor-pentatonic bed whose beat hits when switching would have won | git show f5e5f84f34:research/monty-hall/film/make-audio.mjs | [film-audio] The audio code defines "PENTA = [1, 6/5, 4/3, 3/2, 9/5]" and "out[b] = (other===car) ? 1 : 0". A winning switch accents the beat through "acc[b]?0.32:0.11". The claim does not say losing beats are silent. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | He always opens a door with a goat | git show f5e5f84f34:public/strata/monty-hall/index.html | [knowing-host-behavior] The host filters "goats = others.filter(function (d) { return d !== state.car; })". It opens only one of those goats; the browser also confirms one open goat. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | never the car, never yours. (The classic game.) | git show f5e5f84f34:public/strata/monty-hall/index.html | [knowing-exclusions] The host starts with doors "d !== i" and then excludes "state.car". Thus neither the selected door nor the car can open in knowing mode. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | He opens one of the other doors at random | git show f5e5f84f34:public/strata/monty-hall/index.html | [random-host-behavior] The random branch uses "state.open = others[rint(others.length)]" with the other two doors equally weighted. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | and sometimes blows it, revealing the car. | git show f5e5f84f34:public/strata/monty-hall/index.html | [random-host-car] The explicit branch "!hostKnows && state.open === state.car" displays the car and sets "state.phase = 'void'". The exact independent count is 6/18. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | let the machine do what no contestant ever could: play the same game ten thousand times. | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | [no-contestant] Monty Hall was "the host of 4,500 programs of 'Let's Make A Deal' from 1963 to 1990": the whole show ran fewer than 10,000. The record found no source; its own NYT transcript holds this one. Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Uses the host behaviour you selected above: | git show f5e5f84f34:public/strata/monty-hall/index.html | [sim-host-selection] oneGame() branches on the shared "hostKnows" state. The browser changes the mode and observes switching move from about 66.7% to about 50%. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Run 10,000 games | git show f5e5f84f34:public/strata/monty-hall/index.html | [sim-run-button] runSim() sets "target = 10000" and loops exactly that many attempted games. The displayed denominator correctly excludes spoiled games. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Press run. With a knowing host, switching should land near 66.7%. | git show f5e5f84f34:public/strata/monty-hall/index.html | [sim-expected-initial] theoretical() returns "2 / 3" for a knowing switcher. Its formatted expectation is 66.7%; the local browser's seeded run is 65.6%, within ordinary sampling variation and the original verifier's tolerance. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | A chart of the running win rate as games accumulate, settling onto the exact theoretical probability shown as a dashed line. | git show f5e5f84f34:public/strata/monty-hall/index.html | [sim-chart] drawConv() plots running samples and sets "setLineDash([5 * S, 5 * S])" for the exact theory line. The browser confirms a nonzero canvas and valid simulation output. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Your first pick is right one time in three | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [initial-one-third] The column says "The first door has a 1/3 chance of winning". Uniform initial placement gives the same result directly. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | So a strategy of staying wins exactly 1/3. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [stay-one-third] The column's "first door has a 1/3 chance of winning" and exact enumeration both support staying at 1/3 under the classic protocol. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The car is behind one of the other two doors the remaining 2/3 of the time | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [other-two-thirds] The column says "a 2/3 chance that it’s behind one of the others". The three equally likely initial car locations make this immediate. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the host, by opening the goat among them, quietly sweeps that entire two-thirds onto the single door he leaves closed. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [host-sweeps] The column says "when you switch, you win if the prize is behind #2 or #3". The knowing host's removal preserves those two winning initial cases. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching doesn't gamble on one door; it collects both of the doors you didn't pick, minus the goat the host kindly removed. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [collect-both] The column's "You win either way!" concerns the car in either originally unchosen door. This is the correct grouped-event explanation. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the host's open door is not new randomness [...] it's a concentrated clue. | https://probability.ca/jeff/writing/montyfall.pdf | [concentrated-clue] Rosenthal's host likelihoods "1/2, 1, and 0" yield posteriors "1/3, 2/3, and 0". The reveal is informative despite its random tie-breaking. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Flip the toggle to “Host forgets” and run ten thousand games. Switching drops to a coin-flip [...] 1/2. Nothing about your choice changed. | git show f5e5f84f34:public/strata/monty-hall/index.html | [toggle-half] The simulator's random branch discards car openings and theory says "return 1 / 2". The rendered hint explicitly says "counting only games where a goat was shown"; the observed rate is 51.2%. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The two-thirds edge was never really yours; it was information the host injected by deliberately avoiding the car. | https://probability.ca/jeff/writing/montyfall.pdf | [host-injected-information] Rosenthal's likelihoods "1/2, 1, and 0" explain why deliberately avoiding the car makes the remaining unchosen door preferable. The mathematical edge is supported. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The famous answer “always switch” is not a fact about doors. It is a fact about a host who knows where the car is and is bound to reveal a goat. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [always-switch-rule] Vos Savant specifies "the host always opens a losing door on purpose". The page separately supplies the always-offers-switch condition, so its protocol qualification is supported. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The host throws open every goat door but one, then offers the swap. | git show f5e5f84f34:public/strata/monty-hall/index.html | [ndoor-opening-rule] There are N−1 goat doors and the host opens N−2 of them, leaving exactly one goat door closed along with the car. The preserved goat is the original selection when that selection is a goat, or the other closed door when the original selection is the car. runND() implements this correctly. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Switching wins 2 / 3 = 66.7%. | git show f5e5f84f34:public/strata/monty-hall/index.html | [ndoor-default] renderND() computes "num = N - 1, den = N". At the default N=3 this is 2/3, formatted as 66.7%. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | your one-in-a-hundred guess | https://www.montyhallproblem.com/as.html | [hundred-door-first-pick] The excerpt gives the generalized switching probability "(n-1)/[n(n-p-1)]", not the initial-choice probability. Under the explicitly uniform N-door model the initial choice is correct in 1 of 100 positions. The page is correct, but the record's excerpt is indirect support. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Run 5,000 You pick one. | git show f5e5f84f34:public/strata/monty-hall/index.html | [ndoor-run-button] runND() sets "trials = 5000" and chooses one pick per trial. The source-record claim joins the button label and the next sentence, both present on the page. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Knowing host: staying wins 1/3, switching wins 2/3 | git show f5e5f84f34:research/monty-hall/verify.mjs | [classic-check-counts] The pinned run prints "exact: classic stay wins 1/3 =0.333333" and "exact: classic switch wins 2/3 =0.666667". Independent integer counts are 6/18 and 12/18. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Forgetful host: among games where a goat is shown, staying and switching each win 1/2 [...] and the host reveals the car outright in 1/3 of all games. | git show f5e5f84f34:research/monty-hall/verify.mjs | [forgetful-check] Recomputed counts are 12 goat reveals, 6 stay wins, 6 switch wins, and 6 car reveals out of 18 atoms. The conditional 1/2 and unconditional 1/3 are correct. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | N doors, knowing host opening all but one other: switching wins (N−1)/N [...] 2/3 at N=3, 0.99 at N=100 (simulation matches each). | git show f5e5f84f34:research/monty-hall/verify.mjs | [ndoor-check] The formula is "switch: (N - 1) / N". Simulations print 0.6670, 0.9002, 0.9798, and 0.9903 for N=3,10,50,100. The arithmetic and claimed agreement are correct. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | a switcher wins twice as often as a stayer in the classic game | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [double-win] Vos Savant says "you win 2/3 of the time" when switching and "only win 1/3" without switching. Their ratio is exactly 2. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The check above enumerates the game tree [...] once, in JavaScript, in arithmetic you have to take on trust. | git show f5e5f84f34:research/monty-hall/verify.mjs | [js-enumeration] exactClassic() and exactForgetful() iterate car, pick, and host choice with weights. The described JavaScript game-tree enumeration exists; the more general N-door scope is separately qualified in entries 26/70. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Below the same counts are handed to Lean's kernel, a proof anyone can re-run. | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [lean-repeatable] The proof uses "by decide" and a live Lean run accepts all theorems. A downloaded MontyHall.lean also typechecks using the published /checks/verify.sh; discoverability of those files is a separate entry 87 finding. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The model is identical (an equiprobable atom space, so a plain count is a probability), but now the machine decides it, for every case at once, and [...] the point of this page [...] proves the two host protocols give two different answers: | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [model-identical] The Lean atoms are car × pick × tie, with 18 equally weighted states. The unused tie bit duplicates forced host moves, preserving the JS weights 1/9 and 1/18. Both protocols are equivalent to the numerical verifier's models. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | -- research/monty-hall/lean/MontyHall.lean (zero imports; the kernel alone) theorem the_host_protocol_decides : classicSwitchCount * 3 = classicAtoms.length * 2 -- knowing host: switch = 2/3 ∧ forgetSwitchCount * 2 = forgetGoatCount * 1 -- forgetful host: switch = 1/2 ∧ forgetGoatCount = 12 ∧ forgetCarRevealedCount = 6 -- car blown 1/3 of the time := by decide | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [displayed-theorem] The displayed theorem agrees with the Lean file's logical statement and "by decide". The comment's shorter wording has no mathematical effect. Lean accepts the exact statement. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Each count is a finite enumeration the kernel evaluates itself (by decide) [...] no sampling, no floating point, no imported library. | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [kernel-finite] The proof definitions use finite lists of Nat, Boolean filters, and "by decide". No explicit import, floating-point operation, sampling, or unproved axiom occurs in the proof. Positive control for source inspection: all 13 theorem declarations and five #print axioms commands were located. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Knowing host (18 equiprobable atoms): switch wins 12/18 = 2/3, stay wins 6/18 = 1/3 [...] and the host reveals a goat on all 18 (never your door, never the car). | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [kernel-knowing] The proof asserts "classic_total : classicAtoms.length = 18", "classicSwitchCount = 12", and "classicStayCount = 6". Its validity theorem checks all 18 host openings; the live proof and JS counts agree. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Forgetful host (same 18): the car is blown outright in 6/18 = 1/3; conditioned on a goat, switch and stay each win 6/12 = 1/2. The edge is gone [...] no door, car, or goat moved, only what the host knew. | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [kernel-forgetful] The proof asserts "forgetCarRevealedCount = 6" and "forgetGoatCount = 12" and proves both conditional half ratios. Same doors and placements, different host protocol; the conditioning is stated explicitly. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Ten doors, knowing host (100 atoms): switch wins 90/100 = 9/10. | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [kernel-ten] The theorem asserts "(ndoorAtoms 10).length = 100" and a 9/10 win ratio. The independently recomputed switch count is 90. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The JavaScript verifier recomputes these integer counts and, when Lean is present, drives the proof live. | git show f5e5f84f34:research/monty-hall/verify.mjs | [js-drives-lean] The verifier invokes "lean" when it is on PATH, recomputes all ten integer counts, and checks the output for "does not depend on any axioms". The complete pinned run exercised that branch and passed. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | in her Parade column in 1990 | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [savant-1990] Vos Savant's page says the material was "originally published in PARADE magazine in 1990 and 1991". Tierney's July 1991 article dates the initial column to "last September", supporting 1990 specifically. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | close to 1,000 of them from PhD holders | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | [phds] Tierney says "close to 1,000 carried signatures with Ph.D.'s". This matches the count and type of correspondent. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Paul Erdős, one of the most prolific mathematicians who ever lived | https://sites.google.com/oakland.edu/grossman/home/the-erdoes-number-project/information-about-the-erdoes-number-project | [erdos-prolific] The Erdős Number Project calls Erdős "incredibly prolific" and describes hundreds of research papers. This supports the qualitative claim about exceptional output. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | refused to accept the result until a colleague showed him a computer simulation of it | https://web.archive.org/web/20140413131827id_/http://www.decisionsciences.org/DecisionLine/Vol30/30_1/vazs30_1.pdf | [erdos-simulation] Vazsonyi's first-person account describes his computer simulation and says Erdős "was reluctantly convinced that I was right". It distinguishes accepting the numerical result from understanding the reason later explained by Ron Graham. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the very thing you just ran. | git show f5e5f84f34:public/strata/monty-hall/index.html | [very-simulation] The inline page contains an actual Monte Carlo runSim(). "The very thing" is correct as a computer simulation of the same puzzle, not a claim to use Vazsonyi's original software. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The problem had been posed and correctly solved fifteen years earlier, in 1975, by the statistician Steve Selvin in a pair of letters to The American Statistician | https://www.montyhallproblem.com/as.html | [selvin-1975] Selvin's second letter identifies his February 1975 "A Problem in Probability" and again states the switching probability "2/3". It is labelled August 1975, Vol. 29, No. 3, and signed Steve Selvin. 1990−1975=15. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | his second letter is the first known use of the name “Monty Hall problem,” | https://en.wikipedia.org/wiki/Monty_Hall_problem | [selvin-first-name] The cited Wikipedia section says "The second appears to be the first use of the term". The primary second-letter transcript is titled "On the Mony Hall Problem" (a transcription typo). "First known" properly preserves the historical qualification. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | after the host of the game show Let's Make a Deal. | https://en.wikipedia.org/wiki/Monty_Hall_problem | [name-host] Wikipedia says it is "named after its original host, Monty Hall". Tierney's interview independently identifies Hall as host of Let's Make a Deal. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | “Always switch” requires that the host (a) always opens a door, (b) always opens one with a goat, never the car or your door, and (c) always offers the switch regardless of your first pick. | https://en.wikipedia.org/wiki/Monty_Hall_problem | [standard-assumptions] Wikipedia explicitly lists the three "must always" conditions for unselected door, goat, and switch offer. Vos Savant's clarification and the page's implementations agree. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | These are the standard assumptions of the puzzle; vos Savant later clarified them after the controversy, because a host with other habits gives other answers. | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [clarified-rules] Vos Savant's later discussion specifies "the host always opens a losing door on purpose" and says "Anything else is a different question." This supports the clarification of the rules. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The “Host forgets” toggle drops assumption (b) and the answer moves to 1/2 | git show f5e5f84f34:public/strata/monty-hall/index.html | [toggle-drops-b] The random branch allows opening the car and discards that spoiled game; its goat-reveal subset has 1/2 switch probability. The full paragraph is clarified by the simulator's conditional hint. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | A host who only offers the switch when you've picked the car could make switching lose every time | https://en.wikipedia.org/wiki/Monty_Hall_problem | [adversarial-host] Wikipedia's host-variant table says "Switching always yields a goat" when the host offers a switch only after an initially winning choice. Directly, switching away from a car must lose. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | that adversarial case is named here but not simulated. | git show f5e5f84f34:public/strata/monty-hall/index.html | [adversarial-not-simulated] Read all three game implementations and host controls. The complete host branch is knowing versus random, with no adversarial offer-selection mode. Positive control: the same inspection locates both "Host knows" and "Host forgets" and their handlers. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The probabilities are proven for the stated rules | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [proof-scope] The finite model explicitly proves the stated knowing and forgetful ratios, with N=10 separately proved. The broad N-door formula is mathematically valid, but its enumeration coverage is separately corrected in entries 105/112. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Lean's kernel re-derives the same counts with zero imports and no axioms (research/monty-hall/lean/MontyHall.lean). | git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [proof-zero-imports] The full Lean file and live axiom footprints support the no-explicit-import, no-axiom claim for its stated finite models. Positive control: #print axioms the_host_protocol_decides was found and executed. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | vos Savant's letter counts are her own estimate. | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | [letter-estimates] Tierney attributes the total with "Ms. vos Savant estimates" and describes the PhD count among letters she received. The attribution is accurately characterized as an estimate, not an audited census. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Wikipedia, “Monty Hall problem” | https://en.wikipedia.org/wiki/Monty_Hall_problem | [wikipedia-citation] The fetched article is titled "Monty Hall problem". HTTP 200, with substantive article text rather than a challenge page. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the standard assumptions, vos Savant's 1990 Parade column and the ≈10,000-letter response, Paul Erdős's simulation, and Steve Selvin's 1975 American Statistician letters. | https://en.wikipedia.org/wiki/Monty_Hall_problem | [wikipedia-contents] Read the whole cited article: its introduction covers the 1990 column, approximately 10,000 letters, Erdős's simulation, and Selvin's 1975 letters; its "Standard assumptions" section gives the rules. All listed content is present. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Origin: S. Selvin, “A Problem in Probability,” The American Statistician 29(1), 1975. | https://en.wikipedia.org/wiki/Monty_Hall_problem | [selvin-citation] Wikipedia lists "Selvin, Steve (February 1975a)" and "The American Statistician. 29 (1)". Selvin's August letter independently names his earlier "A Problem in Probability". The title, author initial, journal, issue, and year match. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Probability is the branch of mathematics our intuition is worst at (index.html line 421) | https://web.archive.org/web/20250101000000/https://www2.math.upenn.edu/~kazdan/210/notes-misc/Monty_Hall.html | [intuition-worst] Martin Gardner (1959) as quoted by Tierney: "in no other branch of mathematics is it so easy for experts to blunder as in probability theory." An expert judgment, not a measurement. The record found no source; its own NYT transcript holds this one. Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | this is one of the Wasteland's largest veins. | git show f5e5f84f34:src/pages/probability.astro | [large-vein] recount at the pin: 117 of 1,110 published layers carry probability or statistics (the hub's membership rule); among subject tags only mathematics (150) and physics (126) are larger. Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | 99%-accurate test that's a coin-flip | git show f5e5f84f34:src/content/strata/bayes-theorem.md | [related-test] The linked layer specifies a "99% accurate" test and "a disease 1 in 100 people carry". With sensitivity and specificity both .99, true positives .0099 and false positives .0099 give exactly .5. This is the toy numerical model, not a general medical claim. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | pure chance draws for free | git show f5e5f84f34:src/content/strata/drawn-by-nothing.md | [related-chance-chart] The linked Drawn by Nothing page says "Set every real cause to zero" and describes the Dunning-Kruger scissors generated from random data. It supports the qualitative claim about that linked chart; no additional numerical claim is imported here. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The whole vein, walked movement by movement, is gathered at The Paradoxes of Chance. | git show f5e5f84f34:src/pages/probability.astro | [probability-hub] The pinned hub has "MEMBER_TAGS = ['probability', 'statistics']", a curated MOVEMENTS list, and a remainder for other members. Its displayed title is "The Paradoxes of Chance". This supports the collection claim under its stated tag rule. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | This layer's check opens this page in a real browser and drives it. | git show f5e5f84f34:verify-monty-hall.mjs | [browser-check] The original browser verifier launches chromium, visits its locally served Monty Hall page, clicks doors and host/strategy controls, and checks output. With only import, local root, executable path, and server-port adaptations, all 21 original checks passed. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | It is reading what you are reading. | git show f5e5f84f34:verify-monty-hall.mjs | [reads-page] The browser verifier reads the built page at "/strata/monty-hall/" and checks live DOM output. The pinned page and live body match. This describes reading the rendered interaction, not coverage of every explanatory sentence. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Rung 1 of the portal [...] the dropped condition is the host's PROTOCOL. | git show f5e5f84f34:src/content/strata/the-condition-you-werent-told.md | [portal-rung] The linked portal's relates entry explicitly says "Rung 1 of the portal" and "the host's PROTOCOL". The displayed relation accurately describes that portal's first example. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | this is the third of the time his ignorance shows. | git show f5e5f84f34:research/monty-hall/verify.mjs | [void-one-third] The pinned exact run prints "a forgetful host reveals the car outright 1/3 of the time" and the atom count is 6/18. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | (It doesn’t count toward your tallies.) | git show f5e5f84f34:public/strata/monty-hall/index.html | [void-no-tally] The spoiled-game branch sets "state.phase = 'void'" and returns before finish() increments any tally. The existing tally is preserved, with no count for this void game. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Press run. With a forgetful host, switching should land near 50% (counting only games where a goat was shown). | git show f5e5f84f34:public/strata/monty-hall/index.html | [script-forgetful-half] The rendered hint was read in the local browser after selecting the random host and switch strategy. It exactly matches the claim; the conditional simulation also lands near 50%. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Press run. With a knowing host, staying should land near 33.3%. | git show f5e5f84f34:public/strata/monty-hall/index.html | [script-stay-third] The rendered hint was read after selecting the knowing host and stay strategy. It exactly matches the claim, and the browser run gave 33%. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | Press run. With a forgetful host, staying should land near 50% (counting only games where a goat was shown). | git show f5e5f84f34:public/strata/monty-hall/index.html | [script-forgetful-stay] The rendered hint was read after selecting the random host and stay strategy. It exactly matches the claim; the independent conditional counts are 6/12. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | The smartest people in the world got this wrong | https://web.archive.org/web/20130121183432/http://marilynvossavant.com/game-show-problem/ | [smartest-heading] Vos Savant publishes PhD correspondents' objections, including "many of my academic colleagues have also been stumped". Vazsonyi documents Erdős's objection. This supports the heading's ordinary qualitative meaning of highly accomplished people getting it wrong; it is not a literal measured intelligence ranking. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | the 2/3, heard. | git show f5e5f84f34:research/monty-hall/film/make-audio.mjs | [film-heard-two-thirds] Recreated the seeded accent schedule without rendering audio: 113 winning-switch accents over 171 beats, 66.0819%, matching the log's "density **66.1%**". This is a sonification of a run with theoretical win rate 2/3, not an assertion that this finite sample is exactly 2/3. Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | (added) Both expose optimal as a conditional word whose meaning changes when the question changes. | git show f5e5f84f34:src/content/strata/mastermind-five-guesses.md; git show f5e5f84f34:research/monty-hall/lean/MontyHall.lean | [added-mastermind-relation] [added-mastermind-relation] index.html:455 contains this omitted relation. The linked page says "The two strategies optimize different quantities" and distinguishes worst-case from expected-case Mastermind play. Monty Hall gives different optimal decisions under different host protocols. The qualitative comparison is supported; its exact words are absent from the supplied record, while the adjacent portal relation is present (positive control). Carried from N2-codex.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | (added) The answer feels like a coin-flip and isn't (page dek, index.html line 195) | https://probability.ca/jeff/writing/montyfall.pdf | [added-coin-flip] p. 1: "Most people believe, upon first hearing this problem, that the car is equally likely to be behind either of the two unopened doors, so the probability of winning is 1/2"; Wikipedia: "an overwhelming majority of people assume that each door has an equal probability". Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- CONFIRMED | (added) At 100 doors the host all but points at the car (index.html line 325) | git show f5e5f84f34:research/monty-hall/verify.mjs | [added-hundred-doors] N=100: exact 0.9900, simulation 0.9903 (recreated). Carried from N2-claude.md; earlier source re-read at f5e5f84f34.
- MINOR | F1: The verdict: only the kernel and two propositional axioms. | research/monty-hall/lean/MontyHall.lean; research/assay-line/queue-1014c/monty-hall/N2-claude.md | The checker also flagged this source comment. The five actual Lean 4.35.0 footprints report no axioms. Corrected the comment only; theorem statements are unchanged.

## Findings

- [open note:22b88d] X1: Tierney reports about 10,000 total letters, most disagreeing, and nearly 1,000 critical letters bearing PhD signatures. Corrected the dek, historical paragraph and film source; the encoded film remains unchanged under the no-render rule. At 01:11 the encoded film still describes all 10,000 letters as dissenting; board note needed.
- [fixed] X2: The browser evaluates fixed three-door fractions and (N-1)/N, then simulates. Offline enumeration covers three doors and ten-door atoms. Both descriptions now say exact calculation compared with live simulations.
- [fixed] X3: Rosenthal section 4, PDF page 4, gives posteriors 1/2, 1/2, 0 after a random goat reveal. The chosen door rises from 1/3 to 1/2. Corrected the Bayes relation and added the matching public and markdown correction.
- [open note:22b88d] X4: verify.mjs enumerates three-door models and N=10 atoms; other N use exactNDoor's closed form. The markdown now distinguishes exact calculation, simulation and the finite Lean models. Matching source comments and film closing text were qualified; the encoded film was not rendered. At 02:34 the encoded film still says exact enumeration; board note needed.
- [dated] X5: The original page at afab40b355c already used 2026-06-25; the July 12 log records a later addition. dateModified is now 2026-10-14. The explicit metadata-date exception requires no separate Updated line because the Corrected lines date this revision.
- [fixed] X6: Commit cd73cebfe37 adds film.mp4 on 2026-06-26 and the June 26 log says it is embedded. Corrected VideoObject.uploadDate to 2026-06-26 and added matching public and markdown corrections. No media bytes changed.
- [open note:22b88d] X7: film.html computes the displayed simulation percentages but uses (N-1)/N for its N-door exact values. The caption now says exact value; the film source's method comment and closing text also say exact calculation. The encoded closing text remains unchanged. At 02:34 the encoded film still says exact enumeration; board note needed.
- [fixed] X8: One trial cannot establish the win rate, but a car reveal can distinguish the random protocol from the classic one. Replaced the zero-information claim with the precise win-rate statement.
- [fixed] X9: Rosenthal sections 2 and 4 distinguish host protocols and symmetric tie breaking. The explanation now attributes the unchanged 1/3 to the classic host always showing a goat and choosing equally when both goat doors are available.
- [fixed] X11: Vos Savant's fourth column says most correspondents understood the conditions, while discussing this proposed explanation of the furor. Removed the unsupported historical cause, retained the mathematical dependence on the host rule, and added matching corrections.
- [fixed] X12: The verifier uses enumeration for three-door games and ten-door atoms, closed-form probabilities for other N, and independent seeded simulations. Replaced the universal game-tree enumeration claim with those actual methods.
- [fixed] X13: Fresh fetch: the advertised /checks/research/monty-hall/lean/install-lean-nix.sh returns 404; MontyHall.lean and verify.sh return 200. The page now links the official Lean installation guide and both public files, with a same-folder bash verify.sh recipe. Downloaded files typecheck with Lean 4.35.0 and print five no-axiom footprints. Added matching corrections; no installer was run. Repair also replaced the verifier and runner installation messages with the official Lean guide.
- [open note:22b88d] X14: Re-read Tierney's archived transcript: about 10,000 is the total correspondence, most disagreeing. Nearly 1,000 critical letters had PhD signatures. Corrected the historical paragraph, dek and film source; encoded film wording is not changed. At 01:11 the encoded film still describes all 10,000 letters as dissenting; board note needed.
- [fixed] X15: Tierney describes mathematics and science department letterheads. Removed the unsupported university restriction and mathematics-only narrowing.
- [fixed] X17: The citation covers N-door cases, including N=50 and N=100, whose exact answers come from a formula. Changed exact enumeration to exact calculation, preserving seeded Monte-Carlo.
- [open note:81816d] X18: WRONG and intentionally open under board note 81816d. The manifest's runnable recipe lists only verify.mjs; its source inventory also publishes the proof and runner. A fresh downloaded one-file run with Lean on PATH exits 1 at the missing MontyHall.lean assertion; the same published verifier with that proof beside it passes. This wording is generated by scripts/check-placard.mjs. No local change to the promise or dependency behavior.
- [fixed] X19: The July 12 log records JS plus live kernel ALL PASS before the September 27 commit first added this June 25 last-verified claim. This new passed: 2026-10-14 record supplies the correct source date through assay/lib.mjs. Per the triage exception, the landing must rebuild the generated placard; the old visible date is still present until then. No manual placard edit or separate dated line.
- [fixed] X20: Fresh fetches: /research/monty-hall/verify.mjs returns 404; /checks/research/monty-hall/verify.mjs returns 200 JavaScript. Both authored links now use the published /checks/ URL. Added matching public and markdown corrections.
- [open note:22b88d] K1: Tierney reports about 10,000 total letters, most disagreeing, and nearly 1,000 critical letters bearing PhD signatures. Corrected the dek, historical paragraph and film source; the encoded film remains unchanged under the no-render rule. At 01:11 the encoded film still describes all 10,000 letters as dissenting; board note needed.
- [fixed] K2: The browser evaluates fixed three-door fractions and (N-1)/N, then simulates. Offline enumeration covers three doors and ten-door atoms. Both descriptions now say exact calculation compared with live simulations.
- [open note:22b88d] K3: Brilliant's Bayes discussion explicitly considers a random goat reveal and derives equal probabilities. Removed the unsupported internet-omission wording from the dek, metadata, film caption, film source and verifier/proof commentary. Encoded film text was not rendered. At 01:52 the encoded film still says the internet leaves the control out; board note needed.
- [fixed] K4: Re-read the original column, MathWorld's setup and Brilliant's explanation: they state host knowledge or deliberate goat selection. No prevalence census supports the page's claim. Replaced it with the deciding host rule in plain frontmatter, then regenerated only this layer's aw-plain block. The shared correction makes no inverse majority claim.
- [fixed] K5: Brilliant explicitly explains the random-host variant. Replaced the internet-wide coverage claim with an invitation to change the host's behaviour. No public line for this MINOR item.
- [fixed] K6: The original question explicitly states the host knows what is behind the doors, and its clarification specifies deliberate goat selection. Replaced the unsupported almost-every-telling assertion with the host rule; added the shared correction without asserting an opposite population majority.
- [fixed] K7: The original column, MathWorld and Brilliant all describe the relevant host rule. Replaced the blanket omission heading with The deciding rule, retained the old fragment ID, and added the shared correction.
- [fixed] K8: Rosenthal section 4, PDF page 4, gives posteriors 1/2, 1/2, 0 after a random goat reveal. The chosen door rises from 1/3 to 1/2. Corrected the Bayes relation and added the matching public and markdown correction.
- [fixed] K9: The birthday layer describes 50.7% at 23 people as surprisingly high and has a live simulation. Changed the analogy to two counterintuitive probability classics; retained the sample-space and live-check comparison. This supersedes Codex's earlier confirmation of the loose analogy.
- [open note:22b88d] K10: verify.mjs enumerates three-door models and N=10 atoms; other N use exactNDoor's closed form. The markdown now distinguishes exact calculation, simulation and the finite Lean models. Matching source comments and film closing text were qualified; the encoded film was not rendered. At 02:34 the encoded film still says exact enumeration; board note needed.
- [dated] K11: The original page at afab40b355c already used 2026-06-25; the July 12 log records a later addition. dateModified is now 2026-10-14. The explicit metadata-date exception requires no separate Updated line because the Corrected lines date this revision.
- [fixed] K12: Commit cd73cebfe37 adds film.mp4 on 2026-06-26 and the June 26 log says it is embedded. Corrected VideoObject.uploadDate to 2026-06-26 and added matching public and markdown corrections. No media bytes changed.
- [fixed] K13: Rosenthal sections 2 and 4 distinguish host protocols and symmetric tie breaking. The explanation now attributes the unchanged 1/3 to the classic host always showing a goat and choosing equally when both goat doors are available.
- [fixed] K14: Vos Savant's fourth column says most correspondents understood the conditions, while discussing this proposed explanation of the furor. Removed the unsupported historical cause, retained the mathematical dependence on the host rule, and added matching corrections.
- [fixed] K15: The verifier uses enumeration for three-door games and ten-door atoms, closed-form probabilities for other N, and independent seeded simulations. Replaced the universal game-tree enumeration claim with those actual methods.
- [fixed] K16: Fresh fetch: the advertised /checks/research/monty-hall/lean/install-lean-nix.sh returns 404; MontyHall.lean and verify.sh return 200. The page now links the official Lean installation guide and both public files, with a same-folder bash verify.sh recipe. Downloaded files typecheck with Lean 4.35.0 and print five no-axiom footprints. Added matching corrections; no installer was run. Repair also replaced the verifier and runner installation messages with the official Lean guide.
- [open note:22b88d] K17: Re-read Tierney's archived transcript: about 10,000 is the total correspondence, most disagreeing. Nearly 1,000 critical letters had PhD signatures. Corrected the historical paragraph, dek and film source; encoded film wording is not changed. At 01:11 the encoded film still describes all 10,000 letters as dissenting; board note needed.
- [fixed] K18: Tierney describes mathematics and science department letterheads. Removed the unsupported university restriction and mathematics-only narrowing.
- [open note:81816d] K19: WRONG and intentionally open under board note 81816d. The manifest's runnable recipe lists only verify.mjs; its source inventory also publishes the proof and runner. A fresh downloaded one-file run with Lean on PATH exits 1 at the missing MontyHall.lean assertion; the same published verifier with that proof beside it passes. This wording is generated by scripts/check-placard.mjs. No local change to the promise or dependency behavior.
- [fixed] K20: The July 12 log records JS plus live kernel ALL PASS before the September 27 commit first added this June 25 last-verified claim. This new passed: 2026-10-14 record supplies the correct source date through assay/lib.mjs. Per the triage exception, the landing must rebuild the generated placard; the old visible date is still present until then. No manual placard edit or separate dated line.
- [fixed] F1: Replaced the proof comment claiming two propositional axioms with the actual no-axioms verdict. The live Lean run confirms it; no public correction line for this MINOR checking-method description.