Independent Research · Paper I
Nested Violation Sets for the Generalized Damascus Inequality
An elementary proof of the nestedness conjecture for the generalized Damascus inequality, with reproducibility checks and a Lean 4 formalization.
Abstract / research note
What this work establishes
Proves the three-variable nestedness conjecture and a stronger monotonicity result for positive violations, with exact computational checks and a Lean 4 formalization.
In plain English
What the paper is really doing
This paper asks a persistence question. If a particular triple of positive numbers breaks the Damascus inequality at one exponent, must that same triple still break it at the next exponent? The paper proves that the answer is yes in the three-variable setting.
The picture
For each exponent, collect every product-one triple that violates the inequality. Numerical plots suggested that these regions grow outward in an orderly sequence, with each region contained inside the next.
The conjecture
The open problem was to prove that the apparent nesting was real for every exponent—not merely something seen in experiments or a finite collection of plots.
The proof idea
A violating triple must have two coordinates above 1 and one below 1. A reciprocal symmetry then shows that, when the exponent increases, the two positive contributions strengthen more than the negative contribution.
Headline findings
The results worth carrying away
- Every three-variable violation at exponent n remains a violation at exponent n + 1.
- The result is stronger than simple containment: the numerical amount of violation increases strictly at the next exponent.
- The proof identifies the only sign pattern a violating triple can have—two coordinates above 1 and one below 1.
- It also localizes where violations can occur inside the product-one surface.
- The main argument is elementary and self-contained, with symbolic checks and a separate Lean 4 formalization supplied as independent audits.