Samplinglib mathematical lesson

Fix the positive branch of the determinant square root

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_sqrt_det · theorem · Teaching coverage

Read this first

Mathematical statement

For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O, the nonnegative real square root of det(A_O) equals 2^(-n) det((sqrt(kappa)+1)I-(sqrt(kappa)-1)O). The determinant on the right is positive; it is not replaced by an assumed absolute-value identity.

\[\sqrt{\det A_O}=2^{-n}\det\bigl((\sqrt\kappa+1)I-(\sqrt\kappa-1)O\bigr)\]

Lean statement · singleBlockPrecision_sqrt_det

The source real precision is used literally; finite indices Fin n express the real n-dimensional matrix.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem singleBlockPrecision_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    Real.sqrt (singleBlockPrecision κ O).det = (1 / (2 : ℝ) ^ n) *
      (((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).det)

Exact module and namespace context

Proof roadmap

1Keep every matrix on the path nonsingular
Put a=sqrt(kappa)+1 and b=sqrt(kappa)-1. Then 0≤b<a. If (aI-tO)v=0 for 0≤t≤b, orthogonality gives a^2||v||_2^2=t^2||v||_2^2. Since a^2>t^2, v=0. This proves the determinant never vanishes.
2Continuity fixes the sign
At t=0 the determinant is a^n>0. The determinant is continuous on [0,b]. If its final value were nonpositive, the intermediate value theorem would give a zero on that interval, contradicting nonsingularity.
3Take the positive square root
Apply determinants to the already proved factorization. Multiplicativity and transpose invariance give det(A_O)=4^(-n)(det M)^2. The candidate 2^(-n)det M is positive and its square is exactly det(A_O), fixing the real square-root branch.

Full assumptions and notation

All objects and hypotheses

n is a natural number with n≥3, retaining the source standing block range.
kappa is real with kappa≥4.
O belongs to the full real orthogonal group O(n); determinant -1 and +1 are both included.
All square roots are the nonnegative real square root. No Haar law, probabilistic average or integrability premise is part of these pointwise identities.

Mathematical proof

1. Keep every matrix on the path nonsingular

Put a=sqrt(kappa)+1 and b=sqrt(kappa)-1. Then 0≤b<a. If (aI-tO)v=0 for 0≤t≤b, orthogonality gives a^2||v||_2^2=t^2||v||_2^2. Since a^2>t^2, v=0. This proves the determinant never vanishes.

\[(aI-tO)v=0\ \Longrightarrow\ (a^2-t^2)\|v\|_2^2=0\ \Longrightarrow\ v=0\]

Corresponding Lean step

The private shiftedOrthogonal_det_pos derives norm preservation directly from O^T O=I, uses the finite sum of coordinate squares, and applies Matrix.exists_mulVec_eq_zero_iff. No invertibility/sign bound is a public binder.

2. Continuity fixes the sign

At t=0 the determinant is a^n>0. The determinant is continuous on [0,b]. If its final value were nonpositive, the intermediate value theorem would give a zero on that interval, contradicting nonsingularity.

\[\det(aI)=a^n>0,\qquad \det(aI-tO)\ne0\ (0\le t\le b)\ \Longrightarrow\ \det M>0\]

Corresponding Lean step

Continuous.matrix_det and intermediate_value_Icc' supply the actual sign argument. The source uses a reverse-triangle norm bound for invertibility; Lean instead uses the equivalent squared-norm kernel contradiction. That quantitative norm bound is retained in the source graph and is not separately claimed as a new Lean estimate.

3. Take the positive square root

Apply determinants to the already proved factorization. Multiplicativity and transpose invariance give det(A_O)=4^(-n)(det M)^2. The candidate 2^(-n)det M is positive and its square is exactly det(A_O), fixing the real square-root branch.

\[\det A_O=4^{-n}(\det M)^2=\bigl(2^{-n}\det M\bigr)^2,\qquad 2^{-n}\det M>0\]

Corresponding Lean step

singleBlockPrecision_factorization is genuinely consumed. Matrix.det_smul, det_mul, det_transpose and Real.sqrt_eq_iff_mul_self_eq_of_pos finish the identity.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · singleBlockPrecision_sqrt_det

The adjacent checked Lean body supplies each actual algebraic and sign dependency internally.

Download module (.lean)

theorem singleBlockPrecision_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    Real.sqrt (singleBlockPrecision κ O).det = (1 / (2 : ℝ) ^ n) *
      (((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).det) := by
  have hs : 2 ≤ Real.sqrt κ := by
    nlinarith [Real.sq_sqrt (by linarith : 0 ≤ κ), Real.sqrt_nonneg κ]
  have hpos := shiftedOrthogonal_det_pos O
    (show 0 ≤ Real.sqrt κ - 1 by linarith)
    (show Real.sqrt κ - 1 < Real.sqrt κ + 1 by linarith)
  apply (Real.sqrt_eq_iff_mul_self_eq_of_pos (mul_pos (by positivity) hpos)).2
  rw [singleBlockPrecision_factorization hn hκ O, Matrix.det_smul,
    Matrix.det_mul, Matrix.det_transpose, Fintype.card_fin]
  have hquarter : (1 / 4 : ℝ) = (1 / 2) * (1 / 2) := by norm_num
  rw [hquarter, mul_pow, _root_.one_div_pow]
  ring

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise equations16-18 only. Haar probability and signed averaging, reflection/principal-minor cancellation and equation15, actual Gaussian laws/densities and Fubini, spherical Poisson identities, testing amplification, oracle indistinguishability, and both main lower bounds remain open.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Matrix.exists_mulVec_eq_zero_iff
dotProduct_self_eq_zero
Continuous.matrix_det
intermediate_value_Icc'
Matrix.det_smul
Matrix.det_mul
Matrix.det_transpose
Real.sqrt_eq_iff_mul_self_eq_of_pos

Mathematical sources

Determinant normalization identities — Only the pointwise part through equation18, including its sign argument.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.