Metadata
slug: sra2609-koteljanskii
bibkey: sra2026koteljanskii
doi: 10.48550/arXiv.2609.39979
url: https://arxiv.org/abs/2609.39979v1
triage: theorem
motivation_gids:
- D5/S3/Combinatorics/Permanental/SraReciprocalPermanentLorentzianRefutation.result
Sra’s reciprocal-permanent Lorentzian question
Problem
Suvrit Sra, A Koteljanskii inequality for permanents, arXiv:2609.39979v1, Section 4(d), asks:
Is Lorentzian for every inverse -matrix ?
Here, for ,
An inverse -matrix is entrywise nonnegative, invertible, and has inverse off-diagonal entries at most zero. The empty principal permanent is one. Lorentzian means the coefficient-topology closure of the recursively defined strict Lorentzian class of Brändén–Huh, Definition 2.1; it is not defined here by only a necessary Hessian test. The complete source expressions are in the source note and the Lorentzian note.
Statement echo
| Source clause | Formal counterpart | Fidelity |
|---|---|---|
| Every positive dimension, every real inverse -matrix | claim: , real Matrix (Fin n) (Fin n), InverseMMatrix | No symmetry or strict-entry-positivity assumption is added. |
| Principal-submatrix permutation permanent | PSW.principalPermanent, Matrix.permanent | The subtype supplies exactly the selected indices, including the empty case. |
| Displayed reciprocal polynomial | reciprocalPolynomial | none is and some i is source variable . |
| Brändén–Huh positive homogeneous class, strict recursion, closure | positiveHomogeneous, quadraticHessian, strictlyLorentzian, Lorentzian | All degree- coefficients are quantified; eigenvalue indices count multiplicity; finite-dimensional coefficientwise epsilon approximation expresses the closure. |
| Affirmative universal assertion is false | result | The theorem proves the literal negation of claim. |
Motivation
D5/S3/Combinatorics/Permanental/SraReciprocalPermanentLorentzianRefutation.result
refutes the assertion at dimension five. The public result is the designated
refutation result (basis=refutes) and is exempt from four-slot escape
registration (CLAUDE.md §3.9). It is the module’s only public theorem.
Gap
Preregistration #21688
quotes the published question, fixes the literal definitions and classifies
it as Tier 1. Its literature screen identifies no settlement in the searched
scope. The matrix is Sra’s published Theorem 1.2 witness; its ordinary
permanent-product failure is credited to that source. The distinct conclusion
here is the negative answer to the reciprocal-polynomial question.
Proof shape is bind-only; admission is open-problem-resolution (#21688; Refuted).
Route
The literal positive matrix is
The private theorems witness_positive and inverseM certify its hypotheses.
coefficient_table and witness_coeff compute the relevant coefficients.
The three derivatives in the last three coordinates have Hessian restriction
to with first pivot and
determinant (the exact values are computed below).
close_plane_positive proves that this restriction remains positive definite
when every degree-five coefficient changes by less than .
two_plane_excludes_unique contradicts the exactly-one-positive-eigenvalue
requirement reached after three steps of the strict Lorentzian recursion.
result applies this contradiction to a strict approximation supplied by
the literal closure definition.
Falsifier
The affirmative assertion would force the displayed matrix’s reciprocal
polynomial into that closure. Its fixed positive two-plane excludes every
sufficiently close strict approximation. The kernel-checked result is the
negation of the full assertion. Symmetric or symmetrizable reciprocal
polynomials are a separate, unresolved restriction here.
Evidence
The formal source is SraReciprocalPermanentLorentzianRefutation.lean; its canonical exposition is the corresponding Blueprint Scribe. Private theorem names below are qualified by that module’s namespace.
The rational experiment is
sra-koteljanskii at fc05f5ee612010d382cf8772f7bf43a1cb830aa1.
The checked script is docs/reports/sra-koteljanskii/check.py, SHA-256
bf8bef761479549a67a05ccf46ec6e0ebe90c9adf347d014cec66ea510a92a75.
Command: python3 /tmp/op-sra2609/check.py,
using the bytes read by git show from that immutable revision; exit 0,
ALL_CHECKS_OK. It checks the displayed matrices and the scopes stated in
Triage; it is computational evidence, separate from the Lean proof.
Triage
What the settlement shows
- Proved (kernel-checked):
resultrefutes the unchanged universal assertion at .witness_positiveandinverseMcertify the literal matrix’s strict entrywise positivity and inverse- property.coefficient_table,close_plane_positiveandtwo_plane_excludes_uniqueestablish the persistent positive two-plane obstruction to strict approximation. These are the mechanism of this refutation. - Computed: for this published , the four principal permanents are , with product ratio . The differentiated Hessian two-plane has first pivot and determinant . Evidence: the immutable experiment above, the stated command, exit 0 and SHA-256. No other dimension or matrix family is claimed to be enumerated.
- Open: Lorentzianity for symmetric or symmetrizable inverse -matrices is not settled. The positive-diagonal-scaling extension is not separately formalized. In the source, symmetric inverse -matrices satisfy ordinary permanent log-supermodularity, so the particular strict overlapping-product failure used here does not supply a symmetric counterexample.
- Proved (kernel-checked in the companion module):
SraSymmetricAlphaPermanentRefutation.resultrefutes Section 4(b). Its privatewitness_positive,inverseM,symmetric,differenceandinterval_failurecertify the displayed symmetric inverse -matrix and its failure for every . The difference is . The full companion statement and evidence are in its dossier. - Computed: for that fixed companion matrix, all subset pairs satisfy the inequality at each of and ; the selected difference at is . Evidence: the same immutable experiment, command, exit 0 and SHA-256. This is a finite check at two orders, not a classification of parameter ranges.
- Open: the remaining universal alpha parameter ranges and the source’s tree case are not newly classified or formalized. Literature reading: no proved theorem of the source relies on an affirmative answer to either open question; the refutations change those answers and the reported numerical evidence, while the source’s established theorems retain their stated hypotheses. The source’s distinguished orders and tree result are not on this module’s dependency path.
ASSUMED-UNVERIFIED
Literature completeness is ASSUMED-UNVERIFIED. The preregistration’s screen
covers the source v1, Brändén–Huh v8, arXiv metadata and selected full texts,
Semantic Scholar, Crossref, MathOverflow and MathDB. OpenAlex supplied no
citation list; the broad 200-result full-text query was not exhaustively
read, and web search supplied no reliable relevant hits. Semantic Scholar’s
zero indexed citations is an index reading, not proof of no prior solution.
No journal version was identified or read.