Skip to content

docs(doctrine-v7): honest Putnam framing in §11 canonical-number example#102

Closed
stephenlutar2-hash wants to merge 1 commit into
mainfrom
fix/doctrine-v7-putnam-honesty
Closed

docs(doctrine-v7): honest Putnam framing in §11 canonical-number example#102
stephenlutar2-hash wants to merge 1 commit into
mainfrom
fix/doctrine-v7-putnam-honesty

Conversation

@stephenlutar2-hash
Copy link
Copy Markdown
Member

Summary

Doctrine v7 (doctrine/DOCTRINE_V7.md) lives in this .github repo (referenced by the lutar-lean README badge). Its §11 "Canonical-Number Propagation Deadline" example cited the Putnam value 83.3% (10/12) as the canonical/correct figure.

That figure counts files with structural scaffolding, not proved problems, and is itself misleading. Per the PhD Math audit:

  • 0/12 Putnam 2025 problems are fully proved.
  • A1, A3 are sorry-token-free but stated as → True shells.
  • A5, B4, B6 carry root-level sorries on the main theorem.
  • Two files previously encoded the wrong official answer (P_B6: r=1/2 vs official 1/4; P_A3: Alice vs official Bob), corrected in lutar-lean.

Change

Adds an honesty-correction note to §11. The historical example (the 1/12 staleness bug) is retained to illustrate the propagation rule, but the 10/12 value is explicitly forbidden as a progress metric.

Source verification

Official answers verified against the 86th Putnam official solutions (https://kskedlaya.org/putnam-archive/2025s.pdf): "B6. The largest such constant is r = 1/4" and "A3. Bob has a winning strategy for all n ≥ 1".

Notes

  • Docs-only, single-file change.
  • No canonical_numbers.json exists yet in this repo, so the doctrine doc is the authoritative location for this number.
  • Out of scope this round: several coordination/ and cursor-directives/ files also cite 10/12-style Putnam numbers; flagged for a later pass.

Signed-off-by: Stephen P. Lutar Jr. stephenlutar2@gmail.com

Doctrine v7 §11 used "83.3% (10/12)" as the canonical Putnam value in its
staleness-propagation example. That figure counts structural scaffolding,
not proved problems, and is itself misleading. Per the PhD Math audit,
0/12 Putnam 2025 problems are fully proved (A1/A3 are sorry-token-free but
-> True shells; A5/B4/B6 carry root sorries). Two files previously encoded
the wrong official answer (P_B6 r=1/2 vs 1/4; P_A3 Alice vs Bob).

Adds an honesty-correction note; retains the example only to illustrate
the rule, and forbids citing 10/12 as a progress metric. Official answers
verified against https://kskedlaya.org/putnam-archive/2025s.pdf.

Signed-off-by: Stephen P. Lutar Jr. <stephenlutar2@gmail.com>
@stephenlutar2-hash
Copy link
Copy Markdown
Member Author

Closed per founder directive 2026-05-30 16:23 EDT: Putnam is being dropped from the SZL story; the doctrine §11 example will be replaced with a non-Putnam example in a separate PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant