PFP VII: Designing Executable Lessons with Explicit Evidence Boundaries

PFP VII: Designing executable lessons with explicit evidence boundaries An executable lesson can run successfully while teaching the wrong claim: a cell may compare an answer with itself, a notebook may import an obsolete implementation, or a finite check may be described as general proof. This curriculum-design guide, a companion paper in the Proposal Fidelity Protocol (PFP) series, builds each lesson from five parts: a declared finite example, a worked calculation, a learner prediction, a changed-input probe, and an explicit evidence boundary. The guide works through one rational triangle in detail. Moving a potential shifts the discrepancy from (1/3, 1/3, 1/3) to (0, 0, 1) while the cycle sum stays one, a constant height shift leaves every edge difference unchanged, and negating the claims gives a residual sum of minus one. It maps the 20-notebook integration route at the declared source audit baseline, identifies its saved 20-of-20 receipt as a historical record whose paths are now stale, and explains why one route notebook is expected to stop at a retired interface. A deliberate wrong-sign control demonstrates that a cycle-sum assertion can pass under an incorrect edge convention. The package adds a companion notebook that repeats the worked lesson with exact fractions only, and package tests that check the same arithmetic. It also vendors the two cited Lean files into a pinned local project with historical named and full axiom reports; they bound an integer list and preserve declarations under unary nesting, and neither bounds human cognition. The Landau companion supplies 24 graded problems, a worked study guide, and a separate instructor key; the grading rubric is proposed rather than empirically validated. No learner study, attention measurement, teaching-efficiency estimate, or transfer effect is reported.