← Session 18 — Lean tier (ii): finite-height proof + certified base points
Now update the 8 call sites in `marginTilde_convex` and refactor the `F` regularity to `ContDiffOn (Ioi 1)`. First the mapsTo helpers.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "theorem mapsTo_sqrt_shift :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)",
"new_string": "theorem mapsTo_sqrt_shift :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] \u221am + 1 maps (20, \u221e) into (1, \u221e) (the FAlt\ndomain). -/\ntheorem mapsTo_sqrt_shift_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] \u221am + 1 maps [20, \u221e) into (1, \u221e). -/\ntheorem mapsTo_sqrt_shift_Ici_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 \u2264 x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)"
}
raw content_json (database row)
[{"type":"text","text":"Now update the 8 call sites in `marginTilde_convex` and refactor the `F` regularity to `ContDiffOn (Ioi 1)`. First the mapsTo helpers."},{"type":"tool_use","id":"Edit_31","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"theorem mapsTo_sqrt_shift :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)","new_string":"theorem mapsTo_sqrt_shift :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] √m + 1 maps (20, ∞) into (1, ∞) (the FAlt\ndomain). -/\ntheorem mapsTo_sqrt_shift_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] √m + 1 maps [20, ∞) into (1, ∞). -/\ntheorem mapsTo_sqrt_shift_Ici_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 ≤ x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)"},"extra_content":null}]