ARCADIA-Studio/harness/release-analysis-numeric-implementation-20260911.md

Exact analysis numeric foundation: implementation handoff

Codex-956atf /root/requirements_delta, 2026-09-11. Root ratified the property-base/shared-check/full-capture, R6/R7 and nominal compatibility architecture after independent review C1. This bounded production lease owns only new crates/oa-core/src/analysis_numeric.rs, its analysis_numeric/ files, and this report. Root retains Cargo, dependency/lock changes, module declaration, production adapters, integration tests, ledgers and release publication.

Read Gitea through #170 before implementation, coordinated ownership in #171, read Wiki Home and fetched updated AGENTS.md blob d93cddacdd through Gitea. Resumed coordination through #195, including the independent numeric review lease #191. The new coordinated milestone-prerelease requirement belongs to root's release ownership; an undeclared numeric module is not an independently runnable milestone.

Status and integration needs

Written, not yet compiled or executed: reusable exact rational arithmetic, literal/wire admission and formatting, bounded dimensions, nominal numerical scalar operations, affine/linear unit coordinates, request-local work accounting, and 26 Rust test functions. The module is deliberately not declared in lib.rs, so current builds cannot accidentally claim these tests or semantics. Standalone rustfmt completed successfully on the owned module tree; no Cargo, rustc, native application, current Project/source/API, prior frozen evidence, commit or push work occurred.

Root approved these exact dependency choices. Add them to oa-core directly or via workspace dependencies according to the integration convention, and resolve/preserve the lock with the sole Cargo writer:

num-bigint = "0.5.1"
num-integer = "0.1.47"
num-traits = "0.2.19"

Use their default std features; no rand, num-bigint serde, floating libm or num-rational dependency is needed. Existing serde/serde_json/thiserror supply wire and diagnostic support. The maintained num-bigint manifest identifies 0.5.1, Rust 1.60, num-integer ^0.1.46 and num-traits ^0.2.18; this fits the workspace's Rust 1.90 minimum. num-integer supplies Integer/GCD and num-traits supplies the basic numeric traits. num-traits 0.2.19 was already present transitively in the inspected lock. These are primary crate-maintainer sources, inspected before choosing the APIs; the standard BigInt API supplies bit counts, parsing and integer operations. Big integer arithmetic/GCD is not reimplemented here.

Root's proposed first execution gate is:

cargo test --locked -p oa-core analysis_numeric::tests -- --test-threads=1
cargo clippy --locked -p oa-core --all-targets -- -D warnings

These commands have not run for this implementation. Root must add the dependencies and declare pub mod analysis_numeric first. A successful existing desktop suite while this module is undeclared provides no numeric validation. The independent correctness review is read-only and also does not execute these tests.

Public boundary

Type/API	Responsibility
Exact / ExactWire	Private normalized BigInt numerator and positive denominator; explicit canonical decimal-string wire. No unmetered Add/Div/Ord traits.
Exact::from_wire / parse_literal	Canonical wire admission or one exact source atom with explicit shared caller meter. No expression parser, names, unit resolver or evaluation context.
Exact arithmetic methods	Metered add/subtract/multiply/divide/compare/negate/abs/reciprocal/bounded integer power.
WorkLimits / WorkMeter / WorkUsage	One explicit request-local dynamic and numeric budget; read-only usage/limits; terminal first exhaustion. No Clone/Default on the meter.
Dimension	Validated seven-component integer vector, checked products/quotients/powers; dimension equality is not kind equality.
ResolvedKind	Resolver-supplied verified nominal key with dimension and optional distinct linear difference kind. No package lookup or compatibility cache.
Unit	Positive exact scale; affine offset or zero linear offset; exact canonical coordinate conversion.
NumericType / NumericValue	Internal Number, named linear/point, or anonymous dimension with R6 numerical operations. Boolean, list, property, call/check and AST semantics remain the common evaluator's responsibility.
NumericError / NumericLimit	Classified syntax/canonical/domain/type/dimension and magnitude/work-limit failures. Fuel exhaustion is detectably terminal; a component bit failure is not.

Public Eq on stored bounded values means representation equality; expression equality must call the metered compare operation, which rejects incompatible kinds. A false predicate is not represented by a numeric error. The integrating evaluator maps a valid comparison to Boolean and maps supported numeric failures into Failed/Unresolved. It must still distinguish those from Missing inputs and admission/type rejection.

K is the common resolver's verified same-origin contract key. This module neither derives K from dimensional equality nor mistakes a digest/name for compatibility. ResolvedKind comparison also checks dimension/algebra/difference key, so accidentally supplying the same key with different dimensions does not make two units convertible. The resolver still owns proof of the coherent coordinate basis. Exact definition references, package pins and declared-output anchoring remain model/report provenance outside this numerical value.

K must be a bounded handle with cheap Clone/Eq, such as an admitted internal identifier into a verified environment. A rooted contract graph must not be stored directly in K and recursively cloned/compared during arithmetic. Proof construction, archive reading and its work accounting belong to resolver admission. The generic Rust bounds cannot enforce that integration precondition. Numeric precharges cover the BigInt work, not arbitrary user-defined Clone/Eq implementations. NumericValue::from_unit checks terminal exhaustion before copying its key; display_in compares the existing key by reference.

Exact number and admission policy

Every admitted Exact has a nonzero positive denominator, gcd(n,d)=1, at most 4096 magnitude bits per component, and zero represented as 0/1. BigInts are private, so clients cannot mutate an admitted denominator or inject a wider coordinate. The bounded i64 constructor only creates an exact small integer; all nontrivial arithmetic is metered.

Wire fields are required strings. Leading plus/zeroes, negative zero, negative denominator, whitespace, exponents, decimal fractions, unreduced ratios and JSON numeric tokens reject. Numerator and denominator each enforce the digit limit, actual bit count and canonical grammar. An oversized but reducible wire pair still rejects; wire input is already required to be normalized. Duplicate and unknown fields reject through the closed Serde record.

Source admission reads only an unsigned decimal/integer or ratio(signed_integer, unsigned_integer) atom. It does not parse arithmetic, names or units. Whole source-atom bytes are capped at 2500; mantissa or ratio-component digits at 1234; decimal exponent magnitude at 128. Decimal mantissas require digits on both sides of a present dot. Source ratios/decimals may reduce, preserving distinctions such as accepted ratio(2,4) versus rejected unreduced wire. Ratio denominator zero rejects. No numeric input passes through f64.

Canonical nonnegative integer literals print as integers; other literals print ratio(n,d). A negative literal always prints ratio(-n,d), including d=1. A leading expression minus is not accepted by this literal reader and belongs to the future UnaryNegate AST. This preserves the R7 negative-literal distinction without constant-folding an expression. The complete copied R7 packet contains 10^300, 1/(2^4095), and -(2^4096-1) as full wire strings with full expected literal spellings.

Standalone Exact Serde conversion performs bounded canonical BigInt validation using a fresh per-literal admission meter, after the derived ExactWire decoder has allocated its String fields. It does not bound untrusted JSON string allocation or aggregate whole-document admission. A model/source/REST adapter must bound the encoded envelope and decoded strings, use a bounded visitor where needed, and cap aggregate admission work. The explicit metered entry points can accumulate literal parsing work after text admission. The evaluator must not deserialize repeatedly while interpreting dynamic calls or reset its meter per literal/target. No current Project/REST adapter is changed by this lease.

Bounded arithmetic and conversion

Each binary arithmetic method computes safe intermediate bit estimates and reserves its complete logical numeric charge before constructing cross products or running GCD. Two 4096-bit components multiply to at most 8192 bits; adding two such numerator terms can require 8193. Those bounded raw values normalize before applying the 4096-bit reduced result limit. Raw cancellation is therefore permitted: the tests include an 8193-bit sum numerator that reduces back to an admitted rational, and two approximately 8192-bit products that cancel to one.

Source decimal parsing bounds digit count/exponent before parsing or allocating a power of ten. It reserves parse, scale-construction, multiplication and normalization work using safe decimal-to-binary estimates; no arbitrarily long exponent can trigger an enormous BigInt. Canonical wire validation similarly reserves before BigInt parsing/GCD. The bit estimate uses ceil(3.322 * decimal_digits), an integer-only upper estimate, not a conversion through floating point.

Powers admit syntactic integer exponents -16..16. They use a fixed initial reservation, optional reciprocal, and left-to-right repeated multiplication, with each reduced stage bounded. They never allocate a 65536-bit power and discard it afterward. Division by zero/zero to a negative power fail; 0^0 is the explicit domain failure. A later rational expression that could mathematically cancel an earlier overflowing reduced stage does not erase that NumericLimit.

Unit coordinate conversion is deliberately the fixed path magnitude*scale then +offset; reverse conversion is coordinate-offset then /scale. Every reduced stage must fit the Exact bound. A wider intermediate that would cancel in a later conversion stage still fails. A fused conversion with different limit/work behavior would require an explicit revised profile. This is a practical bound at extreme magnitudes, not a rounding rule; ordinary supported conversions remain exact.

Linear units require positive scale and zero offset. An affine point kind has a distinct linear difference kind of the same dimension; the constructor derives that dimension from the validated linear difference kind and rejects point-as-difference or equal point/difference key. Tests use exact Celsius/Fahrenheit point coordinates and separate Kelvin interval units. Point-minus-point yields that interval kind, point plus/minus its interval yields the point, and interval+point is supported. Point+point, interval-point, point scaling/negation/abs/power reject. Comparison requires the same full type.

R6 numerical products/quotients yield anonymous dimensions when both operands are non-Number linear quantities, with A(0) immediately normalized to Number. Number scaling preserves the other linear type; Number/quantity yields an anonymous inverse. Anonymous add/subtract/compare requires equal dimensions. Named add/subtract/compare requires compatible nominal kinds. Explicit AsKind accepts only a matching anonymous dimension or Number for a named dimensionless kind, never a named-to-named coercion or affine target. The force-distance sum test requires one outer Energy assertion and expects 26 canonical joules.

C1 work contract and precise weights

The accounting profile is Q1-logical-work-1. Root approved implementing provisional reference ceilings of 1,000,000 dynamic events and 50,000,000 numeric work units. These constants still require measured bounded/worst-case calibration before a published stable profile. They are not wall-clock guarantees. Callers can lower either ceiling, including to zero, but cannot raise them through WorkLimits. The effective limits must travel in request/result/freeze identity; comparison of replay or caches requires identical limits as well as capture, context, targets and profile.

The one mutable meter is shared by all outputs and recursive evaluation. Dynamic events are explicit:

• Target before each requested output.
• Expression before every dynamically visited expression occurrence.
• CalculationEntry before every function body entry, additional to its Call expression.
• PropertyBinding before each selected effective property binding, additional to its Property expression.
• ListElement before each visited item, additional to that item's expression.

Charge only executed dynamic branches; statically checking both branches is a separate admission rule. The future evaluator must sort targets by category (properties, then checks) and UUID bytes, use the agreed operand/argument order, and preserve the same logical traversal/cost on cache hits. There is no implementation of an AST/cache here and no cache-parity execution claim. A shortcut that skips charges or uses a different effective budget is invalid; full report reuse must include the complete request identity.

Let W(b)=ceil(max(b,1)/64), using logical 64-bit words on every target platform. Numeric costs are fixed functions of bounded input/estimated intermediate sizes:

Primitive plan	Numeric work units
Product/division allowance P(a,b)	1 + W(a)*W(b)
Sum/comparison allowance S(a,b)	1 + W(max(a,b))
Normalization allowance G(n,d)	1 + 66*W(max(n,d))^2 (64 parts GCD, two parts quotient)
Digit parsing D(k,b)	1 + k*W(b)
Copy/sign/reciprocal C(n,d)	1 + W(n) + W(d)

These are conservative logical weights, not a claim about a crate's GCD complexity or algorithm. They remain independent of actual GCD iteration counts and internal multiplication optimizations. All cost inputs are bounded before these integer formulas; actual arithmetic cannot overflow their u64 computation.

For left component bits (a,b) and right (c,d), exact operation reservations are:

Method	Complete reservation before its BigInt work
add/subtract	P(a,d)+P(c,b)+S(a+d,c+b)+P(b,d)+G(max(a+d,c+b)+1,b+d)
multiply	P(a,c)+P(b,d)+G(a+c,b+d)
divide	P(a,d)+P(b,c)+G(a+d,b+c), then the zero-domain check
compare	P(a,d)+P(c,b)+S(a+d,c+b)
negate/abs/reciprocal	C(a,b), then the reciprocal zero-domain check where relevant
power	C(a,b), optional reciprocal charge, then the fixed sequence of bounded multiply charges
AsKind	C(a,b), after the type check
wire/ratio parsing	D(n_digits,n_est)+D(d_digits,d_est)+G(n_est,d_est)
decimal parsing	D(mantissa_digits,m_est) + (1+2*bit_length(abs(adjustment)))*P(scale_est,scale_est) + P(m_est,scale_est) + G(n_est,d_est)

Decimal adjustment is exponent minus fractional-digit count; scale_est estimates 10^abs(adjustment). These rules intentionally charge a fixed plan even when a sign/zero/identity shortcut could be faster. A one-word rational add costs exactly 75 numeric units; the boundary test independently checks that value.

The meter reserves atomically. A reservation that exceeds remaining fuel consumes no partial charge and latches its first WorkExhaustion (resource, prior usage, attempted charge, limit, operation/event). Further operations, even zero-cost reservations or unrelated target visits, return that same terminal failure without changing usage or traversing more children. The integrating evaluator must stop and label collected causes incomplete. It may not keep traversing siblings to make strict missing/failure cause lists exhaustive.

Component bit-limit errors are distinct nonterminal supported-operation failures: the prepaid bounded operation has finished and another independent output may still be evaluated with remaining fuel. Domain/type/admission classification remains the evaluator/adapter's responsibility.

Authored tests and evidence limits

The 26 test functions are authored in analysis_numeric/tests.rs. They currently cover:

Area	Independent expectations / negative controls
Basic exact arithmetic	400 small rational operand pairs checked against an independent i128 Euclidean-normalization oracle for add/subtract/multiply/divide/order; explicit zero divisors.
Decimal/power/sign domain	0.1+0.2=3/10, reduced source ratios, decimal exponents, positive/negative powers, abs/reciprocal, 0^0 and exponent rejection.
Strict wire/literal boundaries	Both numerator/denominator grammar, leading zero/plus/negative zero, unreduced/zero denominator, JSON numeric fields, duplicate/unknown/missing fields; source atom rejects expression minus/arithmetic.
R7	Exact full copied packets and expected canonical source/wire; negative literal remains signed ratio. This does not execute the future expression AST parser.
Magnitude/preallocation	8193-bit cancelling sum; wide cancelling products; numerator and denominator 4097-bit failures; zero numeric budget yields fuel exhaustion before a result allocation/bit check; forward/reverse affine stages reject 4097-bit intermediates despite a mathematically fitting final coordinate, with fitting conversion controls.
Meter	Exact 75-unit add boundary; zero-cost reservation; u64::MAX request without underflow; terminal first failure; effective limits serialize; shared target budget.
C1	A direct depth-30 call-tree workload stops after 10,000 entered calls; a depth-5 control permits exactly 63 calls and returns 496. This is a meter workload, not a second expression dialect or actual Studio evaluation.
Dimensions/kinds/units	Checked seven-axis limits; same-dimension different nominal kinds reject addition/comparison/conversion; same key/different dimension also rejects; exact duration and Celsius/Fahrenheit conversions.
R6	Anonymous compound energy sum/compare, product-then-quotient momentum, Number scaling/inverse, dimensionless normalization/explicit kind, affine point/interval rejection and power types.

Executed by this worker: the source fixture was copied byte-for-byte from the frozen independently reviewed R7 packet (SHA256 3B959DEC5E100A6F03817F5314BEF497347BA579EBD235476516D4BD83399181); standalone rustfmt succeeded. No test pass, compile pass, Clippy pass, benchmark or source/model/REST/GUI parity is claimed. Root's independent review and serialized execution are the next evidence.

The future vertical integration must add the actual expression traversal/meter propagation, type-check all operands including thresholds/unused branches, obey terminal cause incompleteness, record effective work limits, and test identical cold/warm/source/REST/frozen outcomes. The current R6 result-type helpers are internal to NumericValue; the AST checker should extract/reuse pure NumericType helpers, rather than evaluate dummy coordinates or duplicate the algebra. Number/Number has a valid result type even when a runtime denominator happens to be zero. Integration must also close encoded/decoded input and aggregate admission bounds, bounded resolver keys, nonempty pinned freeze and source AST round-trip. Approximate unit scales and ordinary engineering transcendental functions remain a mandatory subsequent capability; this exact module does not complete the release objective.

Frozen source inventory

Final standalone rustfmt --edition 2024 --check succeeded. A scoped text scan found zero trailing-whitespace lines and counted 26 test functions. The numeric module/dependencies remain absent from lib.rs and inspected manifests. This inventory describes local, uncommitted files awaiting root's integration and execution:

Workspace-relative file	SHA256
crates/oa-core/src/analysis_numeric.rs	6C88EEF3119162AEB6C07B9E75812C3AF9FBFE75554B0503AD00F103CB478408
crates/oa-core/src/analysis_numeric/dimension.rs	D4AD8E5307A1620E31791D724A0E31FDBA860D00DC83E3E1F2209D9C5E22A340
crates/oa-core/src/analysis_numeric/exact.rs	4EB8CB0F66B10E5DA204899AF82EE26ADFEC74BAB47B1A6C9842B5488EE04C4D
crates/oa-core/src/analysis_numeric/fixtures/r7-literal-boundaries.json	3B959DEC5E100A6F03817F5314BEF497347BA579EBD235476516D4BD83399181
crates/oa-core/src/analysis_numeric/meter.rs	1F7174BEB992935B4C399ACDEF91114AF73FAF041070FEAB968455AC827E8EE4
crates/oa-core/src/analysis_numeric/quantity.rs	EAD5142D6EEEA8F99399D57E02D8F7D819980923DE76387CD454694D6A747AEE
crates/oa-core/src/analysis_numeric/tests.rs	323CE82FC057D36F44463569FD8EA324C7D700FDDFBF32BCE15E04BD2A66970B

The SHA256 of the seven sorted path + TAB + uppercase hash + LF inventory lines, UTF-8 without BOM, is E4C2E20476FD21228F58741E8E537C01530B4C995DA47C5A714B407FD7086FD0. The report is excluded from that digest to avoid self-reference. Independent reviewer /root/semantics_critic reported no confirmed arithmetic/type/meter blocker in the read-only review; its final report and root's compiled tests remain separately owned evidence.