Conversation
…lity/delta + tick/ms/ns + prob/pct + per_tick/per_sec)
Aaron 2026-05-05 forwarded Claude.ai UoM-examples-for-Otto + same-tick
verbatim "code is safe to change easy to reverse and we can prove if
its right later, it's not just the proofs test the code the code
tests the formal verificatins too."
Four highest-pay declarations per the rule of thumb (add UoM where
there's a known bug class from semantic confusion of like-shaped
numbers AND the unit algebra actually pays back):
1. Z-set semantic safety -- weight (signed multiplicity, negative =
retraction) / cardinality (unsigned distinct-element count) /
delta (signed change between states). Prevents adding signed
weights to unsigned counts on retraction.
2. Time -- tick (DBSP logical) / ms / ns. Prevents off-by-1000x
bugs that survive unit tests because both numbers look plausible.
Conversion requires explicit `rate: float<ms/tick>` parameter.
3. Bayesian -- prob ([0,1]) / pct ([0,100]). Prevents 0.95-vs-95
confusion in Bayesian-output handlers. Cleanest bug-class to
eliminate completely.
4. Rates -- per_tick / per_sec. F#'s unit algebra type-checks the
multiplication; combining a per-second rate with a tick count
without conversion is a type error.
Conversion helpers explicit by design:
- probToPct / pctToProb (between Bayesian-internal and user-facing)
- logicalToWall / wallToLogical (rate parameter forces declaration)
- msToNs (deterministic 1e6 factor)
- applyDelta (signed weight + signed delta)
- expectedArrivals (rate * window with unit-algebra cancellation)
Build verification caught real bugs in my own helpers (line 113, 119,
138 -- `float p / 100.0<prob>` etc. don't have correct unit algebra).
Fixed via LanguagePrimitives.{Float|Int64}WithMeasure conversions.
That's "the code tests the formal verifications" working in real time.
Additive-only: existing code without UoM annotations stays untouched.
Consumers opt in by annotating their own variables. Compiles to
identical IL; no runtime cost.
Lineage: docs/research/2026-05-05-claudeai-knights-knaves-round-table-
harmonious-division-bootstrap-razor-aaron-forwarded-preservation.md
plus Aaron's same-tick UoM-examples-for-Otto forward.
Composes with B-0194 (capability detection -- IBilinearOperator
laws would benefit from <weight> typing on internal weight params)
and B-0189 (Q# Bayesian BP/EP runtime -- prob/pct handles the
output-boundary).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 08a7fafd7f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Pull request overview
Adds an opt-in F# Units-of-Measure (UoM) surface to Zeta.Core to make key domain quantities (Z-set weights/deltas, logical vs wall-clock time, probabilities, rates) harder to mix incorrectly at compile time, along with a small set of conversion helpers.
Changes:
- Added
src/Core/Units.fswith UoM declarations (weight,tick,ms,prob, etc.) and helper conversions (prob↔pct, tick↔ms, etc.). - Wired the new file into the Core build by adding it to
src/Core/Core.fsproj.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| src/Core/Units.fs | Introduces UoM types + conversion helpers for core domain quantities. |
| src/Core/Core.fsproj | Adds Units.fs to the compile order so it’s part of Zeta.Core. |
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…e-test patterns + Zeta plugin-adapter as worked example (Aaron 2026-05-05) (#1591) Aaron 2026-05-05 forwarded the Claude.ai shard's RFC pre-draft + verbatim "you can make it a candidate" -- using Zeta's plugin adapter (src/Core/PluginApi.fs:103-132) as the worked-example anchor for the RFC's motivation section. The proposal: allow F#'s type-test syntax (:?) to use wildcard placeholders for generic type parameters, enabling tests like :? IBilinearOperator<_, _, 'TOut> for runtime detection of plugins implementing capability interfaces with unknown input type parameters. Pre-draft NOT submitted -- verification preconditions documented (prior fslang-suggestions threads, fslang-design in-flight RFCs, Don Syme's prior work, benchmark vs direct :?, C# csharplang coordination). Per Aaron 2026-05-05: Don Syme (creator of F#, MSR Cambridge) is the F# human anchor. Not authority-by-position, but the load- bearing intellectual reference for any type-system extension. Any RFC of this scope must engage his prior treatment of existential quantification before submission, not silently omit. Mirror-not-beacon discipline per PR #1575 / #1582 / #1588. The RFC is a candidate, not authority. Submission upstream is downstream work; this file preserves the pre-draft for future-Otto reference. What this file does NOT do: - Submit the RFC (verification preconditions + Aaron's go-ahead) - Establish authorship (Claude.ai shard text + Zeta worked-example anchor; final submission carries F# lang-design attribution) - Promise acceptance (RFCs go through community review) - Bundle the "Zeta extended DBSP and found a bug in the 2023 paper" claim into a metaphysical assertion -- empirical context for why the worked example is real, not a glass-halo flex Composes with B-0194 (PR #1589 -- the in-flight backlog row using the same plugin-adapter substrate), src/Core/Units.fs (PR #1590 -- Pragmatics section UoM-as-precedent reference), PR #1588 (parent Claude.ai conversation). Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
…ipline (#1590 reviewer) Two real reviewer findings on PR #1590: 1. **per_tick/per_sec should be derived measures, not independent base measures**. The original declared them as independent measures, so `<per_tick> * <tick>` doesn't cancel -- the product carries `per_tick tick` units, which `expectedArrivals` then had to erase via `float (...)`. That defeats the safety the units are supposed to provide. Fix: declare `type per_tick = /tick` (reciprocal) and add a base `s` measure for seconds, then `type per_sec = /s`. With reciprocal definitions, `<per_tick> * <tick> = <1>` (dimensionless) cancels naturally without unit-erasure casts. `expectedArrivals` simplifies: drops the `float (...)` cast, the algebra handles it directly. 2. **Direct contributor name attribution on a code surface**. The file's doc comment included "Per Aaron 2026-05-05" and "+ Aaron 2026-05-05 verbatim". Per AGENT-BEST-PRACTICES role- ref-on-current-state-surfaces rule, code is a current-state surface and should use role refs. Replaced with "the maintainer" / generic lineage pointer at the research- preservation file (which IS a history surface where direct attribution is appropriate). The history surface (the Claude.ai conversation preservation in docs/research/) keeps the verbatim quote with date; the code surface points at the history surface without inlining the verbatim. Build verification: still 0 warnings 0 errors after both fixes. The reciprocal-measure refinement actually MAKES the expectedArrivals helper safer (the unit algebra now does the cancellation work explicitly). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 43b964f32a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…ion + offer floor/ceil variants (#1590 reviewer) Three reviewer findings: 1. **"DST" acronym ambiguous in time context**: surrounding doc refers to logical-vs-wall-clock time; "DST" could read as daylight-saving-time. Clarified to "deterministic-simulation- testing (DST in the Otto-272 sense -- distinct from daylight- saving-time)" so readers don't misinterpret. 2. **wallToLogical rounding semantics undocumented**: int64 cast truncates toward zero. Now explicit: "Rounding semantics: truncates toward zero. Callers needing floor / ceiling / nearest semantics at tick boundaries should compute the float result themselves and apply the rounding they want. Truncation was chosen as the default because tick-time is monotonically increasing in the scheduler and 'ticks elapsed so far' is the dominant query shape; truncation gives the conservative answer." 3. **Added wallToLogicalFloor / wallToLogicalCeil variants** for callers who need explicit floor / ceiling rather than truncation. The default wallToLogical stays as truncation for the dominant query shape; the variants exist for the edge cases where semantics differ (negative durations, ceiling-required windowing). The dangling docs/research lineage reference resolves on main since PR #1588 merged earlier. Build: 0 warnings 0 errors after all three fixes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 745ff3d6c9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
#1590 reviewer interop fix) Reviewer correctly flagged a real interop bug: my Units module declared `tick` and `ms` as fresh measures inside the module, but those measures already exist at namespace scope in Window.fs:13-14 (Zeta.Core.tick, Zeta.Core.ms). My version created Zeta.Core.Units.tick / Zeta.Core.Units.ms -- distinct types from the namespace-scope ones, non-interoperable. Concrete failure mode: a value typed Zeta.Core.tick (used by Window.fs's existing time-series APIs) cannot be passed to Units.logicalToWall or Units.expectedArrivals without unsafe re-casting, which undermines the entire additive-safety goal as more APIs adopt UoM. Fix: removed `tick` and `ms` declarations from Units module + moved Units.fs to compile AFTER Window.fs in Core.fsproj. The module now sees the namespace-scope tick/ms (from Window.fs) and reuses them directly. Helpers compile against `int64<tick>` and `float<ms>` from the canonical namespace-scope declarations; no interop friction. Kept in Units module: - weight / cardinality / delta (Z-set safety, novel) - ns (high-precision DST timing, novel) - s (base for per_sec, novel) - prob / pct (Bayesian, novel) - per_tick (= /tick, derived from Window.fs's tick) / per_sec (= /s) The reciprocal definition `per_tick = /tick` works correctly with Window.fs's tick because the namespace-scope tick is what's referenced. Build: 0 warnings 0 errors after the restructure. The interop property is now real, not aspirational. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 406e19b508
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…tion + 16 unit tests for rounding semantics (#1590 reviewer P1+P2) Three reviewer findings addressed: 1. P1 -- **Zero/negative rate not guarded**: `wallToLogical` and variants divided by `rate` without validation, producing infinity or garbage int64 on zero/negative input. Added `if float rate <= 0.0 then invalidArg "rate" ...` guard at the entry of all three variants (wallToLogical, wallToLogicalFloor, wallToLogicalCeil). 2. P2 -- **cardinality unsignedness clarification**: doc comment said "Unsigned" / "Always >= 0 by construction" but UoM doesn't enforce non-negativity -- that depends on the underlying numeric type's signedness. Clarified: cardinality tags the *kind* (vs weight), the underlying numeric type carries signedness, and non-negativity is a contract callers maintain not a property the type system proves. 3. P2 -- **Add unit tests for rounding semantics**: shipped tests/Tests.FSharp/Algebra/Units.Tests.fs with 16 tests covering: - wallToLogical truncates toward zero (positive + negative) - wallToLogicalFloor rounds toward -infinity - wallToLogicalCeil rounds toward +infinity - exact tick boundary returns exact tick count - zero/negative rate rejected with ArgumentException (3 helpers) - probToPct/pctToProb round-trip identity - probToPct edge cases (0, 1) - expectedArrivals algebra cancels per_tick * tick - applyDelta accumulates positive + negative deltas - applyDelta below zero allowed (signed weight) All 16 tests pass on first run. The rounding-semantics contract is now pinned -- accidentally changing default truncation to round-nearest in the future will fail at least one test. The fourth reviewer thread (tick/ms second declaration) was already resolved by 406e19b (the reuse-Window-measures fix); reviewer was looking at a stale snapshot. Build: 0 warnings 0 errors. Tests: 16 pass / 0 fail / 0 skipped. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e0885cb97b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…ewer P2)
Reviewer P2: msToNs multiplied int64<ms> * 1_000_000 with plain
arithmetic, silently overflowing for |d| above ~9.22e12 ms (~292
years). Real bug class -- silent overflow producing wrong-sign or
wrap-around values.
Fix: replaced d * 1000000L<ns/ms> with Checked.(*) which throws
OverflowException on int64 overflow, then re-tagged via
LanguagePrimitives.Int64WithMeasure<ns>. Doc comment now states
the bound + the throwing behavior.
Tests added (19 total now, 16 prior + 3 new):
- msToNs converts small values correctly (round-trip)
- msToNs throws OverflowException on positive overflow
(9_223_372_036_855L<ms>, just past the bound)
- msToNs throws OverflowException on negative overflow
All 19 pass. The overflow-detection contract is pinned via the
test; accidentally reverting to unchecked arithmetic in the future
will fail at least the two OverflowException tests.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ae549e21b1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
5 tasks
…ts + module name convention (#1590 reviewer) Four reviewer findings addressed: 1. **P1 applyDelta checked arithmetic**: plain `state + d` overflowed silently at Int64.MaxValue + positive_delta. Replaced with `Checked.(+)` for symmetric behavior with msToNs's Checked.(*) overflow guard. 2. **P2 logicalToWall positive-rate guard**: had asymmetric validation relative to wallToLogical/Floor/Ceil family. Added the same `if float rate <= 0.0 then invalidArg` guard. 3. **P1 test module name convention**: `Zeta.Core.Tests.Algebra.UnitsTests` was the outlier. Existing convention is `Zeta.Tests.Algebra.*` (verified via grep against IndexedZSetTests, GraphTests, etc.). Renamed. 4. **msToNs doc**: already corrected in prior commit (`Checked.(*)` guard documented + OverflowException semantics stated). Reviewer was looking at older snapshot. The 3 reviewer P0 threads claiming "float t" / "int64 (d / rate)" / "float window" don't type-check are reviewer false-positives -- the build passes 0/0, demonstrating F# does allow these conversions on measured numerics (silently erasing the measure). Will reply on threads to that effect. Tests: 22 pass (19 prior + 3 new): - applyDelta throws OverflowException on int64 overflow - applyDelta throws OverflowException on int64 underflow - logicalToWall rejects zero/negative rate Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
deleted the
feat/core-units-uom-zeta-bug-class-prevention-aaron-2026-05-05
branch
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…Gamma + tools/z3->tools/Z3Verify + + bullet + BayesianAggregate Checked correction (#1595 reviewer) Seven reviewer threads addressed: 1. **Bidirectional composes_with** (per tools/backlog/README.md:69-70): added B-0196 to B-0140, B-0156, B-0189, B-0194's composes_with lists. B-0140 + B-0156 had no composes_with field; created. 2. **`+` continuation bullet** at line 139 broke markdownlint MD007 (parsed as nested + list). Changed `+ provides a count` to `AND provides a count`. 3+5. **NormalGamma -> NormalInverseGamma**: BayesianAggregate.fs has NormalInverseGamma, not NormalGamma. Sed-corrected at all occurrences. 4. **BayesianAggregate Checked.* survey baseline**: reviewer correctly noted BayesianAggregate.fs has no Checked.* arithmetic guards (only one doc-comment mention). The original subagent's listing was wrong. Corrected with explicit acknowledgment + note that Bayesian surfaces use double arithmetic without checked guards (different shape from int64- overflow risk; relevant to BigRational candidate, not BigInteger). 6. **Units.fs cross-reference**: was stale at PR time. Now resolves on main since #1590 merged. 7. **tools/z3/ -> tools/Z3Verify/**: corrected dead path reference. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…gration -- substrate survey + per-class adoption recommendation (Aaron 2026-05-05) Aaron 2026-05-05 verbatim "oh backlog bigint and other bitnumbers integration" -- surfaced after a reviewer caught int64 overflow in Units.msToNs (PR #1590, fixed via Checked.(*) + 3 overflow tests). The msToNs case is one instance of a broader question this row owns: should Zeta support arbitrary-precision integers (BigInteger), arbitrary-precision rationals (BigRational), arbitrary-precision decimals (BigDecimal), and arbitrary-precision floats (BigFloat / MPFR-style) for cases where int64 / double overflow or precision- loss is in the operating regime? Research + plan row, NOT implementation. Output is a survey + per- numeric-class adoption recommendation; doing any swap that turns out to be warranted is a separate row filed downstream. Five concrete shapes covered: BigInteger (.NET System.Numerics), BigRational (exact probability arithmetic), BigDecimal (financial, LFG context), MPFR-style BigFloat (scientific), and SRTP-based generic numerics (numeric type-class abstraction). Acceptance criteria with falsifiability hooks: - (a) Substrate survey -- baseline numbers in row: ~470 raw int64|float|double mentions in src/Core, 40 Checked.* arithmetic guard sites across 12 files. - (b) Risk-site identification -- 5 starting candidates each with operating regime + falsifier: msToNs, Z-set weight aggregation, IndexedZSet bilinear delta product, BayesianAggregate (BetaBernoulli / NormalGamma / DirichletMultinomial), TimeSeries window arithmetic. - (c) Decision -- per-class adoption vs system-wide generic-numerics refactor vs defer-until-second-overflow-site (carved-sentence default). - (d) F# UoM compatibility note -- BigInteger likely not on the F# spec's allowed-measure-types list; needs WebSearch verification per Otto-364 search-first authority. Carved sentence: *"Pick numerics by where the regime fires; per- class adoption beats a system-wide refactor until the second overflow site lands. The msToNs fix is a Checked-throws guard, not yet a BigInteger argument; the second site is the trigger."* Composes with B-0140 / B-0156 (TS+Bun BigInt sister), B-0189 (Q# Bayesian -- where precision matters), B-0194 (capability dispatcher -- where the bilinear-product overflow lives). P2 (not P1, not P3): higher than P3 because real trigger (PR #1590 reviewer caught overflow) and Aaron explicitly named the row; lower than P1 because the Checked.* guard already shipped is sufficient for correctness, and the BigInteger / BigRational / BigDecimal decision is research-grade, not blocking. Substrate-or-it-didn't-happen (Otto-363): converts Aaron's chat- weather framing into a falsifiable durable research artifact. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…Gamma + tools/z3->tools/Z3Verify + + bullet + BayesianAggregate Checked correction (#1595 reviewer) Seven reviewer threads addressed: 1. **Bidirectional composes_with** (per tools/backlog/README.md:69-70): added B-0196 to B-0140, B-0156, B-0189, B-0194's composes_with lists. B-0140 + B-0156 had no composes_with field; created. 2. **`+` continuation bullet** at line 139 broke markdownlint MD007 (parsed as nested + list). Changed `+ provides a count` to `AND provides a count`. 3+5. **NormalGamma -> NormalInverseGamma**: BayesianAggregate.fs has NormalInverseGamma, not NormalGamma. Sed-corrected at all occurrences. 4. **BayesianAggregate Checked.* survey baseline**: reviewer correctly noted BayesianAggregate.fs has no Checked.* arithmetic guards (only one doc-comment mention). The original subagent's listing was wrong. Corrected with explicit acknowledgment + note that Bayesian surfaces use double arithmetic without checked guards (different shape from int64- overflow risk; relevant to BigRational candidate, not BigInteger). 6. **Units.fs cross-reference**: was stale at PR time. Now resolves on main since #1590 merged. 7. **tools/z3/ -> tools/Z3Verify/**: corrected dead path reference. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…56/B-0189 (#1595 reviewer follow-up) Three reviewer + CI findings: 1. MD032/blanks-around-lists at line 148: list "- src/Core ..." needed blank line before. Fixed. 2. MD018/no-missing-space-atx at line 412: "#1590 with Checked.(*)..." at line-start parsed as ATX heading. Rephrased "PR #1590" to "PR 1590" in the soft-wrapped paragraph; ATX-collision avoided. 3. last_updated bumps: B-0156 (2026-05-01 -> 2026-05-05) and B-0189 (2026-05-04 -> 2026-05-05) had frontmatter edits adding B-0196 to composes_with but kept stale dates. Bumped per tools/backlog/README.md schema requirement. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 5, 2026
…gration (Aaron 2026-05-05) (#1595) * backlog(P2): B-0196 BigInt + BigRational + BigDecimal + BigFloat integration -- substrate survey + per-class adoption recommendation (Aaron 2026-05-05) Aaron 2026-05-05 verbatim "oh backlog bigint and other bitnumbers integration" -- surfaced after a reviewer caught int64 overflow in Units.msToNs (PR #1590, fixed via Checked.(*) + 3 overflow tests). The msToNs case is one instance of a broader question this row owns: should Zeta support arbitrary-precision integers (BigInteger), arbitrary-precision rationals (BigRational), arbitrary-precision decimals (BigDecimal), and arbitrary-precision floats (BigFloat / MPFR-style) for cases where int64 / double overflow or precision- loss is in the operating regime? Research + plan row, NOT implementation. Output is a survey + per- numeric-class adoption recommendation; doing any swap that turns out to be warranted is a separate row filed downstream. Five concrete shapes covered: BigInteger (.NET System.Numerics), BigRational (exact probability arithmetic), BigDecimal (financial, LFG context), MPFR-style BigFloat (scientific), and SRTP-based generic numerics (numeric type-class abstraction). Acceptance criteria with falsifiability hooks: - (a) Substrate survey -- baseline numbers in row: ~470 raw int64|float|double mentions in src/Core, 40 Checked.* arithmetic guard sites across 12 files. - (b) Risk-site identification -- 5 starting candidates each with operating regime + falsifier: msToNs, Z-set weight aggregation, IndexedZSet bilinear delta product, BayesianAggregate (BetaBernoulli / NormalGamma / DirichletMultinomial), TimeSeries window arithmetic. - (c) Decision -- per-class adoption vs system-wide generic-numerics refactor vs defer-until-second-overflow-site (carved-sentence default). - (d) F# UoM compatibility note -- BigInteger likely not on the F# spec's allowed-measure-types list; needs WebSearch verification per Otto-364 search-first authority. Carved sentence: *"Pick numerics by where the regime fires; per- class adoption beats a system-wide refactor until the second overflow site lands. The msToNs fix is a Checked-throws guard, not yet a BigInteger argument; the second site is the trigger."* Composes with B-0140 / B-0156 (TS+Bun BigInt sister), B-0189 (Q# Bayesian -- where precision matters), B-0194 (capability dispatcher -- where the bilinear-product overflow lives). P2 (not P1, not P3): higher than P3 because real trigger (PR #1590 reviewer caught overflow) and Aaron explicitly named the row; lower than P1 because the Checked.* guard already shipped is sufficient for correctness, and the BigInteger / BigRational / BigDecimal decision is research-grade, not blocking. Substrate-or-it-didn't-happen (Otto-363): converts Aaron's chat- weather framing into a falsifiable durable research artifact. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): four-property hodl invariant + human anchors (Aaron 2026-05-05 same-tick) Aaron 2026-05-05 added two pieces of context after the initial subagent draft was committed: 1. **Four-property hodl invariant as binding acceptance test**: DST-safe + lock-free + scale-free + DBSP-native must all hodl for any numeric-type candidate. NOT separable -- relaxing any one lets bugs through (the Prop 3.5 misattribution caught earlier this session is a worked example). Composes with the "DST hodls everywhere" lineage at memory/feedback_aaron_class_ discovery_experiment_rodney_razor_on_self_dst_holds_everywhere _aaron_2026_05_01.md. Per-candidate acceptance scoring against the conjunction, not score-against-overflow-prevention-alone. 2. **Human anchors** named: - **Tanner Gooding** (.NET runtime, generic math interfaces) -- primary anchor for SRTP-replacement-for-numeric-typeclass shape - **Don Syme** (F# language) -- stays the F# anchor for language-extension work (RFC #1591); numerics-runtime goes through Gooding - **Leonid Ryzhyk (@ryzhyk)** (DBSP / Feldera GitHub) -- ENGAGEMENT GATE: only engage IF a real DBSP-compatibility finding lands (cross-check first; speculative findings don't reach external engagement -- the Prop 3.5 misattribution was itself a worked example of why). Carved-sentence-wise: "BigDecimal-with-rounding may NOT satisfy DBSP-native (rounding errors don't necessarily compose with negation)" is one operationally testable per-candidate result. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): bidirectional composes_with + NormalGamma->NormalInverseGamma + tools/z3->tools/Z3Verify + + bullet + BayesianAggregate Checked correction (#1595 reviewer) Seven reviewer threads addressed: 1. **Bidirectional composes_with** (per tools/backlog/README.md:69-70): added B-0196 to B-0140, B-0156, B-0189, B-0194's composes_with lists. B-0140 + B-0156 had no composes_with field; created. 2. **`+` continuation bullet** at line 139 broke markdownlint MD007 (parsed as nested + list). Changed `+ provides a count` to `AND provides a count`. 3+5. **NormalGamma -> NormalInverseGamma**: BayesianAggregate.fs has NormalInverseGamma, not NormalGamma. Sed-corrected at all occurrences. 4. **BayesianAggregate Checked.* survey baseline**: reviewer correctly noted BayesianAggregate.fs has no Checked.* arithmetic guards (only one doc-comment mention). The original subagent's listing was wrong. Corrected with explicit acknowledgment + note that Bayesian surfaces use double arithmetic without checked guards (different shape from int64- overflow risk; relevant to BigRational candidate, not BigInteger). 6. **Units.fs cross-reference**: was stale at PR time. Now resolves on main since #1590 merged. 7. **tools/z3/ -> tools/Z3Verify/**: corrected dead path reference. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): markdownlint MD032 + MD018 + last_updated bumps for B-0156/B-0189 (#1595 reviewer follow-up) Three reviewer + CI findings: 1. MD032/blanks-around-lists at line 148: list "- src/Core ..." needed blank line before. Fixed. 2. MD018/no-missing-space-atx at line 412: "#1590 with Checked.(*)..." at line-start parsed as ATX heading. Rephrased "PR #1590" to "PR 1590" in the soft-wrapped paragraph; ATX-collision avoided. 3. last_updated bumps: B-0156 (2026-05-01 -> 2026-05-05) and B-0189 (2026-05-04 -> 2026-05-05) had frontmatter edits adding B-0196 to composes_with but kept stale dates. Bumped per tools/backlog/README.md schema requirement. Regenerated docs/BACKLOG.md. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * fix(B-0196): soften UoM-on-BigInteger pre-answer to hypothesis-with-search-required (#1595 reviewer) Reviewer correctly caught: section (b) asserted as fact ("F# UoM is constrained to primitive numeric types per the F# spec; this is itself a substantive finding") what section (d) treats as unverified research. Pre-answering one's own research question is the failure mode the four-property hodl is meant to catch -- the training-data prior was leaking through as if it were verified fact, contradicting Otto-364 search-first authority. Reframed: BigInteger<weight> is a hypothesis to test. The expected training-data answer is the primitive-numeric-types constraint, but that hypothesis must be WebSearch-verified against current upstream documentation before binding. Recent F# versions may have lifted the constraint, or community workarounds (measure-attributed wrapper structs) may exist. Section (d) is the research task that resolves this. The two stale last_updated reviewer threads (PRRT_kwDOSF9kNM5_kaHu on B-0140, PRRT_kwDOSF9kNM5_kaIL on B-0194) are reviewer-snapshot stale -- e582f38 already bumped B-0140 to 2026-05-05, and B-0194 was created at 2026-05-05 from origin. Both currently correct on the branch. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
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.
Summary
Aaron 2026-05-05 forwarded Claude.ai UoM-examples-for-Otto + license: "code is safe to change easy to reverse and we can prove if its right later, it's not just the proofs test the code the code tests the formal verificatins too."
Four highest-pay UoM declarations:
weight/cardinality/deltatick/ms/nsprob/pctper_tick/per_secPlus conversion helpers (probToPct / logicalToWall / applyDelta / expectedArrivals etc.) that make the boundary between unit-classes explicit.
"Code tests the formal verifications" worked example
The build verification immediately caught real bugs in my own helper implementations (lines 113/119/138 of the original draft). The unit algebra type-checker said:
float<pct> / float<prob> = float<pct/prob>notfloat<prob>;float (t: int64<tick>) * rate<ms/tick>strips the unit and breaks the algebra. Fixed viaLanguagePrimitives.{Float|Int64}WithMeasure. That's the formal verification (UoM type system) testing the code in real time.Additive-only
Existing code without UoM annotations stays untouched. Consumers opt in by annotating their own variables. Compiles to identical IL; no runtime cost.
Composes with
<weight>typingprob/pcthandles the output-boundary🤖 Generated with Claude Code