Block-scaled representation capability

Block-scaled codes store one scale shared by several significands. This proof-only capability relates that concrete decomposition to a system's finite block denotation while leaving the index, scale, stored significand, lane value, and scaling operation fully generic.

def FloatLib.Numerics.BlockScaled (system : NumericalSystem) (Index : Type u) (Scale : Type v) (Stored : Type w) (Lane : Type x) (laneAt : system.Scalar → Index → Lane) (scaleOf : system.Code → Scale) (storedAt : system.Code → Index → Stored) (applyScale : Scale → Stored → Lane) : Prop

A numerical system's finite denotation is lane-wise reconstruction from one shared scale.

All executable projections are explicit parameters. The proposition certifies them but does not force numerical kernels to access a typeclass dictionary in their inner loops.