ns_to_uj prices an attempt at wall time × a fixed ~15 W that no host
calibrated, and Propositional, Z3Smt, LeanVerifier and every Z3Server
attempt that is not sealed as a tree reading graded that figure
ModelBased. By the JCP ladder (SPEC §5.1) and the proof SPEC's own
definition a model earns ModelBased by its calibration; an assumed power
scaled by time is an estimate, so the figure claimed better provenance
than how it was obtained.
- proof-schema: Energy::estimator(uj), and Provenance docs that say a
default or assumed parameter makes a figure Estimator.
- proof-solvers: DEFAULT_ACTIVE_MILLIWATTS (15 W, same arithmetic) and
wall_time_estimate; all four sites now Energy::estimator. The public
Modelled / modelled_uj names are kept; their docs say estimate.
- Tests that pinned the over-claim now pin Estimator: grade_attempt's
unit tests, z3_tree.rs (server(), refuted goal, settle bound, cascade
total [Estimator, HwShunt] -> Estimator, undeclared z3), and proof-cli
tests/measure.rs (receipt "provenance Estimator", "stay Estimator").
New test: every wall-time rung (T0 proved/refused, one-shot z3, an
absent Lean) is Estimator with no measurement.
- proof-cli, proof-cascade, proof SPEC §5 / README, and joule-code-remediate
(FormalOutcome docs, joule_fix's printed label) say Estimator.
proof/conformance/v1 is unchanged: gen-vectors output is byte-identical
(it seals the stand-in ladder's estimate_tier figures, never ns_to_uj).
Co-Authored-By: Claude Opus 5.5 <[email protected]>
e42c3d1c07