kb: an invariant generalised from a fix generalises the fix

Three facts from Wave M's Codex round, and the middle one is about the kind of
mistake that is hard to see from inside.

Having repaired the categorical under-count, the agent proposed a
never-under-counts invariant WHILE THE TREE ALREADY HELD A COUNTER-EXAMPLE —
the missing Date arm, which Codex then found. An invariant written immediately
after a fix tends to state what the fix established rather than what the code
guarantees, because the evidence in front of you is the defect you just
closed. The question that would have caught it is about the OTHER function:
'what else does the thing I approximate do that I have not mirrored?'

The agent retracted it unprompted, before it was ever recorded.

Its structural fix is the right shape: encoded_width now matches Forced with
NO WILDCARD, so a fourth variant is a compile error rather than a silent
categorical fallback — which is exactly how Date was missed.

And the reason both bugs were invisible to a green suite: an advisory bound
over another function is a duplicated derivation, and nothing compared the two
at all. A width asserted against a constant passes at every stage while the
approximation drifts. The only honest test is to run the thing it approximates
and compare against what it actually produced.

Noted while filing: scripts/kb refused the first draft with dangling_citation,
because the doctrine named an invariant that was retracted and never recorded.
The same class as a dead ticket id, caught by the tool.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FC2jVn8Au7E9JPkw6bwXXH

prolog-sessions/kb.pl

@@ -122,6 +122,7 @@ invariant(where_and_is_share_a_word_boundary,'where_clause, inline_where and is_
 invariant(evaluate_aggregated_takes_a_named_state,'Model::evaluate_aggregated takes Aggregation::{Exact, OverHidden}, not none_cats: &[String] (improvise-5jm5). The list was consulted once, for emptiness, in every revision since Axis::None was introduced -- the aggregation runs over key.0 via matching_values. Aggregation::of reduces at the boundary and the regression guard is the SIGNATURE. recompute_formulas and aggregate_raw keep &[String] because they walk the elements.').
 invariant(normal_mode_is_resolved_not_carried,'AppMode::Normal is resolved through App::normal_mode() when the mode is SET -- ChangeMode and ReturnToNormalUnlessMoved are the only two places a batch sets it, and CloseWizard reads the same function -- so no keymap binding and no commit command carries an exit mode, and none can forget one (improvise-sihr). It reads the batch OPENING layout (gotcha 23), which is the property rather than a defect: that is the grid the user was looking at, and toggle-records-mode works in both directions because of the staleness rather than despite it. Carrying the entry mode on MinibufferConfig was the ticket proposal and was declined -- carried generically it also returns CategoryAdd to CategoryPanel. Known gap, filed as improvise-e5pf: Command::ChangeMode(Normal) is on the wire and reduce_view folds it without the resolution.').
 invariant(the_frame_basis_follows_active_view,'The cursor frame basis re-bases AT THE SWITCH, in the loop, as soon as active_view moves -- not at the next geometry effect. Guarding the COMPARISON on the two names agreeing (PR #78 round 2) exempted the first geometry effect after a mid-batch SwitchView from the check altogether, which is under-reporting and gotcha 35 expensive side. SwitchView stays ViewOnly: the basis is App own bookkeeping and none of it crosses the wire, so this needed no protocol change. Costs one extra view_frame per batch that both switches and moves geometry, DrillIntoCell paying most.').
+invariant(encoded_width_mirrors_every_preprocess_branch,'The preflight runs BEFORE preprocess and the exact check AFTER it, so the exact check bounds the error message and not the allocation. encoded_width must mirror EVERY arm of preprocess inference -- Numeric, Date (5 parts, 7 with a time) and Categorical (distinct plus the reserved (missing)) -- plus the .missing flag. It may over-count; it must never under-count. improvise-x1ns was TWO under-counts one inference-branch apart: the categorical (missing) one-hot, and the entire Date arm. The guard is that encoded_width matches Forced WITH NO WILDCARD, so a fourth variant is a compile error rather than a silent categorical fallback -- which is exactly how Date was missed.').
 doctrine(bug_first,'write a failing test demonstrating the bug before fixing it').
 doctrine(unit_over_e2e,'prefer small unit tests over integration/e2e').
 doctrine(suite_speed,'Two numbers, because the ambiguity between them is what let this drift: NO SINGLE TEST BINARY may exceed 2 seconds, and the WORKSPACE WALL CLOCK is the sum of them. Measured at 22d43b2: 1309 tests over 33 binaries, ~2.2s wall, longest single binary 1.42s -- so the workspace is already past 2s and the rule that bites is the per-binary one. Re-MEASURE rather than re-assert: cargo test --workspace prints a \"finished in\" per binary. Excludes compilation, and excludes harness/ (Playwright, minutes, its own CI job).').
@@ -291,6 +292,8 @@ doctrine(read_the_reviews_before_merging_and_authorship_will_not_identify_them,'
 doctrine(bounded_by_a_later_check_does_not_bound_the_cost,'improvise-x1ns: encoded_width is a PREFLIGHT whose whole purpose is to refuse an expansion BEFORE allocating it, and its categorical branch under-counted by the missing level that build_categorical actually emits. The wave own review had seen the shape and reasoned it away as \"bounded by the exact check\". Codex rebuttal is the keeper: THE EXACT CHECK RUNS AFTER THE ALLOCATION, so it bounds the error MESSAGE, not the cost. When a guard exists to prevent work rather than to report a wrong answer, a downstream correctness check is not a backstop for it -- the thing you were protecting has already happened. Second instance on this path: improvise-zv8t own round found forcing by NAME while budgeting by INDEX, repaired as a data dependency so the ordering became a compile error. Both are the same shape -- two halves of one decision disagreeing about what a column costs.').
 doctrine(inject_the_rival_fix_not_only_the_bug,'check_the_checker says inject the fault and watch the check fail -- which proves the test SEES THE BUG. It does not prove the test encodes the RULE. On improvise-711n two implementations both repair \",.2f\": take the leading digit run after the last dot, or trim trailing non-digits. They differ on exactly one shape, \".2f3\", and without that case the assertion is satisfied by either. So the discriminating injection is not the original bug but the OTHER PLAUSIBLE FIX. Ask, for every repair: what else would make this test pass, and is that thing also correct? Where a rival exists, the fixture must contain the input that separates them or the test pins a behaviour rather than a rule.').
 doctrine(a_preflight_must_mirror_every_branch_the_real_path_can_take,'encoded_width is a cost preflight over preprocess, which dispatches Numeric -> Date -> Categorical. It mirrored two of the three. improvise-x1ns was the categorical arm under-counting the (missing) one-hot; ChatGPT Codex then found the DATE arm missing entirely -- a date column takes the categorical fallback because \"2024-01-15\" does not parse as f64, so a column holding one distinct date promises 1 where build_date materialises 5, or 7 with a time. Two findings, one shape, one inference branch apart. A preflight is a SECOND IMPLEMENTATION of the thing it guards, so it inherits every branch of it, and the branch nobody mirrored is the one nobody was thinking about. Note the second finding contradicted an invariant proposed in the same hand-back that fixed the first: the counter-example was already in the tree.').
+doctrine(an_invariant_generalised_from_a_fix_generalises_the_fix,'Having repaired the categorical under-count, the Wave M agent proposed a never-under-counts invariant -- WHILE THE TREE ALREADY HELD A COUNTER-EXAMPLE, the missing Date arm, which ChatGPT Codex then found. An invariant written immediately after a fix tends to state what the fix established rather than what the code guarantees, because the evidence in front of you is the defect you just closed. The question that would have caught it is about the OTHER function, not about the bug: \"what else does the thing I approximate do that I have not mirrored?\" The agent retracted it unprompted, before it was ever recorded, and replaced it with the per-arm form now held as encoded_width_mirrors_every_preprocess_branch, which is the right outcome and the reason to record this.').
+doctrine(an_advisory_bound_over_another_function_is_a_duplicated_derivation,'encoded_width exists to approximate what preprocess will allocate, which makes it a SECOND IMPLEMENTATION in the improvise-edp sense -- and both of its bugs were invisible to a green suite for the same reason: NOTHING COMPARED THE TWO AT ALL. A width asserted against a constant passes at every stage while the approximation drifts. The only honest test of an advisory bound is to run the thing it approximates and compare against what that actually produced (here data.feature_names.len()), never against a number computed a second way -- which would be comparing_a_function_against_itself_tests_nothing wearing a different hat.').
 work_done('improvise-8tk',bug_fix,'ZZ/:wq quit even when the save failed, silently discarding the model. Save now aborts the effect batch on failure; save_to_current_path/1 returns Result<String,String>; three tests in ui/effect.rs.').
 work_done('improvise-907',bug_fix,'Import wizard step machine redesign: validation_error() gate at ReviewProposals (no-category and over-limit), history-stack previous() bound to Left on every step, and Done made a real confirmation step holding the built workbook. Superseded improvise-gfq, improvise-o1c, improvise-c6j.').
 work_done('improvise-6sq',wont_do,'Merging EditOrDrill and EnterEditAtCursorCmd into one EnterEdit{mode} is not safe: they differ in WHEN the cell value is read, not in a mode parameter. Added ui/app.rs::tests::i_and_o_diverge_on_an_empty_records_grid as executable evidence.').