Correctness of exact-rational P3109 projection

The imported rational semantics prove the report's exact quantum, floor, parity, and selection formulas, with direction and error theorems for deterministic modes and selection correctness for every supplied stochastic word. This file proves that the result always fits the direct encoder's precision grid, then reuses the same saturation-and-encoding theorem as dyadic projection.

The logarithm bound imported here is a proof theorem about exact natural-number quotients; the P3109 runtime itself remains independent of binary-interchange representation and policy.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_fitsPrecisionGrid (format : Format) (mode : RoundingMode) (exact : ℚ) : format.FitsPrecisionGrid (format.roundFiniteRatToPrecision mode exact)

Exact-rational precision rounding always lands on the descriptor's direct-encoding grid.

The proof is uniform in width, precision, signedness, domain, rounding mode, and stochastic bit width. Every mode chooses one of the two adjacent integer candidates at the same exact quantum.

theorem FloatLib.Floats.Formats.P3109.Format.sameDatum_decode_projectRatCode (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : SameDatum (format.decode (format.projectRatCode policy value)) (format.projectRatValue policy value)

Decoding exact-rational projection returns its round-then-saturate datum.

The representation theorem is shared with dyadic projection; only the proof that rational rounding lands on the precision grid is new.

theorem FloatLib.Floats.ExecFloat.P3109.decode_projectRat {format : Formats.P3109.Format} (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.NumericalValue ℚ) : Formats.P3109.Format.SameDatum (projectRat policy value).decode (format.projectRatValue policy value)

Decoding projectRat exposes the exact P3109 rational round-then-saturate specification.