Realized as WeightedCarving R P in the Mathlib-free core (Aggregation), carried at whatever numbers the task uses: WeightedCarving.mean is the ratio of the weighted fold to the weight fold, and needs the carrier's * and / beside the + every mode needs. What cannot live there is the mode's law — see below.

WeightedCarving.mk? is a dif on the carrier's own equality test, and mk?_eq_none_iff says it refuses exactly the carvings whose total is the carrier's zero. Uses weighted carvings.

What the test rejects is what the carrier calls zero, and that is where the ladder starts mattering. At Float the license is satisfied by NaN: an all-NaN carving is accepted and its mean of a constant is NaN, refuting at that carrier the law proved below. Nothing is wrong with the field; what is absent is a carrier law to spend it on, which is why the executable rungs state their own gate rather than inherit this one.

A constant factors out of the fold (fold_mul_const, by induction), and the license discharges the cancellation. Cancellation is a field law, which is why this statement is in the PhysLib-backed AggregationLaws over \mathbb{R} while the mode it is about is in the core: the structure travels down to every carrier and the law stops at the lawful ones.

That the weights are load-bearing is checked separately: a carving weighted 1 and 3 over values 3 and 1 has mean 3/2 where the unweighted average of the same values is 2, so a mean ignoring its weights would fail the probe.

A mean is the first aggregation mode that is not a fold — it multiplies, sums, and finally divides — so it is exactly the shape the adequacy layer's forward-error theorem (dag_fp32_error_bound) was built for. MeanBound compiles a carving into that layer's Expr (weights and values as exact binary32 constants, the folds as add nodes, the ratio as the one div node) and reads the bound off it. Every rounding the mean incurs is a node of the budget, and the quotient rule's magnitude factors are what a small total weight costs.

The load-bearing detail is that the license does not cross the bridge. WeightedCarving's field says the total is not the carrier's zero, which at binary32 is a statement about the rounded fold; the theorem also needs one about the exact fold, and neither implies the other. Both directions are ordinary floating-point behavior and both are exhibited: weights 2^{24}, 1, -2^{24} sum exactly to 1 while their binary32 fold is exactly +0, because the first addition absorbs the 1; and weights 2^{24}, 1, 1, -(2^{24}+2) sum exactly to 0 while their binary32 fold is exactly -2, because two absorbed 1s leave the running total short. So forgetting a binary32 carving to the real carving it specifies takes the specification's license as an argument, and the signature is where that is recorded.

By induction on the carving: identity rounding makes the bridge law an additive homomorphism, so the fold commutes with the forgetting. Stated in the core, over an arbitrary refinement, since nothing about binary32 enters.

This is the strongest of the two remedies and the one to reach for first, because it removes the question rather than answering it. It is available exactly when the weights are counts or indicators — a validity mask, a sample tally, a pixel count — which is the ordinary shape of a masked average: fold the denominator where addition is exact and convert to the numerator's carrier once, rather than accumulating it in the same floating-point type as the numerator.

Both counterexamples are built from cancellation, so nonnegativity is exactly what excludes them. The floating-point content is one lemma — a grid point does not shrink when a nonnegative is added to it and the sum is rounded, which is monotonicity of rounding together with rounding fixing the grid. Absorption may return the grid point unchanged; it cannot return anything smaller. Induction then gives both halves: a positive exact total forces a positive rounded one, and a zero exact total forces a zero rounded one.

Grid membership is a real hypothesis, not bookkeeping: the rounding-spec format is a bare record over \mathbb{R} with representability a separate predicate, so "this is a binary32 number" has to be said, and without it a weight below half the smallest subnormal would round away and the argument would fail at the leaf it starts from.

This covers the weights metrology actually uses — masses, areas, durations, coverage fractions, validity indicators — but it is the second-best fix. Where the weights are counts, the theorem above applies and no floating-point reasoning is needed at all.

Two inductions over the carving, one per fold, each with the same shape: a leaf is the erasure by definition, and a join is Carrier.add on both sides once the operands have been rewritten. Realized in the Mathlib-free core (Aggregation.lean), depending on propext alone.

The theorem is what makes the kinded layer honest about its cost. Nothing is recomputed and no numerical claim is restated: the three obligations above are discharged once at construction, and everything proved downstream about magnitudes continues to hold.

Immediate from the quotient bridge, and that is the point: until the mean acquired kinds, the bridge had no consumer that was not a test of itself. A weighted mean is the first model-level construct in the library that divides across a licensed kind change, so it is the first place the law does work.

What the theorem does not say is that the whole mean commutes with the forgetful map. The folds above the division round at every join, and pushing the forgetful map through them is exactly what the exact-carrier hypothesis supplies. The division is one step of that argument, stated where it holds with no side condition. Instantiated at the binary32 rung on an indicator-weighted carving whose license is discharged rather than assumed.