A ceiling you can take apart.

The claim is conditional.

For the supplied readings, fixed tariff and equipment assumptions, no schedule in the model below saves more than the certified value. The certificate is an arithmetic proof of that statement. It does not establish that the readings, equipment specifications or quote are authentic, or that the model predicts a future year.

The comparison is useful only when a quote concerns the same recorded period and scope. Grid charging, VPP income, new solar, changed household demand, demand charges, subsidies, finance and backup value belong to different questions.

The invented example is generated deterministically. It is not a customer, a real installer quote or a measured performance claim.

One interval at a time.

For interval t, let E_t be baseline grid export and I_t baseline grid import, both in kWh. They are gross channels after direct solar self-consumption, recorded with no battery operating. Do not net them together: both may be positive within an interval.

The model chooses AC charge c_t, AC discharge d_t and stored energy s_t. Capacity is C; charging and discharging efficiencies are η_c and η_d. The interval lasts h_t hours.

0 ≤ c[t] ≤ cmax[t] = min(E[t], chargePower × h[t])
0 ≤ d[t] ≤ dmax[t] = min(I[t], dischargePower × h[t])
s[t+1] = s[t] + ηc × c[t] − d[t] / ηd
0 ≤ s[t] ≤ C

energy-bill saving J = Σ (buy[t] × d[t] − feed[t] × c[t])

Rates are dollars per kWh. Charging has an opportunity cost: it gives up the feed-in payment. Unchanged daily supply charges cancel. The bound permits any initial and final state in [0, C], including free initial energy. It does not force the battery to end empty.

The UI applies the entered round-trip efficiency r as η_c = r, η_d = 1. For a physical constant-efficiency model with η_cη_d = r, changing state to y = η_ds gives the same dynamics and capacity η_dC ≤ C. Using C in the transformed model therefore relaxes that capacity constraint. This reasoning needs a compatible usable-capacity basis and the same constant efficiency. A manufacturer’s headline round-trip rating is not proof of the efficiency in your household.

Aggregate readings hide the order of energy inside an interval. The model can charge and discharge in one interval and checks state at interval boundaries. Its schedules need not be physically executable with the actual subinterval timing. That enlarges the modeled opportunities; it is why we call the schedule a comparison policy, not a dispatch instruction.

There is no standby consumption, degradation or temperature model. With signed tariffs, adding an omitted effect need not only reduce savings. The claim remains about the stated model.

The certificate needs no optimizer.

Choose any sequence of rational prices p_t, in dollars per stored kWh. Write x⁺ = max(x, 0). Every model-feasible schedule obeys:

J ≤ U(p)

U(p) = Σ [cmax[t] × (ηc p[t] − feed[t])+
        + dmax[t] × (buy[t] − p[t]/ηd)+]
     + C × Σ(t=1..T−1) (p[t] − p[t−1])+
     + C × (p[0])+ + C × (−p[T−1])+

To see why, insert p_t times the state-conservation equation into each saving term. Charge and discharge contributions are bounded by their limits times the positive part of their coefficient. The remaining storage contribution telescopes:

Σ p[t] × (s[t] − s[t+1])
= p[0]s[0] − p[T−1]s[T]
  + Σ(t=1..T−1) (p[t] − p[t−1])s[t].

Each stored state lies between zero and C, which gives the last three terms in the bound. This argument holds for any supplied price sequence. An inaccurate optimizer can give a loose certificate; it cannot make a valid exact certificate overstate what it proves.

The browser proposes prices with a dynamic program over the distinct breakpoints 0, feed/η_c and buy×η_d. At most 64 price states are searched; larger sets are sampled and disclosed. The optimizer uses floating point. A separate checker recomputes the bound with BigInt rational arithmetic, validates every comparison-policy constraint and checks the stated upper value, policy value and gap.

The policy starts empty. It charges chronologically when a later rate could justify it, tracks acquisition lots, and discharges eligible lots in order. It has future-rate lookahead and is not offered as a deployable controller or an optimal solution. The gap between its value and the bound is model optimization uncertainty, not a confidence interval for real savings.

The positive-capacity interval relaxation can even pass energy through a zero-capacity store if both gross channels coexist. The capacity chart’s 0 kWh row instead means a physical no-battery baseline with saving zero. Every positive-capacity row uses the stated interval model.

Inputs that the first version accepts.

• CSV with start,durationMinutes,importKwh,exportKwh, optionally paired buyRate,feedInRate in dollars/kWh. Decimal inputs have at most nine fractional places. Readings must be ordered, nonnegative, contiguous and nonduplicated. Durations are 5, 15, 30 or 60 minutes.
• ISO timestamps with explicit offsets, or offset-free timestamps interpreted with a fixed clock explicitly chosen by the reader. Daylight-saving wall clocks without offsets are not guessed. Tariff windows and chart labels use the selected fixed clock.
• A strict NEM12 subset: one site, one household import E stream and one household export B stream, kWh, complete matching actual days, unchanged meter/configuration and no event flags. Estimated, substituted, incomplete, multiregister or ambiguous streams are refused. Both channels require explicit selection. The file’s identifiers stay out of the normalized report.
• A flat tariff, a daily peak window aligned with interval boundaries, or per-interval CSV rates. Rates must be constant throughout each meter interval. A tariff change inside an interval needs finer aligned meter readings. Neither a starting rate nor an energy-weighted average captures which part of the load a battery could serve; an average can produce an invalid physical comparison.
• Up to 110,000 intervals and a 30 MiB meter file. The independent report reader has a 120 MB file limit. Model values and rational denominators are bounded so malformed files cannot demand unbounded arithmetic.

These checks detect structural problems. A CSV cannot certify that its readings were actually measured; the reader must confirm their provenance. No missing interval is filled with zero and no partial year is annualized.

The field meanings follow AEMO’s metering data format documentation. NEM12’s import/export naming is from the grid’s viewpoint: E is energy delivered to the household, B is household export.

Run the check yourself.

Save a report from the calculator, then download the offline checker ZIP and extract it beside the report. It contains four JavaScript files and a README. Node.js 20 or later is sufficient; it needs no installed packages or network connection.

node check-report.mjs battery-report.json

Try the same command with the small invented example report. Its two intervals and exact ceiling of $0.40 are small enough to inspect by hand. The available initial energy can meet all imported demand, and no saving can exceed that imported energy’s $0.40 value.

Individual files: command-line checker, quote comparison, certificate checker, exact arithmetic. The optimizer is separately readable as engine.mjs, and the parser as importer.mjs.

The JSON report carries normalized meter rows, the full tariff, battery parameters, the policy’s charge/discharge/state arrays, the price witness, exact rational result claims, quote scope confirmations and code/data hashes. Code hashes identify the source files fetched at export time, not an attestation of modules already loaded in the browser. Hashes identify bytes; they are not signatures or evidence of authenticity. The checker verifies arithmetic and the conditional quote verdict, not arbitrary explanatory text or hashes.

Displayed ceilings round upward to cents. Displayed policy values round downward. Quote comparisons use exact fractions, so a quote a fraction of a cent over a ceiling can exceed it even when their displayed cents coincide. The dispatch CSV rounds to nine decimal places; the report preserves exact values.

Evidence, and the open edge.

The engine’s executable tests include hand-derived cases, independent exhaustive enumeration of small integer-state models, arbitrary dual witnesses and intentionally broken checker variants. Importer tests cover clock transitions, quality flags, missing channels, interval continuity and a full year of five-minute NEM12. Report tests alter quotes, scope flags and mathematical witnesses. The browser is tested through imports, stale inputs, comparisons and downloads.

Those tests establish mathematical and software behavior. They do not establish the accuracy of a forecast or demonstrate that a real installer’s quote is wrong. The release’s evidence record distinguishes generated inputs, openly published research traces and actual matched quote comparisons. Read the release evidence and remaining limits.

Existing tools already replay battery performance from meter data, including SolarQuotes and SunSPOT. This tool adds a narrow conditional quote test and a portable exact certificate; it makes no first-or-only claim.