1. One semicircle per subdivision
Lay A and B end to end on a diameter. Erect a perpendicular at their junction: its intersection with the semicircle gives the height √(AB). Keep the half-interval containing θ.
REAL EXPONENTS · DIRECT ROOT ENCLOSURE
A root between two constructed lengths.
Bisect an interval of exponents. At each step, construct one geometric mean with a semicircle. Then retain the exact position of θ = 1/p through a weighted harmonic–arithmetic enclosure.
In exact geometry: L ≤ X^(1/p) ≤ U. Displayed decimals are floating-point approximations, not outward-rounded certified bounds.
Relative width · U/L − 1
Weight λ
Exponent interval [a, b]
2. Keep the exact weight
On an auxiliary segment, construct θ = 1/p by similar triangles, then λ = (θ − a)/(b − a). Between rails carrying A and B, a parallel at fraction λ reads U. The same construction on 1/A and 1/B, followed by inversion, reads L.
Construction and guarantee
A = Xᵃ, B = Xᵇ, b − a = 2⁻ⁿ, λ = (θ − a)/(b − a)
L = AB / ((1 − λ)B + λA)
L ≤ A1−λBλ = X1/p ≤ U = (1 − λ)A + λB
The upper bound follows from convexity of the exponential function. Apply that same bound to 1/A and 1/B, then invert positive quantities, to obtain the lower bound. Only products, quotients, weighted sums and square roots are needed to construct the two bounds.
A given real length p is allowed. This does not assert that every real p can itself be constructed from a unit segment. The √2 preset uses a numerical representation of that constructible length.
Precision, depth and construction cost
U/L − 1 = λ(1 − λ)(B − A)²/(AB)
U/L − 1 ≤ sinh²(ln X / 2ⁿ⁺¹)
The identity follows by multiplying the two weighted sums; λ(1 − λ) ≤ 1/4 gives the bound. For fixed X and relative precision, the sufficient depth is independent of p. Logarithms occur only in the analysis. The stopping rule compares the computed width with the tolerance directly.
The cost is n geometric means plus a fixed number of arithmetic constructions for θ, λ, L and U; this is not a count of individual strokes and arcs. Browser roundoff and physical drawing accuracy are separate from the exact mathematical guarantee. Automatic refinement uses tolerances of at least 10⁻¹² and stops at 24 subdivisions.
| Subdivisions | Maximum U/L − 1 |
|---|---|
| 8 | 1.84 × 10⁻⁶ |
| 12 | 7.16 × 10⁻⁹ |
| 16 | 2.80 × 10⁻¹¹ |
| 20 | 1.10 × 10⁻¹³ |
Relationship to the power chain and AD
The original chain already requires integer p because it repeats an operation p − 1 times. Binary exponentiation accelerates that chain; it does not introduce the integer restriction.
This construction directly encloses the root. It is a separate architecture from constructing sᵖ and applying AD. Combining AD with an enclosure of a fractional power would require an analysis of correction uncertainty before claiming the same convergence orders. The elementary ingredients here are classical; no claim of novelty or new Lean formalization is made.