Positive parameters give a nonempty actual row set

Proved

OAI.PiExponent.DeterminantContradiction.actualRowCount_ge_one_of_pos

by Eyal1990 · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryopenai-pi-exponent-017

For any fixed admissible data and any positive real parameter H, the actual row count is at least one.

Preamble

import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_AnalyticAggregate_RemainderData

open scoped BigOperators Topology
open Filter
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction
open OAI.PiExponent.LiteralAnalytic

Formal statement

theorem OAI.PiExponent.DeterminantContradiction.actualRowCount_ge_one_of_pos {nu : ℝ} (d : FixedData nu) (H : ℝ) (hH : 0 < H) : 1 ≤ actualRowCount d H := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/LiteralAnalyticSummand.lean#L177-L199

View graph