REAL_SOSFIELD (positive denominators)

Recommended implementation order: 5th of 10.

Context

Harrison's REAL_SOSFIELD clears denominators in goals involving /. We can do the positive-denominator case (which only adds inequality side conditions) without depending on the equality machinery in #21.

Size & files

~150–250 LOC. SOS/Reify.lean, SOS/Tactic.lean.

Approach

Lean on Mathlib.Tactic.FieldSimp rather than implementing a custom Expr walker (which would have to handle nested divisions, sign flips on < vs ≤, side-condition discharge — easy to get wrong).

Design

New tactic sos_field that:

1. Runs field_simp (with positivity hypotheses as side conditions) to clear denominators.
2. Routes the cleared polynomial inequality through sos.
3. Falls back with a clear error if field_simp leaves residual divisions ("denominator b could not be proven non-zero / positive — add it as a hypothesis").

Do not add Raw.div to SOS/Raw.lean — Raw stays a true polynomial ring.

Verification

• example (x : ℝ) (hx : 0 < x) : 0 ≤ 1/x + x - 2 := by sos_field
• example (a b : ℝ) (h : 0 < b) : 0 ≤ a^2 / b := by sos_field

Risks

field_simp may rewrite into shapes the reifier doesn't re-recognise. Add a norm_num / ring_nf post-pass to normalise.

Start by reading SOS/Reify.lean and SOS/Tactic.lean, then run the two verification examples in the issue to understand the expected tactic behavior. Done means a new sos_field tactic handles positive denominators through field_simp and sos, reports unresolved denominators clearly, and accounts for the normalization risk noted in the issue.