Exact semantics of arbitrary-width square-root prefixes #
The direct square-root kernel scales a positive dyadic by an even power of two, computes its
integer square root, and jams whether the exact root continues beyond that integer prefix.
This module proves the representation-independent integer facts. Posit-specific square-root
refinement is kept in Direct.Proof.
Dyadic exponent parity is always zero or one.
Casting the executable parity recovers the Euclidean exponent remainder.
The source exponent splits into the generated root scale and its two restored half-scales.
The scaled integer radicand and two copies of the restored root scale denote the source dyadic.
Scaling preserves positivity of a nonzero source significand.
The truncated root is positive for every nonzero source significand.
The truncated root's square is the lower endpoint of the exact root cell.
The scaled radicand lies strictly below the square of the next integer root.
The exact square remainder vanishes exactly for an integral scaled root.
Generating precision fractional root bits puts the truncated root's leading bit at or above
that position.
Exact rational continuation at the scale represented by a generated root prefix.
Instances For
The executable prefix rounds exactly like any proper rational continuation in the same integer root cell.
Only exactness versus a nonzero continuation is observable after sticky-bit jamming. This theorem lets the square-root refinement proof choose convenient rational lower and upper witnesses around the mathematical root.