Repository navigation
Conversation
A sum term that is an odd function of a negative literal gives its sign to the joiner (`x1 - sin(2)`), as `simplify`'s infix text does (owner ruling 2026-08-08). `pi_fit` picks between the literal in front and the literal below in one match. Tests pin rule 5 with an integer reciprocal (`x1/(243*x2)`, bare `x1/243` a multiplier) and the divisor grouping (`x0/(x1^2*x2)` grouped, `x0/x2/cos(x1)` one slash per non-plain divisor). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The state keeps `c^5` as a power when the exact value of an 80-digit `c` to the fifth leaves the size cap. Once the display writes `c` as its float, the power of that float is an ordinary number and is combined exactly (`3.0492025996286705e-14*x1`), as the re-read state combines it; before, the display wrote `0.001980784624751695^5*x1` and only rule 11's second pass reached the fixed point. `3^5000` (an integer that fits) stays a power. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…nded once Permissive ran three arms (two fold disciplines and the f64 chain), finished the f64 arm's states, continued long-literal winners up to four rounds, re-read every candidate and selected per budget. It is now one walk, like every mode: the chain to its fixpoint, then the search, in permissive's own canon and rules. - The ground fold (G) is a step of the pass: a ground node whose class the interval layer does not decide is evaluated by the deployed f64 evaluator and offered as its float's shortest decimal, tried after the rules at each node and accepted only when it descends. The constructors no longer fold in permissive, so a constructor identity always sees the unfolded shape (`atanh(tanh(30))` is `30`), and G still folds `asin(1e-8)` and whole ground nodes neither old arm folded (`exp(9.55893790547399)`, `3.141592653589793^(3/2)`). - Literals are rounded once, where they land (ρ, owner ruling P2): arithmetic between literals stays exact, and a literal moves to its float (`lossy_literal`) when it becomes a constant term, a coefficient, a power's operand beside a non-literal, a function argument or a state's root. ρ is mu-neutral under the float cap, so no descent argument changes, and the walk never holds a literal a later step would move. Removed: the selection (`ac_simplify_ex_permissive`, `permissive_arms`, `finish_defaults`, `cand`, `Cand`, `LITERAL_FOLD_ROUNDS`, `print_prefix`), the literal-fold snaps (`snap_lossy_literals`, `snap_long_literals`, `prints_long`, `printed_coefficient`), and the search's `trace` parameter, which only the selection read. The answer is the walk's final state: it starts at the input's reading and every step descends (L3), so it never prices above the input; a capped run is a prefix of the uncapped walk, so more effort never ends costlier; and a fixpoint and search valley is reproduced by a second call (L6) wherever its print reads back as itself. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
Permissive's `pow` distributes a reciprocal over a product unconditionally, so `c/(A*B)` is held as `c * A^-1 * B^-1`: no DISTRIBUTE reaches the product inside the reciprocal, and the coefficient never merges into the sum it divides. The sound modes keep such a reciprocal joined and expand inside it. On srbf's predictions this was the main reason permissive's old selection needed its f64 arm (149 of the 195 rows that arm decided). A new search move, RECIPROCAL JOIN (permissive only), proposes `A^-1 * B^-1 -> (A*B)^-1` and `c * A^-1 -> (A/c)^-1`, each with the inside distributed into one sum through `distribute_product` (same licences). Like every move, it is a candidate the search descends and keeps only when it lands strictly below; nothing is projected. On the 195 prediction rows of shard 0 where step 0 needed the f64 arm, the one walk improves on 182 with this move, and 175 reach step 0's answer or below. f64 and real are unchanged (the move is gated on permissive). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The reciprocal join also proposes `f * A^-1 -> (A/f)^-1` for any other factor `f` of the product, with `1/f` distributed over `A` (`x7/(x7 - x5)` is `1/(1 - x5/x7)`), the shape the sound modes reach because they keep such a reciprocal joined. Like every move it is a candidate the search descends and keeps only when it lands strictly below. Against the join of literals and sums alone, on srbf's 6,531 ground truths 258 answers get cheaper and 3 costlier, on shard 0 of the T8.1 inputs 472 and 1, and on shard 0 of srbf's predictions about 170 and 3, for 7% (GT), 16% (T8.1) and 2% (predictions) more work units. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…ssive Owner ruling P5: `work` stays an opt-in cap that ends a search early and never changes which algorithm runs, and no mode has one by default. `DEFAULT_WORK` (declared by the core) is now `None`, `work='default'` resolves to it in every mode, and the miner's marks follow it (`serve_work`). Permissive needed its 10,000-unit default only to bound its three arms; its one walk runs uncapped at 2.6-3.3 times f64's work units on the three bench sets (the selection at its budget: 5.9-10.6 times). Docs: the simplify guide, formal.md (the selection's proposition retired; L3, L6 and the effort prefix argument cover permissive; the double-rounding residual of rounding at landing, measured) and the CHANGELOG (the one walk, measured against the selection on srbf's ground truths and shard 0 of the T8.1 inputs and of srbf's predictions). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`find_rules` records each mode's final set only when it writes an output file, so a mine without one ended holding the LAST mode's working set (permissive's) in the default slot. That was invisible while permissive re-minted the f64 rules it did not fold. With permissive's ground fold in the pass it folds `cos(np.pi)` itself and mints no rule for it, and the in-memory mine lost the f64 rule. An in-memory mine now records each mode's mined set, so the engine ends holding the f64 mine's set in the default slot and the real and permissive sets in their attributes, as a file mine does. The exact-collapse test asserted `sin(np.pi) -> 0` in the default set, a rule only the real mine mints (f64 computes 1.2246467991473532e-16); it now reads it from the real set. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… for D1 Two spellings of one value reached one answer in permissive only because its old selection took the f64 arm's answer. The one walk reads them apart: - `(sin(x1) - x1)*(x1 + sin(-x1))` (and `atan`): permissive spells `x1 - sin(x1)` as `x1 + sin(-x1)` and does not read the two factors as one class (51,000 vs the square's 32,585); - `1/((1 - x1 - x2)*(1 - x1 - x2)^(1/3))` against its split spelling: the reciprocal orients one base and the cube root keeps the sign inside the other, so they do not merge. Both are sign placement, owned by the sign round (D1). They are strict xfails in permissive only, so they fail loudly once D1 fixes them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`1/exp(t) -> exp(-t)` is the rule the strict-Kruskal respell test expects the mine to find. Each file is mined in its own mode: f64 refuses it (the two spellings round differently near underflow), real and permissive mint it. The test read it from the default slot, which an in-memory mine filled with permissive's set until the previous commit; it now asks permissive, which serves it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The Python driver mines each file in its own mode end to end, and the judge's tier is decided inside the scan rather than routed afterwards. - The per-length judge loop (miner.md 2.6). After a length's scan, each pick's pattern and every entry the mode serves from it go to the judge (injected: find_rules(judge=, judge_processes=); default judge_tiers, a spawn pool for batches of 64 or more, verdicts memoised by pair). A pick whose tier the file's mode does not license (verify.MODE_TIERS), or that the mode does not serve, is excluded and only its source is re-scanned (mine_one_length gains `exclusions` and `indices`, keyed by the global source index). Exclusions only remove refused targets from a deterministic scan, so the result is the scan that consults the judge per candidate: another mode's pick never shadows a licensed alternative. The loop stops at 8 rounds and fails the mine loudly if it gets there. - Gate and install per length (2.7): only licensed picks are installed, so a refused rule never prunes a longer source. Rows the mode's load would mint anyway (a twin-shadow owner) are dropped and the census re-read. The dedup tie-break is the mode's serve ordering (dedup_target_wins), not token count, here and in the proposals' duplicate accounting. - Checkpoint and resume per length: <file>.checkpoint.json holds the licensed rules, the per-length record, the judge memo and the progress, under a fingerprint of the parameters, the mode, the universe and the starting sets; the climb resumes after the last completed length and the checkpoint goes once the file is final. The rule file and its sidecar are written once, by the post-pass. - The post-pass per mode: the symbolic gate keeps what the mode licenses, the covered prune asks the mode's serve answer and ordering (prune_covered_rules(rule_mode=)), promotion and refund run in the mode. The final gate judges the installed set's file spellings and its served entries with the loop's judge and drops what the mode does not license; the preemption check is a gate after it. Both are listed in the sidecar (`gates`), with per length the judge rounds, the exclusions and the twin-shadowed rows (`per_length`). _route_triple, _TIER_MODES and _assert_triple_invariants are gone; verify.effective_tier is the one reading of a judged tier. - rule_mode is required on the mining path: find_rule, ac_simplify_suppressed, deduplicate_rules, prune_covered_rules, promote, promote_rules and refund. The refund's dedup keys now read in its mode. - Each mode's result is kept when no output file is written, so the next mode mines beside the f64 set and the engine ends holding all three (they used to collapse to the last mode's set in the default slot). Tests (each made to fail once): a refused pick yields to the next candidate (stub judge); a rule refused at length 3 moves no length-4 mark (spy on the marks; with the rule licensed the mark moves); two shards equal one mine, exclusions included; a crashed mine resumes from its checkpoint to byte-identical files; the final gate drops an unlicensed file spelling and an unlicensed served entry; a pick the mode does not serve is licensed nowhere; twin-shadow removal keeps the served set; the dedup tie-break follows the ordering; three-mode determinism across PYTHONHASHSEED, thread count and judge processes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… its mode - The judge loop excludes a refused target by its canonical key in the mine's mode (miner.md 2.6), not by its spelling. The library keeps spellings of one class apart where their guards differ (`* 1 x0`, `+ 0 x0`, `/ x0 1` beside `x0`), and the judge's verdict is the class's, so a spelling exclusion re-scanned the same refused class once per spelling (`tan atan x0` four times): length 3 of the f64 smoke took five judge rounds, two now. - The covered prune instantiates `$` slots like the other sorts (they stayed literal tokens, which f64 and real read as opaque and permissive as a variable), probes `$` with the wide sorts' composite, and in permissive, where every slot binds any subtree, also probes each non-finite literal. Permissive keeps `$0 / $0 -> 1`, which takes `inf/inf` to `1` where its constructor gives `nan` (the mask-sentinel rule the per-mode prune had dropped); f64 and real prune it: their constructors cancel the probed instances, and their ground fold reads `inf/inf` before any rule. Measured on the acj-3-2c reference against R2b: f64 125 -> 123 and real 111 -> 108 (`$0 / $0 -> 1`, `0 / $0 -> 0`, and in real `* !0 log 1 -> 0`, covered by each mode's own constructor), permissive 16 -> 14 (four covered rules pruned, `* 0 !0 -> 0` and `- !0 !0 -> 0` kept for their non-finite instances). The 400 release-corpus rows give identical answers in all three modes. Tests (each made to fail once): exclusion by class, on a source with two accepted classes; permissive keeps the mask sentinel; a `$` slot is instantiated and its prune changes no answer; the judge loop judges a pick's file spelling as well as its served entries. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…o env switch
- `simplipy verify-mine <file> --mode m` (`mining.verify_mine`): the re-mine gates of one
mined file in its own mode -- no twin-shadowed row (the rows twin-shadow removal drops,
one predicate `_twin_shadow_owners` for both), no engine-owned law (`law_instance`), every
file spelling and served entry licensed (the mine's own final gate), no preempted ground
rule, a translation that subsumes and drops nothing, a clean measure fingerprint, and no
SIMPLIPY_* switch in the sidecar's record or in the checking process. Exit code 1 when a
gate fails; `--report` writes the JSON.
- Every core entry that reads a mode takes it explicitly (keyword-only, no default):
ac_simplify_in_mode, ac_simplify_infix_in_mode, ac_simplify_explore (its `wildcard_all`
becomes `rule_mode`), prettify, ac_complexity(_certified), ac_rules_info_in_mode,
ac_served_rules_in_mode, mode_rules_len. The mode-less twins ac_simplify,
ac_simplify_infix, ac_ordered_below, ac_rules_info, ac_served_rules and set_rules are
retired (set_mode_rules('default', ..) keeps the pushed-rules digest). Python keeps its
public defaults.
- Proposals are one more length of the judge loop (miner.md 2.11): find_rule_lib and
judge_hint take the loop's exclusions (by class, through the Acceptor), a certified target
the mode does not license is excluded and the proposal certified again, and one left
without a licensed target reads rejected at stage `judge`. The sidecar records the loop
under `proposals.judge_loop`.
- A checkpoint resumes only its own mine: the fingerprint carries the code digest (the
compiled core and the package's sources), and a checkpoint of any other mine refuses to
start, loudly, and stays in place.
- Environment: SIMPLIPY_IVL_NODE_BUDGET is `find_rules(interval_node_budget=)` (config key
`interval_node_budget`), set for the mine, restored after and recorded in `params`;
SIMPLIPY_TAGGED_FRACTION_MAX is gone (the bound is 10). ARTIFACT_ENV_SWITCHES is empty, and
`soundness.env_overrides` records every set SIMPLIPY_* variable but the inert ones.
- Sidecar per file: `acceptance` (rtol, atol, rescue, the near-miss gate the core declares as
NEAR_MISS_FRAC, the licensed tiers, the judge's digest) and `code_digest`.
Tests (each made to fail once, 16 mutations): every gate on a planted violation and a clean
mine passing all of them in each mode; the CLI's exit code; the acceptance record; a
proposal refused at the judge; a resume across code or parameter changes refusing; the node
budget set and restored; every mode-taking entry raising without its mode, and no mode
default left in the extension's signatures.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- docs/rules.md: "How mining works" per mode (sources, mark, scan, certify, confirm, the judge loop, install), the post-pass and file gates, determinism with shards and the checkpoint, the sidecar's records; "Verifying a mine"; the covered prune per mode; the `interval_node_budget` config key. - docs/guides/artifacts.md: each file mined in its own mode, its sidecar records, verify-mine. - docs/formal.md: how a rule is accepted per mode, and the judge loop's fixed point. - docs/environment.md: the empty registry, the node budget argument, the env record. - CHANGELOG: mining per mode, the checkpoint, verify-mine, the sidecar, the switches, the retired router, and the breaking calls (`prune_covered_rules`/`deduplicate_rules`/`promote` need `rule_mode`; the sidecar's `triple` is now `gates`/`per_length`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`ac_judge` answered in a fixed reading -- the default set with folding off, the legacy mark R2b retired from the mine -- without naming a mode, the last mode-less entry. Its callers, all tests, now ask the mine's mark (`mine_mark`) in the mode they mean, and the retired-twins test lists it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…borrowed" The Python shim installed a lazily built mode set by string-matching pyo3's "Already borrowed" error, sleeping 2 ms and retrying for up to 60 s, with a condition variable parking new readers so the push could land. The cause: `set_mode_rules` took `&mut self`, so pyo3's borrow flag refused it while any reader was inside the core. The push needs the engine exclusively because it extends the append-only token table. The pyclass is now `frozen` (every method takes `&self`, no borrow flag), the engine sits behind a `RwLock`, and the push takes the write lock with the GIL released: it waits for the calls in flight, and new calls queue behind it (std's RwLock on Linux prefers writers). A guard that spans `py.detach` is taken inside the detached closure, so no reader holds the lock while it waits for the GIL. Deleted on the Python side: the retry loop and its deadline, the string match, the fairness condition variable and `_await_no_pending_push`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… call There were two lazy layers. `modes=` decides which sets the core receives, and the core then translated each received set only on that mode's first call, so `load(modes='all')` returned before any mode was ready and the first call per mode paid the translation (seconds on acj-5-4-llm). Now there is one: `from_strs` and every `set_mode_rules` push translate every set the core holds before returning (GIL released). A mode named at load is ready when `load` returns; a mode deferred by `modes=` builds and translates in one step on its first use, as before. The translated sets are the same structures, so answers do not change; the RSS figures in the `modes` docstring and the artifacts guide are re-measured with them included. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The dialect of an expression argument was detected in four places with different rules: inline in `simplify` (and a copy in `complexity`), `_conversion_input` for the conversion API, `normalization._input_dialect`, and a re-detection inside `_explain_invalid`. They disagreed: only the conversions read realization notation, only `simplify` checked an ndarray's shape and dtype, and `normalization` ravelled an N-D array the others refuse. `_read_input` is now the one reading, used by `simplify`, `complexity`, `prettify`, the conversions and `simplipy.normalization`; `_explain_invalid` is handed the form `is_valid` already decided. Measured effects: `simplify(['simplipy.operators.neg', 'x1'])` reads like `to_prefix` (it raised "invalid or malformed prefix expression"), and `complexity(np.array([['x1']]))` raises a clean ValueError (it raised pyo3's raw TypeError). A bytes ndarray is decoded instead of passed through as `b'..'` reprs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…s first The twin loop checks G7 before the cross-rule guards, and `ordered_below` is a strict total order, so a twin that is the reverse of a loaded rule never reached the "twin-inverse" check. A debug assertion states that asymmetry at each admitted twin. The asset-side guard stays (it is reachable: 3 rows in the real set). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`rewrite_pass` (owned loop) and `rewrite_pass_opt` (borrow-side visit) each carried the whole fire / fold / rebuild / composite / memo protocol, so every acceptance change had to be made twice. Both entries now run one `visit`, which returns what it decided (normal form, fold, or descent step); the composite step and the memo mark are helpers. `visit` and `composite_step` are inlined into both entries, so the walk's recursion keeps the frame layout of the two former copies. Same steps, same memo marks, same traces. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…orpus STEP_CAP used to bind silently: the walk stopped firing and memo-marking, and the answer could be a non-fixpoint with no signal. Every step the cap refuses is now counted (`ac::rules::step_cap_binds`, exposed as `Engine.step_cap_binds()`), and a cargo test walks the 400-row corpus in all three modes at the default effort and asserts the count stays 0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…d-local The up-to-sign retry read a thread-local counter before and after the first match to learn whether a near miss occurred. The counter is now a `Cell` in `MCx`, the context every match of the pass already shares, so the signal is scoped to the matches that produced it. The gate itself is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The Python corpus gate already walks the 400 rows at the deployed default effort; it now also reads `Engine.step_cap_binds()` after the walk, so the counter has an in-repo reader on the Python side too. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
Removed from `_core.Engine` (and the stub): `ac_odd_neg_carriers` (the instrument of the closed F80 E3 read), `interval_zero_set_null_generic_const` and `interval_entire_analytic_composition` (F80 E2 design-read probes), and `registry_pole_refusals` with the counter it was the only reader of. Nothing in the package, tests, benchmarks or docs called them. `ac_node_census` stays: the tests use it. The interval test that went through the probe wrapper calls the gate directly. Two of the clippy warnings go with `ac_odd_neg_carriers`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`ac_canonical_key` drops a needless `Some(..??)`, the miner's class-quotient map gets a named key type, and the worker copies an `Option<Vs>` instead of cloning it. The one warning left (`identity_op` on `MU_RAT_FLOOR` in rust/ac/expr.rs) waits for the pending expr.rs branch. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…a fixpoint
The pass re-enters every node it changes, so its output is a pass fixpoint. Debug
builds now assert that after every productive pass of the chain (both permissive
phases included), against a FRESH pass with an empty memo, so the check cannot
trust the marks the pass placed itself. The cargo suite (corpus gates, and the
step-cap test in all three modes at the default effort) passes with it.
`max_passes` stays as the public safety cap. The core used to read 0 as 1 through
`.max(1)` in three loops; it now reads it literally (0 runs no pass: the canonical
form), which is what `is_valid`'s parse-only projection always said it did.
`simplify(max_passes=0)` now raises ValueError ("must be at least 1") instead of
silently running one pass; the documented "0 is treated as 1" is gone. Docs drop
the "2-4 passes" figure for the asserted one-pass fixpoint.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`ac_simplify_in_mode`, `ac_simplify_infix_in_mode` and `ac_simplify_suppressed` defaulted `explore_budget` to 0 (the chain alone) while `simplify` and the core's `prettify` default to None (search until a round finds nothing), so a direct `_core` caller that omitted it silently got a different answer. All four now share the public default. Every production caller already passed the budget, except `is_valid`'s parse-only projection, which now states 0; the tests that meant the chain alone state 0 too, and the effort test pins the FFI default to the public one. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… symbols, not lines In rust/lib.rs, `ensure_ac_well_formed`'s doc was fused onto `parse_rule_mode`, `ac_canonical_keys`' doc onto `ac_node_census`, and `core_serialization_ops`' doc onto `set_interval_node_budget`; each now documents its own item. Two comments in rust/interval.rs cited `rust/lib.rs:764`, which is another function now; they name the `interval_value_set_box` contract instead. Comment-only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…ty feature are gone `Tape::eval_row`, `interval::infinite_set_null`, `positive_ae` and `defined_measure_p` had no production caller and shipped behind `allow(dead_code)`; they are now compiled for the tests only. `Engine::operators_ref` and `worker::select_best` carried `allow(dead_code)` while production code calls them; the allows are gone. The `fast-assets` cargo feature gated nothing. (`ac::convert::canonical_tokens` is test-only too; it is left for the pending convert.rs work.) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
`ac_node_census` was exported but not stubbed, and `find_rule` marked six parameters as required that the core defaults (a test relies on the defaults). A new test compares the stub's public names with the compiled module, `Engine` and `CandidateLibrary`, both ways, so an export added or deleted without its stub fails the suite. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… in the core `utils.is_numeric_string`, `_looks_numeric` and `reserved_numeric_spelling` were Python copies of `rust/utils.rs` kept "in sync" by comments. The core now exports `is_numeric_string` and `reserved_numeric_spelling`, the Python functions call them, and the copies (two grammar regexes, `_looks_numeric`, the radix table) are deleted. `literal_float` and `evaluator_literal` read the grammar through the same call. Parity before the switch, on 353,356 fuzzed tokens (random strings over digits, signs, dots, exponents, slashes, underscores, radix prefixes, parentheses and words, plus structured numerals and near misses): - `is_numeric_string`: 0 mismatches. - `reserved_numeric_spelling`: 79 mismatches, every one a token with whitespace (` 21_07`), which Python's `float()` strips and Rust's parser does not. The core refuses whitespace in any token at its boundary, so the difference never reached an engine call. `literal_float` stays: against the core's own literal reader (`numeric::leaf_value` restricted to numerals) it differs on `-0` and `-00` (+0.0, as the deployed evaluator reads an integer, against -0.0) and on a fraction beyond Python's integer-string limit (None against 0.0). It is the deployed evaluator's reading, not a copy of the core's. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The contract judge reads every value at a point from the core's table and judges the specification's criterion. Its own definitions of the values go where it was their only user (the float64 operation table and range test, the singular-input scoping, the 5% grid bar); the mpmath kernels stay for the monitor and promotion until they read the table. - Clause (a) holds at every binding where the left side has a value: a disagreement on a null set is no longer tolerated (`pow(0, asinh(_0)) -> pow(0, _0)`: +inf against pow(0, -1)). - Clause (b) is measured by certified cells of the interval layer, read in the table's values at every point a cell holds (`with_table_points`), not by a fraction of a grid: `x0 + 0*sqrt(x0^2 - 0.01) -> x0` is refused; `tan(asin(ceil x0)) -> atanh(ceil x0)` is refused in real (undefined against +inf on (0, 1]). An undecided cell search refuses (`UNDECIDED-MEASURE`). - A ground rule has no tolerance (`log(-1) -> 0`, `exp(tan(asin(1))) -> inf` refused in real); a `_` slot owes +-inf and NaN (`0*tanh(_0) -> 0*_0` refused); `!` and `$` owe nothing at their excused atoms. - Each `<constant>` is its own symbol, with a product battery and a multi-constant witness fit: `exp(x0 + C1)*C2 -> C3*exp(x0)` holds, `pow(rootn(x0, C1), C2) -> pow(x0, C3)` does not. Nothing is owed at a constant where the left side is finite nowhere, in each mode's values. - Permissive holds by clause (a) alone over real-valued bindings: tiers `permissive` (`exp(log x0) -> x0`) and `real-only` join the lattice, and MODE_TIERS with them. - The f64 bar of the 0.15 heads probes each slot over its sort (data finite) and accepts the true value at a range event: `ceil(1/cosh(x0)) -> 1` is core. - `simplipy.verify.licensed` = holds and the named policies, each read from its one place (evidence from certified cells, the load's gates, the ground-composite predicate now shared with the mint's library, the registry, the duplication predicate, the preemption gate). - The ladder: a climbed rung measures the intermediates afresh, a class or a cancellation the large intermediates put past the ceiling is skipped, never convicted, and a witness is not compared at rungs finer than itself. The differential test's phase-2 marks go: the judge's assertions (5, 6 and the table part of 4) pass; 22 marked failures remain, each on a phase-3 step. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…dent slots - Clause (c): where the left side is +-inf only on a null set (the infinite-set certificate, now public as `_core.table_infinite_null`), the right side owes nothing there, for rules with variables: `abs(log(cos x0)) -> log(1/cos x0)` holds in real. - A measure-zero allowance of (b) or (c) needs a slot that guards it. An event that depends on a slot other than `?` (it vanishes when that slot moves to a generic value) refuses the rule: `atan(tan(asin(_0))) -> asin(_0)` and `!0/!0 -> 1` are refused; with a `?` slot the first holds. - Every way two or more `?` slots can coincide is judged as its own rule (up to four slots): `(x0 - x1)/(x1 - x0) -> -1` is refused in real and f64. A cell search that certifies no extension while the grid reads one is undecided, not zero (the cells cannot see through `x - x`). - UNDECIDED-MEASURE refuses real and f64, which both owe (b); permissive keeps its tier. - The diagonal cell check is replaced by the coincidences. On the shipped acj-4-3 triple real now has 77 offenders (+22 unguarded extensions, -1 holding by clause (c)) and permissive 23; the three `abs rootn _0 (-5) -> pow abs _0 -0.2` rules of the f64 file are f64-tier KILLs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- `interval::collapse_licence` is the one licence: a variable-free expression holding a `<constant>` collapses to a fitted constant where it has evidence in the mode's values (`interval::evidence`, defined once and read by `_core.table_evidence`): finite on a set of positive measure of its constants, in float64's values in `f64` and the table's in `real`. `permissive` collapses without evidence. Nothing is owed where the expression is not finite. - The engine's constant fold and its bag absorption read it; the engine's second licence (the permissive shortcut beside `constant_collapse`) is gone. The mint still reads `constant_collapse` until it switches. - `pow(0, C)` now folds to `C` in `f64` and `real` (0 for C > 0, 1 at 0); `(-1)^C`, finite only at the integers, does not. A product absorbs a ground member only where it is certainly nonzero (`C * 0` stays 0). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- The real ground fold reads the table (`table::ground_value`): a ground node folds to its exact value where the table has one and to NaN where it has none: `exp(-inf)` is 0, `tanh(inf)` 1, `acosh(1)` 0, `exp(0)` 1, `sin(pi)` 0; `1/0` and `pow(0, -1)` are NaN (the limit rule), `pow(0, -2)` +inf. The constructor's arithmetic on literals reads the same table (`table_literal_fold`): `pow(1, inf)`, `pow(inf, 0)` and `pow(nan, 0)` are NaN. - permissive's values are real's: it reads one zero (no IEEE signed zero) and the table's literal values, so `1/(x1*0)` is NaN where it was `inf/x1`; its classes come from the table and its finite ground values stay its float fold. A literal infinity keeps permissive's written reciprocal until the pass's fixpoint, so `inf/inf` still cancels as like terms. - The permissive-dominance sweep over the shipped corpus has no violation left (the one row that read float64's signed zero is gone). - The table: a power past its working exponent range is Unresolved, never an infinity (`2^(1e40)` read as +inf), and `max`/`min` of an exact and an approximate value it cannot tell apart is approximate, so `max(2, cosh(acosh(2)))` is not folded to `2`. - Tests that pinned real's +inf at 1/0, permissive's signed zero, and real leaving exact ground values to rules now pin the table's values. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- The judge's table-points switch is the layer's real reading (`with_real_reading`, `ReadingScope`): every point is the table's value, an operation on exact points included (`table_at_points`: `inv(0)` undefined, `pow(0, -2)` +inf, `tanh(inf)` 1), and float64's saturations do not exist (`tanh` stays below 1 past 19.06, `erf` below 1 past 5.92, `exp` above 0 below -745.13). - Every certificate that takes `f64` reads in the reading it names, and the engine runs `real` and `permissive` in the real reading and `f64` in float64's, so the per-engine certificate caches stay one reading each. - `acosh(tanh(x0))` has evidence in f64 and none in real; `rootn(-1, tanh(?0)) -> -1` is a measured KILL instead of UNDECIDED-MEASURE (the index never reaches a nonzero integer). - `_core.interval_value_set_box(..., real=True)` reads the real reading; the differential test's enclosure assertion holds for `1/0`, `pow(0, -1)`, `tan(asin(1))`, `pow(1, inf)`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- `ac::expr::Permissive` names the list (inverse pairs, like terms, constant collapse, literal to float, any slot, f64 rules) and `Agreement` for the steps that hold in permissive by its criterion; every permissive switch in the constructor, the search, the matcher and the collapse licence names its entry (`Cx::permits`, `Permissive::applies_in`), and `Cx::lossy` is gone. `_core.permissive_simplifications()` lists the names. - Inverse pairs cancel in both orders, ignoring domain and branch: `asin(sin(x0))`, `atan(tan(x0))`, `acosh(cosh(x0))`, `exp(log(x0))`, `cos(acos(x0))` are `x0`; a root cancels a power whose exponents multiply to an integer (`sqrt(x0^2)` is `x0`). - Removed: composing an even power under a root that remains. `(x0^2)^(1/4)` was written `x0^(1/2)`, which has no value where x0 < 0; it is now `abs(x0)^(1/2)`. Every other power of a power still composes (it keeps the input's value at every real binding). - `abs`, `max`, `floor` and `min` are untouched: permissive gives real's answer there. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- A decimal whose exponent lies past the exact readers' 4,000 is a table leaf of its own (`Leaf::Dec`, read at the working precision) and the judge's exact `m * 10^k`, up to an exponent of 1,000,000: `2.827881176741212e-244756`, which the engine keeps as written in every mode, no longer makes a rule unsupported. - A test over the engine's answers in every mode checks that each literal it writes reads. - The differential test's remaining marks are the mint's, promotion's and the overlap gate's, and name the step that fixes them (3b). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- The owner's ruling: powers compose naively in permissive, ignoring the sign, a named entry of permissive's list (`Permissive::PowersCompose`). `(x0^2)^(1/4)` is `x0^(1/2)` again, `(x0^3)^(1/3)` is `x0`, `(x0^2)^(3/2)` is `x0^3`; the sound modes compose as before. - The list's last entry reads P3 as ruled: the rules that agree with real's values up to float resolution, except at isolated points, are served (`FloatResolution`, "float-resolution rules served"); `_core.permissive_simplifications()` lists eight entries. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- The owner's reading of P3: permissive's ground values are computed by the table and written as floats. Its ground fold writes the double nearest to the table's value (`table::nearest_f64`, the top 128 mantissa bits rounded once) where it wrote float64's: `floor(tanh(40))` is 0 (float64 rounds tanh(40) to 1.0 and floors that to 1), and `sqrt(exp(19.11787581094798))` is 14170.787488305128 (float64: 14170.787488305119). Its member fold compares the table's values: `mod(sin(1), 2)` is still `sin(1)`, and `floor(tanh(40))` is no `tanh(40)`. One table reading per ground node serves the class, the float and the member. - A nonzero value below the normal doubles has no faithful float and stays as written (`exp(-800)` is no 0), as does a node the table cannot decide (`mod(sin(1), 1e300)`). - Cost, permissive ms per row against 83cf4eb, 1,500 rows, two rounds: t81 3.365 -> 3.475 (+3.3%), predictions 14.40 -> 14.82 (+2.9%); f64 and real unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- permissive admits a rule where its two sides agree with real's values up to 8 units in the last place (F6 on the doubles nearest to the table's values), except at isolated points, where it admitted the rules that hold in float64. A disagreement is isolated where it vanishes when a `?` slot moves off the point and on no other slot's move: a `_` slot bound to a constant subexpression would hold it on positive measure. - `tanh(cosh(-10)) -> 1` holds in permissive (1 - 2e-9566 is the double 1.0); so does `tanh(sinh(atanh(x0))) -> tanh(tan(asin(x0)))`, which differs only at +-1; the `_0` spelling does not, nor does `pow(0, asinh(_0)) -> pow(0, _0)`, which holds in f64. - The table's float-resolution reading (`Ctx::saturate`, `TableExpr.eval_float_resolution`, `table::ground_value_float`): a bounded function inside its boundary band reads as the working float's value there, where the exact reading is Unresolved. The judge's float resolution and permissive's ground fold read it. Past the table's reach (a value beyond the doubles' range, `exp(sinh(-50))`) the judge takes float64's doubles under the range standard. - New tier `f64-only` (holds in f64, not in permissive); MODE_TIERS: f64 holds it, permissive does not. On the shipped acj-4-3 triple permissive's offenders go 23 -> 34. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- real and permissive re-judge a near miss by the table, at the precision the row's intermediates demand (cosh(650)^2 - sinh(650)^2 cancels 565 digits, read at 1,180), confirmed one rung finer; a reading in a boundary band climbs (atanh(tanh(800))). The mine's own 1,024- to 8,192-bit evaluator (Residual, judge_row) goes. - A source row float64 reads off a rounded pole or an exact zero is the table's in real and permissive: tan(asin(ceil(x))) has no value at ceil(x) = 1 (float64: 1.633e16), 1/0 none. - f64 compares the rows of a constant-free pair by F6 (8 units in the last place), the judge's agreement, so log(exp(x0)) -> x0 (34 apart) no longer passes the scan; its bar probes the mined variables over finite doubles (the `?` domain), a range row read by the table: ceil(1/cosh(x)) -> 1 passes. - permissive owes no domain gate (clause (b)): exp(log(x0^3)) -> x0^3 mints there; real's gate reads the reals. - A collapse to <constant> reads the mode's collapse licence (interval::collapse_licence): 0^c mints in every mode, (-1)^c in permissive; an instance where the source is nowhere finite binds nothing. - worker::Lane carries the mode into the scan (rescue, owes_b); the differential test's X2, X6, N2, N10 and R1 marks go. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The CI's rustfmt (1.10.0, Rust 1.99.1, the stable dtolnay/rust-toolchain installs) puts the brace of rust/worker.rs's ground-composite filter on the condition's line; `cargo fmt --check` with that toolchain is clean on the tree. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- promote(): each rule with slots climbs two rungs, its slots respelled at `_` and then at `!`, each asked of verify.licensed in the rule's mode (the judged tier at that sort and the named policies; duplication of a `_` slot among them); it ships at the strongest rung licensed, else at `?`. The derivability refund runs between the rungs on the `_`-promoted set; the seeded cancellation identities join where the judge licenses them. A rule without slots passes through. promote(judge=) takes the mine's judge; two positive controls are asked of it first. - Gone with promotion's own bars: _f64_eval (numpy), _hp_equiv (mpmath), _pointwise (the atom lattice with +-inf for `?`), _const_bearing (the witness map), _overturn (the arbiter) and _ladder (the ground tier, the pow and step preimage witnesses, the spike refusal). ceil(1/cosh(x)) -> 1 ships at `!` in f64 and real, `_` in permissive (X1). - The monitor (verify._monitor) judges each rewrite input -> output with judge_rule, held to the mode's MODE_TIERS; an undecided verdict is UNSCORED; a tagged side is read through the engine. Its evaluator, signed-zero lanes, folds, snaps and tolerances go, and with them verify._contract's OPS and c_* kernels, which only the monitor and _hp_equiv read. monitor_ruleset's result loses `tolerated` and `f64_folds`. - Tests: the instruments' own suites go (test_promotion_gen2, test_periodic_range_refusal, test_judge_upgrade); promotion and monitor tests read the judge. Four strict xfails record what the judge-backed instruments now report: a jump preimage the judge's battery misses (ceil(sinh(x) + 1/2) - floor(sinh(x) + 1/2) -> 1 is tier real), and three f64 engine answers the judge refuses or cannot decide (the asinh(sinh(s)) - s residue, x0^x1 * x0^x1 -> x0^(2*x1), the corpus walk's row 263). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… the final gate - mining._licences: verify.licensed of each pair in the mode's file, the judge's tier memoised by pair; the named policies are each read from their one place (the core's evidence, load gates, ground-composite and duplication predicates, the registry, the cell, the preemption gate). - The completion step offers only a completion the mode licenses; the overlap gate lists as missing only a licensed completion the file lacks, and every refused one with the judge's tier and `refused_by` (asin(1) -> acos(0) is a ground composite, no longer demanded: the differential test's X3 marks go). The final gate (before each prune and on what ships) drops a file row refused by the tier or by a policy, `[lhs, rhs, tier, refused_by]`; verify-mine reads both gates, and its CLI counts the refused overlaps by policy. - Promotion's positive controls ask the rule judge itself (verify_rule), so a mine run with a stand-in judge promotes by it unchecked, as before. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…nsed The stopgap retires: the mint builds a source context for a source with several <constant>s (worker::SourceCtx), and the load serves such a rule (ac::rules::translate drops nothing for it; MAX_LHS_CONSTANTS, the multi-constant-lhs drop reason, the load warning and Engine::ac_multi_constant_rules go). The judge reads each <constant> as its own symbol, so the mine's judge loop refuses pow(rootn(x, C1), C2) -> pow(x, C3) (the mint's scan accepts it, as a pre-filter may) and its gates keep what verify.licensed passes; C1*exp(x + C2) -> C3*exp(x) holds in real and permissive. verify.policy_refusals no longer maps multi-constant-lhs to the constant count. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
real's and permissive's source rows are re-read by the table (hiprec::table_classes) before the evidence decision counts them, and an evidence top-up draw counts where the mode's value is finite. tan(atan2(x0, 0)) has no value off x0 = 0 in the reals, where float64 gives 1.633e16, and the interval layer certifies cells of x0 > 0 as finite (it reads the pole of tan at a varying argument as a null set, and atan2(x, 0) is pi/2 on all of x > 0): with its rows read by the table after the evidence decision, every target matched the remaining x0 = 0 rows, the judge refused each, and the reduced mine stopped at length 4 in real (the judge loop gave up on the source after eight refusals). It is uninformative now in real and permissive. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
… is dropped Found by the reduced mine: the real and permissive files lacked 16 and 25 completions the mode licenses, each refused by a mint check stricter than the judge. - hiprec::rescue skips a row the table cannot read up to MAX_DPS (erf(sinh(-100)) is -1 + e^-(1.7e86)), as the judge skips a point it cannot resolve; range_rescue likewise. - table_row: where the source is +-inf, a candidate with no value owes nothing at a row of a rule with variables (the judge's isolated infinity; sinh(atanh(x)) -> tan(asin(x))). - table_classes reads a value float64 gives off a rounded zero (0 < |y| <= 1e-15) by the table, as one off a rounded pole (tan(acos(-1.0)) is -1.2e-16, tan(pi) is 0); table::is_exact_zero. - The special-point battery checks float64's divergence in f64 only (the specification's step table), reading the lane's mode; in permissive a REAL-CHANGE at one special point is no refutation, nor is the exceptional-point pole refusal, nor a sampled row whose disagreement a move of one variable clears (hiprec::IsolationScope, isolated_row): P3 excuses an isolated point and its judge decides one. - find_rules' liveness gate drops a rule the engine holding the file never fires (permissive's inverse pairs, cancelled ignoring the branch, reach abs(atanh(tanh(x))) before abs(atanh(tanh(_0))) -> acosh(cosh(_0)) can match), listed under gates.dead. The differential test gains the cases; the Rust tests read real's lane without float64's divergence check (atanh(tanh(tan x)) -> tan x and the seam class are `real`). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…skipped A row the table cannot read is skipped (the judge skips such a point), so climbing the precision ladder to read it bought nothing a refutation needs and cost much: the reduced mine's real length-4 scan ran at a third of its speed (26 against 69 sources per second 13 minutes in). The row is read at the precision its intermediates demand and confirmed one rung finer; a reading Unresolved at either is skipped (atanh(tanh(800)) included). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
hiprec::isolated_row excused a disagreement that vanished on one move of a variable, and a move out of the source's domain reads as agreement: ceil(acosh(asin(x))) -> 1 differs at x = 1 and on (0.99961, 1], and the move above 1 left asin's domain, so the mint took eight targets the judge refused and the reduced mine stopped at length 4 in permissive. A disagreement is isolated now where it vanishes on both sides of the point; the differential test gains the pair. The CHANGELOG reads the table rows as they are read (no climbing). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…de's values - CHANGELOG: the reduced length-4 mine (seed 42, 4 threads) writes 429 f64, 495 real and 682 permissive rules in 4,104 s; verify-mine holds every gate of the f64 file and every gate but the overlaps of the real and permissive files (2 and 4 licensed completions missing, each named); every rule with a variable the files lose is served or no longer licensed. - test_permissive_literal_fold: permissive writes each ground node's table value as a float and f64 folds in float64, so the cosine of a 9,121-radian argument parts the two answers (14.817389436549217 and 14.817389436549087; the true value is 14.817389436549068...). The test pins both; it failed since permissive's ground values became the table's. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
integration/0.15's CI refused (x0 + C)^2 -> x0^2 + C1*x0 + C2 in real on py3.12 and certified it on py3.13. Both jobs installed the same numpy 2.5.4, scipy 1.18.1 and mpmath 1.4.1, and the verdict does not depend on the interpreter or the hash seed: it depends on the OpenBLAS kernel the runner's CPU dispatches. fit_witness_multi's Gauss-Newton read J.T @ J, np.linalg.norm and np.linalg.solve, whose summation order follows the kernel; forcing OPENBLAS_CORETYPE reproduces the CI on one machine (Haswell, Nehalem: certified; Sandybridge, Prescott, Core2: KILL). Two defects carried those last bits into the verdict. At <C_L0> = 0 the fit returned -2.5e-17 for the exact 0: the per-coordinate snap trials were built from the unsnapped fit and, on a tie, undid the joint snap. mp_polish_multi then took the noise to ~1e-557 instead of 0, a nonzero right side at x0 = 0 where the left side is exactly 0 (a class change, KILL). The fit now sums exactly rounded (math.fsum: _norm and the normal equations) and solves in plain float arithmetic (_solve, Gaussian elimination with partial pivoting); every snap trial reads the current fit; the polish keeps an exact zero where zero fits as well at every environment, as mp_polish does. The fit's trace is bit-identical under every OpenBLAS kernel and on py3.12.13 and py3.13.13. (x0 - C)^2 -> x0^2 - C1*x0 + C2 and (x0 + C)/C -> C1*x0 + C2, refused on every kernel before, hold in real. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
S1. ceil(sinh(x) + 1/2) - floor(sinh(x) + 1/2) -> 1 is false in real only where sinh(x) + 1/2 is an integer: transcendental points no battery, grid or double holds, so the judge passed it in real. _judge_contract now probes the jump preimages along each grid lane (_jump_probes): where an argument of floor, ceil, mod (literal divisor), harmonic or atan2 crosses a level between two grid points, and where an abs, max or min under one of them has its kink or switch, the preimage is solved (Illinois, 30 digits then 500) and judged with every subtree equal to the solved argument replaced by its exact level (for a switch, the other argument), so each head reads its value at the level. A point where a side, so substituted, is not continuous across the preimage is skipped; levels stay within the doubles' exact integers (past them the table reads a level that rounds onto an integer as exact). f64 reads the 17 doubles nearest the preimage. At most 16 preimages a rule, 4 tries per lane and level set, nearest the origin first: about 0.1 s more on a rule with a jump head. The rule above is permissive (refused in real and f64); the strict xfail goes. floor(_0 + 1) -> floor(_0) + 1 and kin read ENGINE-MISALIGN now (tier real as before): the doubles next to the preimage show the f64 lane the break the f64 bar saw. S2. The judge's f64 lane read a grid whose smallest magnitude is 0.0137, so log(exp(atanh(_0))) -> atanh(_0) (float64 loses exp's 1 + y for small y) was admitted in f64 while the mint refuted it on its rows. The mine's sampler is one function (_contract.mine_rows, RuleMiner._mining_sample_x calls it); the judge reads the deployed sides at every row of the mine's sample and confirmation matrix (judge_rows: the shipped mine's, seed 42 x 1,024 x 2 confirmed, by default; find_rules and certify_rules set their own for the extent of the mine, the judge pool's workers receive them, and verify_mine draws them again from the sidecar's seed and shape) through TableExpr.eval_f64_rows, and judges the first 8 rows where float64's sides disagree (F6) as grid points, in the reals and in f64. On the published acj-4-3 triple: f64 offenders 6 -> 25 (pi - acos(_0) -> acos(-_0) cancels near -1, 77 ULP at -0.99971), real 77 -> 79 and permissive 34 -> 36 (sin(abs(atanh(_0))) -> abs(sin(atanh(_0))) and its twin, false where atanh passes pi near 1). The differential test sets the judge's rows to the mint's and checks the example. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…one rounding, 4.8 - O2 (i) The near-miss gate bounds the work, not the verdict (hiprec::rescue): a wide miss has WIDE_MISS_ROWS = 4 of its failing rows, spread over them, read by the table, and the mint refuses at the first confirmed disagreement. floor(erf(cosh(x))) -> 0 (float64 rounds erf to 1 on most rows) is minted in real and permissive. - O2 (ii) Evidence is one function: interval::evidence confirms a certified cell at four points drawn in it (a cell is finite almost everywhere; its centre may be the null set, 1/x on [-64, 64]), read in the mode's values by the table, and the mint's source decision (worker::evidence_rows, the source context now taking the lane's mode) reads it, or for a variable-free source of constants the collapse licence in the mode (permissive collapses without evidence, 4.9). tan(atan2(x, 0)) -> nan has no evidence in real and permissive for the mint and the policy alike. - O2 (iii) The overlap completion runs to its fixpoint: each round settles the set with the final gate first and asks the gate's question there; a completion the mode did not license is asked again on the next round's set, one the mint refused is offered again once the set has moved (keyed by the set it was offered against); the pass ends when a round offers or certifies nothing (_COMPLETION_ROUNDS = 32, a safety cap). - A P4's move is defined once (table::ISOLATION_STEP = 2^-20, table::isolation_move, exported as TABLE_ISOLATION_STEP): the judge's permissive criterion reads it and asks both sides (a slot whose move clears the disagreement in each direction, and only ? slots moving it at all), the mint's isolated_row moves its rows by it. An unresolved exact reading at a moved point is read at float resolution (tanh(sinh(atanh(x))) -> tanh(tan(asin(x))) just below 1). - B The monitor reads F8: every rule step the engine took (the new Engine.ac_simplify_fires, a FireLog at the matcher's four fire sites) judged in the mode, and a rewrite the mode does not license as a whole is OK where it holds in the reals and float64's disagreements are what rounding does (the judge records their kinds, f64_kinds: ROUNDING, SIGN, EXT, and the class changes and ZERO-SIGN F8 does not let pass); a step that holds in the mode alone leaves such a rewrite UNSCORED, float64 unread too. On the acj-4 engine with no rules (223-row corpus, seed 5) 2 native refusals and 8 unscored of 186 rewritten (6 and 7 before): x/(x/(x^2 - x)) -> x*(x - 1) and tan(x + pi) -> tan(x) pass, and 1/(0 - x^4) -> -1/x^4 (a zero's sign) and (-x)^(-1/2) -> 1/(-x)^(1/2) stay refused. - 5 Permissive rounds a ground subtree once: no literal lands inside a ground node (ac::expr::in_ground at the five landing sites), so the table values the subtree whole and the ground fold writes its nearest double: the stream draw is 14.81738943654907, the double nearest to 14.817389436549068 (14.817389436549217 before). - 6 (4.8) What the engine does itself is refused where the mine first considers it: the per-length loop (RuleMiner._unlicensed) refuses a ground pick the rule-less engine already takes to its right side and a pick that does not fire on its own generic instances with the length's picks installed; the final gate checks preemption and liveness and drops nothing (the liveness drop goes). - The core stub, tests (the differential test's P4, wide-miss and evidence examples, the mine's first-consideration refusal, the monitor's step and exact-algebra readings), and the CHANGELOG. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
Reading four failing rows of every wide miss by the table made the reduced mine's real length-4 scan about eight times slower (8 sources/s against 76 at the same point of 3b's mine): every false const-free candidate cost a table reading. A wide miss of float64 is no disagreement of the reals only where float64 misreads a side, and the source is one per scan: rescue now asks source_faithful (float64's value within 1e-12 of the table's, its class the same, on 16 binding rows spread over them; once per source instance, cached per thread) and reads the failing rows only where the source is misread; where it is read faithfully the miss is the candidate's and is refused as before. floor(erf(cosh(x))) -> 0 is minted still. table_row also reuses its first readings at the first rung and fails a gross disagreement there (a residual a millionth of the larger side, at the precision the intermediates demand) without a second rung. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The judge's two-sided isolation counted an extension as a disagreement (the left side without a value, the right side with one), so a permissive rule that differs at a point and extends on one side of it was refused: acos(ceil(acos(x))) -> 0 differs at x = 1 alone, both 0 below it, the left side undefined above it. Permissive's criterion owes nothing where the left side has no value, so the move off the point reads an extension as agreement, as the mint's isolated_row reads Extend. Re-judged with it, the 3b reduced mine's files keep every real rule, 679 of the 682 permissive rules and 426 of the 429 f64 rules (it refused 30 permissive rules without it, and with it refuses ceil(erf(sinh(x))) -> ceil(sin(x)) and its floor twin, which differ on (pi, 2*pi), not at an isolated point). The first reduced mine at c022201 met it as 468, 222 and 141 permissive picks refused round after round of its length-4 judge loop. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
- The reduced mine at 81009bf failed in permissive: its length-4 judge loop refused 402, then ever fewer picks, and gave up on 22 sources after 8 rounds each (erf(cosh(cosh(x))), tanh(exp(cosh(x))), erf(pow(x0, x1)) and kin, every pick a false candidate). Their rows past small x lie inside erf's or tanh's boundary band at every rung, so the four spread rows of a wide miss were often all unreadable and the pick passed on to the judge unread. A wide miss now reads its failing rows, a spread of 16 first and then the rest, until four are read, and passes on only where some row was read and none disagreed (WIDE_MISS_TRIES). Emulated on the mine's rows, the stubborn sources end in no pick or a licensed one within two rounds; floor(erf(cosh(x))) -> 0 is still minted. - saturation_verdict read a slot's written bound off the battery as an mpf, and a battery atom is a TV: erf(cosh(cosh(_0))) -> _0 raised TypeError at _0 = 2 (since the battery became the table's atoms; the mine's judge read the exception as a refusal). It reads the atom's value. The mint-row lane binds its rows as mpf, as the grid does. - CHANGELOG: P4's extension reading, the wide miss, the saturation rule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The reduced mine at aa25d5b failed in permissive on one source: atanh(harmonic(ceil(x1))), each of eight picks (0, ceil(x1), -ceil(x1), ...) refused by the judge. Where ceil(x) = 1 the left side is atanh(H_1) = atanh(1) = +inf, but the table computed H_1 as an approximation of 1, which atanh's boundary band leaves unreadable at every rung: the mint skipped those rows and passed each candidate on. table::harmonic now returns H_n as the exact rational for an integer 0 <= n <= 64 (harmonic_exact), so the pole is read where it is; emulated on the mine's rows the source ends in a licensed pick (atanh(ceil(x1)), permissive) in one round. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
assets/engines/acj2-4-llm holds acj2-4's operators and its complete 4->4 mine settings, with acj-5-4-llm's batch of 194 LLM proposals offered beside the scan, as acj-5-4-llm does at 5->4. The acj2-4 and acj2-5-4-llm mine settings lose a comment that said the new heads cannot enter the real file; they can since the real kernels landed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
The test pinning the acj-4-3 triple's offender counts printed only a truncated report, so a count that differs on another machine did not say which rule moved. It now prints every mode's offenders (index, sides, verdict); pytest shows the captured output in full on a failure. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
…ibm decides On the CI runners the f64 lane also refuses row 126 of the acj-4-3 triple, asin(sinh(atanh(_0))) -> asin(tan(asin(_0))): both sides are x/sqrt(1-x^2) under asin, and whether they leave asin's domain at the same double is decided by the platform's math library, which f64 follows by contract. The development host certifies it. The BLAS kernel is not involved (the same counts under the default, SkylakeX, Haswell and Zen kernels). The gate now pins the count of the other 25 f64 offenders and real's and permissive's counts exactly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W
This branch has not been deployed
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
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.
Integration branch for SimpliPy 0.15.0. Draft: work lands here as it is finished, and this PR runs CI on it. It is not ready to merge.
In so far
rootnkeeps the sign of zero on every evaluation surface (IEEE-754rootn(±0, n odd) = ±0), and scalarabs(-0.0)is+0.0. This closes three registered pole residuals.x1*1e-300comes back as1e-300*x1again.requires_simplipy, which is checked at load. The measure fingerprint is recorded per rule file and compared probe by probe.complexity(canon=)explicit_constant_placeholders(convert_numbers_to_constant=)Still to come before review
prettifyWritten by Claude (Claude Code) on behalf of @psaegert.
🤖 Generated with Claude Code
https://claude.ai/code/session_016gamUqKQqroqag4GFsNu6W