proof: Lemma B at-pre helpers Qed + preservation Phase 2 wired (12→11 admits)#146
Merged
Conversation
…und truth 4 of 5 sub-tasks discharged; 1 remaining proof item with revised case count and wall-clock estimate (~4-6h, was 8-15h). Records empirical coqc 8.18 verification: 1 admit in step_preserves_type + 1 in Lemma B + 12 cascading goals in preservation = one structural admit (S_Region_Step r=r1 sub-case) mirrored twice, with the path forward agreed (Option 2: exit-typing helper by structural recursion on Hstep). Refs hyperpolymath/standards#134 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two updates to formal/PRESERVATION-HANDOFF.md: 1. Add 2026-05-24 and 2026-05-26 rows to the "State at a glance" table. The 2026-05-24 session closed Cluster A (7 β-reduction) and Cluster C (6 region/compound-value) entirely, and 9 of 18 of Cluster B. The 2026-05-26 coqc 8.18 re-verification shows the current shape: 1 admit in step_preserves_type + 1 admit in Lemma B (same structural sub-case, mirrored) + 12 cascading goals in preservation. 2. Add a current "Effort revision" section that supersedes the 2026-05-24 "8-15 focused hours for Lemma B alone" estimate. The actual remaining surface is one helper lemma (exit_implies_typing_at_remove_first by structural recursion on Hstep) plus the mechanical cascade. Wall-clock ~4-6h to Qed. Retained the historical estimate below for context. Closure path agreed 2026-05-26: Option 2 from § "Genuinely-closing options". No code changes; this is a doc-truthing pass. Refs hyperpolymath/standards#134 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Option 1 Pre-flight analysis of the structural-recursion approach (option 2 from PRESERVATION-HANDOFF.md) found a counterexample the handoff didn't anticipate: e = ELet (ERegion r v_inner) e2 (well-typed at R with In r R) e' = ELet v_inner e2 (after S_Let_Step / S_Region_Exit) e2 may reference r, T_Let has no sibling-freedom premise, and after the step R no longer has r — so the structural recursion cannot rebuild e''s typing at R'. This blocks both the freedom-extraction path AND the typing-rebuild path the doc described as "orthogonal". Revises the resolution-path table: - Path 2 (structural recursion ~150 LOC) → blocked, not orthogonal - Path 1 (mutual induction) → most robust, ~8-12h - Paths 4/5 (language change) → outside standards#134 scope No proof code committed this session because Option 2 doesn't pan out and Option 1 deserves its own focused multi-hour push. The lemma-b-phase2 branch retains the prior two doc commits and now this audit; the actual proof work will resume on a fresh branch keyed to the chosen Path 1 approach. Refs hyperpolymath/standards#134 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Two artefacts that bring the session into the human/machine-readable canonicals: 1. docs/sessions/SESSION-2026-05-26-lemma-b-pivot.adoc (human) — matches the docs/sessions/SESSION-YYYY-MM-DD pattern from SESSION-2026-05-20-proof-engineering-lessons.adoc. Records the case-count truthing, the Option 2 counterexample, and the Path 1 pivot. Cross-references to the three audit/handoff docs already in this PR. 2. .machine_readable/6a2/STATE.a2ml (machine) — updates phase/next_action/last_action/blockers to the post-session shape (was stale from 2026-05-20). Adds @artifacts block listing the doc-only commits parked on this branch. Refs hyperpolymath/standards#134 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Final doc-truthing pass. ROADMAP.adoc § "Preservation closure plan"
gained two new rows in the reduction-story table:
- 2026-05-24 night cluster closures (4 → 1 of 35 in Lemma B)
- 2026-05-26 re-verification (1+1+12 picture, Option 2 blocked,
Path 1 pivot)
plus an updated effort estimate.
PROOF-NEEDS.md got the same revision: replace the old 5-phase
"Lemma B + region-env weakening" decomposition (which assumed the
now-blocked Option 2 + independent region-env weakening lemma) with
the Path-1 3-phase shape: mutual induction restructuring → cascade
preservation's 12 goals → unwind checklist. ~8-12 hours wall-clock
(was "3 sessions / ~10 hours").
Companion artefacts already in this PR:
- docs/reports/audit/audit-2026-05-26-lemma-b-option-2-obstacle.md
- docs/sessions/SESSION-2026-05-26-lemma-b-pivot.adoc
Refs hyperpolymath/standards#134
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…lpers Path 3 plug-in. Both upstream lemmas' single shared S_Region_Step r=r1 admit closed via the same trick: region_env_perm_typing transports the body's T_Region typing from (r :: remove_first r R0) to R0 (same membership when In r R0), then a new at-pre helper (both typings at R, not R/R') closes type/output equality. Adds two scaffolded helpers BEFORE the upstream lemmas: - step_preserves_type_at_pre: signature matches step_preserves_type but with both typings at R (not R/R'). The S_Region_Step cross-case (T_Region_Active vs T_Region) collapses to a contradiction (In r R vs ~In r R) under the same R, so the problematic sub-case vanishes. - step_output_context_eq_at_pre: same idea for the linearity-context side of the equivalence. Both helpers carry a single 'all: admit.' as scaffolding for the 35 step rule cases. Per-case work (~6-10h) is the remaining lift. Net proof state: - step_preserves_type: Admitted -> Qed (was 1 admit at 4885) - step_output_context_eq: Admitted -> Qed (was 1 admit at 5963) - step_preserves_type_at_pre: NEW, 1 admit (scaffolding) - step_output_context_eq_at_pre: NEW, 1 admit (scaffolding) - preservation: Admitted (12 cascading goals) The obstacle has been MOVED, not closed: the same number of admits remain, but they're now in helpers whose S_Region_Step case is structurally simpler (no cross-case mismatch). Per-case work to discharge the at-pre helpers is the path to full Qed. Refs ephapax#146, standards#134.
…tactic blocks Build on the prior at-pre scaffold. Three new per-case tactic blocks specific to at-pre framing (atomic leaf inversion, S_Region_Step at-pre, S_Region_Exit at-pre) close 8 cases. Cluster A (beta-reduction) and Cluster B (congruence) blocks copied verbatim from step_preserves_type close 19 more cases (their patterns use ?R/?R' polymorphically, so they work for at-pre framing where both are R). Net: step_preserves_type_at_pre is now 27/35 closed, 8 admits via the final `all: admit.` catch-all. The remaining 8 are step_preserves_type's "Per-goal" cases (S_StringConcat_Step2, S_Let_Step, S_LetLin_Step, S_App_Step2, S_If_Step, S_Pair_Step1, S_Pair_Step2, S_Case_Step) that need explicit per-goal blocks (~30 LOC each). step_output_context_eq_at_pre still has 35/35 admitted via `all: admit.` — parallel work to do for it next. Both upstream lemmas (step_preserves_type, step_output_context_eq) remain Qed; the obstacle has been further narrowed. Refs ephapax#146.
Parallel work to the prior commit for step_preserves_type_at_pre. The Atomic + Cluster A/B/C tactic blocks from step_output_context_eq (~946 lines, lines 5757-6702) work as-is in the at-pre framing because their patterns use ?R/?R' polymorphically — for at-pre both unify with R0. Skipped: the final S_Region_Step block (line 6703+) which references step_output_context_eq_at_pre itself via the plug-in — copying it would create a self-reference. The S_Region_Step case in at-pre is structurally simpler anyway (T_Region_Active forced on both sides) and is amenable to a single ad-hoc tactic block to be added later. Net: step_output_context_eq_at_pre now has the body filled in; estimated 24-27 of 35 cases close via these blocks. The remaining cases (including S_Region_Step) fall through to the final `all: admit.` catch-all. Both upstream lemmas (step_preserves_type, step_output_context_eq) remain Qed; preservation remains Admitted (12 cascading goals). Refs ephapax#146.
… admit step_preserves_type and step_output_context_eq are now both Qed (was both Admitted with 1 admit each at the SAME shared S_Region_Step r=r1 cross-case). Two new helper lemmas — step_preserves_type_at_pre and step_output_context_eq_at_pre — encode the typing pair at a SHARED pre-step env R; the S_Region_Step cross-case (T_Region_Active vs T_Region) collapses to a vacuous contradiction (In r R vs ~In r R) at the same R, sidestepping the original obstacle. Both helpers are themselves Admitted with the bulk of step rule cases closed (via verbatim copy of step_preserves_type's and Lemma B's tactic blocks — patterns use ?R/?R' polymorphically so they work for at-pre). ~8 cases pending in step_preserves_type_at_pre, ~11 in the output_context_eq_at_pre — all in the per-goal section territory. preservation remains Admitted: its 12 cascading goals are a SEPARATE structural problem (region-env weakening for non-values), not the shared shared-admit closed by the at-pre helpers. Refs ephapax#146 (lemma-b-phase2 branch).
…+ docs Three sub-agents fanned out in parallel: - Swarm A drafted 8 per-goal closures for step_preserves_type_at_pre. After integration, 3 of 8 cases closed. 5 remain: S_StringConcat_Step2, S_App_Step2, S_Snd_Step, S_Case_Step, S_Copy. - Swarm B confirmed the Cluster A+B copy already covered all but S_Region_Step for step_output_context_eq_at_pre. Delivered the S_Region_Step at-pre block. Closes 1 of 12; 11 remain (touches_region RIGHT branches from Cluster B's | fail ]). - Swarm C re-diagnosed preservation's 12 admits. Key finding: 11 LEFT branches are now trivially closable via step_output_context_eq as oracle (the new Qed lemma resolves the output-context skolem mismatch that was silently failing them). RIGHT branches still need region-env weakening. To be applied in a follow-up commit. Net proof state (verified by coqc 8.18.0): - step_preserves_type: Qed - step_output_context_eq: Qed - step_preserves_type_at_pre: Admitted (5 remaining of 35) - step_output_context_eq_at_pre: Admitted (11 remaining of 35) - preservation: Admitted (12 cascading; Swarm C splice TBD) Doc updates: PRESERVATION-HANDOFF.md "2026-05-26 eve" row + STATE.a2ml refresh. Refs ephapax#146.
Restructures S_Let_Step's tactic block from try solve [LEFT | fail] to try (LEFT | idtac), with LEFT now using step_output_context_eq as oracle to resolve the output-context skolem (Gout = Gmid via assert+subst before eapply T_Let). The change doesn't reduce admit count yet — both LEFT and RIGHT must close to remove a goal from preservation's catch-all Admitted. RIGHT still needs region-env weakening for non-values. Lands as scaffolding for the structural C work: the LEFT closure pattern is verified correct under coqc, ready to propagate to the other 10 congruence blocks once RIGHT-closure infrastructure exists. Refs ephapax#146.
…n LEFT branches closed
Brings together three pieces of the 2026-05-26 Lemma B campaign:
1. `step_preserves_type_at_pre` (Swarm A) — 5 remaining per-goal cases
closed via explicit `1: {...}` blocks (S_StringConcat_Step2,
S_App_Step2, S_Snd atomic, S_Case_Step, S_Copy). Now Qed.
2. `step_output_context_eq_at_pre` (Swarm B) — 11 remaining per-goal
cases closed. Now Qed.
3. `preservation` — Swarm C oracle splice closes the LEFT (R = R')
branch of every congruence case via `step_output_context_eq` (Qed):
`assert Gmid = Gout by (eapply step_output_context_eq; …); subst`
unifies the IH's existential output context with the sibling
typing's input. `S_StringLen_Step` closes ENTIRELY as vacuous
(`EBorrow`'s inner is `EVar` or a value — neither steps — pattern
lifted from `S_Borrow_Step`). `S_StringConcat_Step1` collapsed from
3-way `step_R_change_shape` to 2-way `step_R_eq_or_touches_region`
for consistency with the other 10 S_*_Step blocks; the MIDDLE
(push) closure is folded into the touches_region RIGHT and will be
re-distinguished by the C-lemma's structural recursion.
Net: preservation drops from 12 → 11 admits. The remaining 11 are:
- 10 touches_region RIGHT sub-cases (`HTR : touches_region` in
scope), each blocked on region-env weakening for non-values
(= Brief C, structural follow-up).
- 1 `S_Region_Step` cross-case `T_Region_Active × T_Region` at
`r = r1` ("inner step exits outer region from inside") — same
shape inside `step_preserves_type_at_pre`'s original obstacle, now
cleanly characterised in PRESERVATION-HANDOFF.md.
Verified with `coqc 8.18.0` on a clean rebuild.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
changed the title
Owner
Author
Scope update — d6ebf68 lands the actual proof workThis PR originally tracked docs-only reconciliation (audit + handoff + Option-2 obstacle analysis). With d6ebf68 it now also lands the Path-3 at-pre closure campaign: Now
|
…6ebf68) Three call-outs were stale relative to the Swarm A+B+C closures landed in d6ebf68: * `ROADMAP.adoc` preservation table row — said `12 open goals ... blocked on Lemma B per-case closure`. Lemma B (`step_output_context_eq`) + its at-pre plug-ins are all `Qed` now, so the count is 11 and the blocker is region-env weakening for non-values (Phase 3) not Lemma B. * `formal/PRESERVATION-HANDOFF.md` Path-3 callout — said `both [helpers] are Admitted with a final all: admit. catch-all` and listed the per-goal cases as pending. Both are now `Qed`; the residual 5 + 11 cases closed via explicit `1: {...}` per-goal blocks at the tail of each helper. The summary table at line 27-29 of PRESERVATION-HANDOFF.md was already accurate (entry for `(eve) Qed × 2` and `(late eve) Qed × 4 + 11`); only the prose callout was lagging. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…its → pop-only) Converts all 10 congruence `S_*_Step` blocks in `preservation` from 2-way `step_R_eq_or_touches_region` to 3-way `step_R_change_shape` dispatch: - LEFT (R = R'): unchanged — closes via `step_output_context_eq` oracle. - MIDDLE (R' = rw :: R, push): NEW closure via the same oracle to unify the IH's existential `Gout` with sibling's `Gmid`, plus `region_add_typing` (already Qed) to lift the sibling typing from `R` to `rw :: R`. - RIGHT (R' = remove_first r R, pop): `idtac` — needs Brief C. Result: each of the 10 remaining preservation admits is now narrower. Pre-commit each had `HTR : touches_region` in scope; post-commit each has `Hrem : R0' = remove_first r R0` and `HinR : In r R0` in scope. Brief C's required structural lemma is correspondingly tightened from "region-env weakening across any touches_region step" to "pop-only weakening" (the surviving sibling must transport from R to remove_first r R when In r R). Coq subtlety: S_StringConcat_Step1 and S_StringConcat_Step2 must use `[rw …]` in the destruct pattern because the outer T_StringConcat inversion binds an `r` (the TString region) in scope already — Coq's intro patterns silently fail on name collision, which earlier caused the whole `try (...)` to revert. The other 8 blocks can use `r`. The 11 cascading admits in preservation: - 10 POP sub-cases (one per congruence), each blocked on the C lemma in narrowed pop-only form. - 1 `S_Region_Step` cross-case (T_Region_Active × T_Region at r = r1) — same shape as the obstacle that Path 3 resolved upstream; not reachable via Swarm-C techniques here. Verified clean with `coqc 8.18.0` on `lemma-b-phase2-middle-narrow`, branched off `lemma-b-phase2` HEAD `d6ebf68`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
## Summary
Adds the static-shadowing-prevention lemma referenced by the forward
comment at `formal/Semantics.v:9096` (post-MIDDLE-narrowing diagnostic
block):
```coq
Lemma typing_free_of_absent_region :
forall R G e T G' r,
R; G |- e : T -| G' ->
~ In r R ->
expr_free_of_region r e.
```
Proved by structural induction on the typing derivation (26 cases, ~50
LOC). Each typing rule's region premise is incompatible with `~In r R`
when applied at `r`:
- T_Loc and T_StringNew force the `r0 <> r` case via their `In r0 R`
premise.
- T_Region's body recurses under `r0 :: R` where `~In r (r0 :: R)` still
holds when `r <> r0`.
- T_Region_Active contradicts directly when `r = r0`.
## Why this matters
Does **not** close any preservation admit on its own — the
touches_region RIGHT cases have `In r R` (not `~In r R`) by
construction. But this lemma is the **kernel** of Brief C's structural
recursion: any closure path that traces an exited region back to its
introducing ERegion via inversion-on-Hstep will need this fact to
establish sibling-disjointness from the inner T_Region's `~In` premise.
Lands as a Qed building block alongside
`region_shrink_preserves_typing_dup` (also adjunct), available for Brief
C work to pull in.
## Test plan
- [x] `make -f Makefile.coq Semantics.vo` clean rebuild on `rocq`
toolchain → exits 0
- [x] `grep -c "^Admitted\." formal/Semantics.v` == 1 (only
`preservation`)
- [x] GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`)
- [x] Co-author tag for Claude Opus 4.7
Refs ephapax#146.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 31 issues detected
View findings[
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Admitted leaves proof hole (3 occurrences, CWE-704)",
"type": "admitted",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Coq admit tactic leaves goal unproven (7 occurrences, CWE-704)",
"type": "coq_admit_tactic",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "User-defined Coq axiom -- not verified by kernel (2 occurrences, CWE-704)",
"type": "coq_axiom",
"file": "/home/runner/work/ephapax/ephapax/formal/Semantics.v",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
"type": "believe_me",
"file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
"type": "assert_total",
"file": "/home/runner/work/ephapax/ephapax/src/formal/Ephapax/Formal/RegionLinear.idr",
"action": "flag",
"rule_module": "code_safety",
"severity": "high"
},
{
"reason": "unwrap_or(0) with dangerous default (2 occurrences, CWE-754)",
"type": "unwrap_dangerous_default",
"file": "/home/runner/work/ephapax/ephapax/lib/linter.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (2 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/ephapax/ephapax/src/ephapax-wasm/src/debug.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
"type": "unwrap_dangerous_default",
"file": "/home/runner/work/ephapax/ephapax/src/ephapax-wasm/src/lib.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "expect() in hot path (1 occurrences, CWE-754)",
"type": "expect_in_hot_path",
"file": "/home/runner/work/ephapax/ephapax/src/ephapax-package/src/manifest.rs",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
Merged
3 tasks
hyperpolymath
added a commit
to hyperpolymath/standards
that referenced
this pull request
May 27, 2026
…PR (#221) ## Summary The trusted-base reduction policy's P0 migration table cited **3 Admitteds** in `ephapax/formal/Semantics.v`. The actual count on `main` is **1** — the other two (`step_preserves_type` and `step_output_context_eq`) were discharged via [ephapax#146](hyperpolymath/ephapax#146) (Path 3 at-pre helper landing) before this policy doc was filed. Also adds: - Link to `formal/PRESERVATION-DESIGN.md` (four-layer redesign on branch `proof/l1-region-threading-design`) as the principled closure plan. - Forward link to [ephapax#164](hyperpolymath/ephapax#164) — the P0 migration PR adopting this policy in `ephapax/docs/proof-debt.adoc`. No semantic change to the policy itself — just keeping the migration table accurate as repos adopt the schema. ## Test plan - [x] One-line `.adoc` table cell edit; no build target affected - [x] GPG-signed commit (key `4A03639C…2867091E`, noreply email) - [x] Auto-merge SQUASH enabled 🤖 Generated with [Claude Code](https://claude.com/claude-code)
Owner
Author
|
📌 Archaeology marker (added 2026-05-27 post-counterexample) This PR predates the 2026-05-26 counterexample landing in The post-discovery doctrine lives at:
Do NOT apply the lemma shapes or tactics from this PR's diff to current proof work. The legacy judgment lacks the structural invariant the counterexample demands; no lemma collection bolted onto it will help. See |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Three doc-only commits parking the proof-debt analysis on a dedicated branch, ahead of the actual Lemma B body work:
`032e8ea` audit reconciliation — `docs/reports/audit/audit-2026-05-26-standards-134-reconciliation.md`. 4 of 5 sub-tasks of `[P2] ephapax: 11 partial + add ABI seam (Rust/SPARK NON-COMPLIANT) standards#134` were discharged pre-2026-05-26 (Idris2 totality, ABI seam, stance doc — all DONE). The remaining one is the Coq `preservation` Qed, which empirical coqc 8.18 verification shows is much closer to closed than the 2026-05-21 case-count framing implied: 1 admit in `step_preserves_type` + 1 in Lemma B (same structural sub-case mirrored) + 12 cascading goals in `preservation` that close mechanically when Lemma B closes.
`83e1e31` handoff case-count correction — adds 2026-05-24 + 2026-05-26 rows to `formal/PRESERVATION-HANDOFF.md`'s "State at a glance" table, and supersedes the stale "8-15 focused hours for Lemma B alone" estimate with the current shape (one helper lemma + cascade). Retains the historical estimate for context.
`36ff88e` Option 2 obstacle audit — `docs/reports/audit/audit-2026-05-26-lemma-b-option-2-obstacle.md`. Pre-flight analysis of the handoff doc's recommended Option 2 (structural recursion on `Hstep`, "~150 LOC, orthogonal") found a counterexample: `ELet (ERegion r v_inner) e2` with `e2` referencing `r` is well-typed (T_Let has no sibling-freedom premise) but the post-step expression cannot be retyped at `R'`. Pivots the recommendation to Path 1 (simultaneous mutual induction over `step_preserves_type` + `step_output_context_eq` + `preservation`), ~8-12h focused session.
Why merge these as docs-only
These corrections are correct independent of when the actual Lemma B body lands. Merging them now:
What this PR does NOT do
Test plan
Refs hyperpolymath/standards#134