Normalizer: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Factor the actual precision as a positive square
Fix the positive branch of the determinant square root
Move the determinant sign inside the normalization factor

Samplinglib mathematical lesson

Factor the actual precision as a positive square

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

Read this first

Mathematical statement

For every natural n≥3, real kappa≥4 and real orthogonal n by n matrix O, put M=(sqrt(kappa)+1)I-(sqrt(kappa)-1)O. The literal precision A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T) equals (1/4) M^T M.

\[A_O=\tfrac14 M^\top M,\qquad M=(\sqrt\kappa+1)I-(\sqrt\kappa-1)O\]

Lean statement · singleBlockPrecision_factorization

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_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    singleBlockPrecision κ O = (1 / 4 : ℝ) •
      ((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
       ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)))

Exact module and namespace context

Proof roadmap

1Expand the orthogonal square
Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.
2Use the nonnegative square root
The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.

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. Expand the orthogonal square

Write s=sqrt(kappa). Orthogonality gives O^T O=I. Expand the two factors, keeping O and O^T distinct.

\[M^\top M=((s+1)^2+(s-1)^2)I-(s+1)(s-1)(O+O^\top)\]

Corresponding Lean step

Use mem_orthogonalGroup_iff', transpose linearity and distributivity of matrix multiplication.

2. Use the nonnegative square root

The standing kappa≥4 implies kappa≥0, so s^2=kappa. The diagonal and cross coefficients then give the exact source precision.

\[\tfrac14\bigl((s+1)^2+(s-1)^2\bigr)=\tfrac{\kappa+1}{2},\qquad \tfrac14(s+1)(s-1)=\tfrac{\kappa-1}{4}\]

Corresponding Lean step

After expanding matrix entries, ring normalization and Real.sq_sqrt prove the coefficients. The existing literal singleBlockPrecision is used unchanged.

Lean verification

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

Lean proof · singleBlockPrecision_factorization

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

Download module (.lean)

theorem singleBlockPrecision_factorization {n : ℕ} (_hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    singleBlockPrecision κ O = (1 / 4 : ℝ) •
      ((((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).transpose) *
       ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ))) := by
  have horth : (O : Matrix (Fin n) (Fin n) ℝ).transpose *
      (O : Matrix (Fin n) (Fin n) ℝ) = 1 :=
    (Matrix.mem_orthogonalGroup_iff' (Fin n) ℝ).mp O.property
  simp only [Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one,
    Matrix.sub_mul, Matrix.mul_sub, Matrix.smul_mul, Matrix.mul_smul,
    Matrix.one_mul, Matrix.mul_one, horth]
  ext i j
  simp only [singleBlockPrecision, Matrix.sub_apply, Matrix.add_apply,
    Matrix.smul_apply, smul_eq_mul]
  ring_nf
  rw [Real.sq_sqrt (by linarith : 0 ≤ κ)]
  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

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision

Mathlib API called (external library)

Matrix.mem_orthogonalGroup_iff'
Real.sq_sqrt
Matrix.transpose_sub
Matrix.mul_sub

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.

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.

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.

Samplinglib mathematical lesson

Move the determinant sign inside the normalization factor

AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_signed_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 of either determinant sign, det(O) sqrt(det(A_O)) equals 2^(-n) det((sqrt(kappa)+1)O-(sqrt(kappa)-1)I).

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

Lean statement · singleBlockPrecision_signed_sqrt_det

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

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Multiply by the transpose inside the determinant
The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.
2Transpose once more
A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.

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. Multiply by the transpose inside the determinant

The exact matrix identity O^T M=(sqrt(kappa)+1)O^T-(sqrt(kappa)-1)I follows from O^T O=I. Determinant multiplicativity and det(O^T)=det(O) bring the sign inside.

\[\det(O)\det M=\det\bigl((\sqrt\kappa+1)O^\top-(\sqrt\kappa-1)I\bigr)\]

Corresponding Lean step

hmatrix proves the matrix equality from orthogonality; hdet is its determinant image, using det_mul and det_transpose.

2. Transpose once more

A determinant equals that of its transpose. Combine the preceding identity with the actual square-root theorem, leaving O rather than O^T in the final formula. This works for both determinant components.

\[\det\bigl((\sqrt\kappa+1)O^\top-(\sqrt\kappa-1)I\bigr)=\det\bigl((\sqrt\kappa+1)O-(\sqrt\kappa-1)I\bigr)\]

Corresponding Lean step

The proof calls singleBlockPrecision_sqrt_det, not an assumed Gaussian normalization law or a sign-restricted orthogonal subgroup.

Lean verification

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

Lean proof · singleBlockPrecision_signed_sqrt_det

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

Download module (.lean)

theorem singleBlockPrecision_signed_sqrt_det {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    (O : Matrix (Fin n) (Fin n) ℝ).det * Real.sqrt (singleBlockPrecision κ O).det =
      (1 / (2 : ℝ) ^ n) *
      (((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).det) := by
  have horth : (O : Matrix (Fin n) (Fin n) ℝ).transpose *
      (O : Matrix (Fin n) (Fin n) ℝ) = 1 :=
    (Matrix.mem_orthogonalGroup_iff' (Fin n) ℝ).mp O.property
  have hmatrix : (O : Matrix (Fin n) (Fin n) ℝ).transpose *
      ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)) =
      ((Real.sqrt κ + 1) • (O : Matrix (Fin n) (Fin n) ℝ) -
        (Real.sqrt κ - 1) • (1 : Matrix (Fin n) (Fin n) ℝ)).transpose := by
    simp only [Matrix.mul_sub, Matrix.mul_smul, Matrix.mul_one, horth,
      Matrix.transpose_sub, Matrix.transpose_smul, Matrix.transpose_one]
  have hdet := congrArg Matrix.det hmatrix
  rw [Matrix.det_mul, Matrix.det_transpose, Matrix.det_transpose] at hdet
  rw [singleBlockPrecision_sqrt_det hn hκ O]
  calc
    _ = (1 / (2 : ℝ) ^ n) *
        ((O : Matrix (Fin n) (Fin n) ℝ).det *
          ((Real.sqrt κ + 1) • (1 : Matrix (Fin n) (Fin n) ℝ) -
            (Real.sqrt κ - 1) • (O : Matrix (Fin n) (Fin n) ℝ)).det) := by ring
    _ = _ := by rw [hdet]

end AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily

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.mem_orthogonalGroup_iff'
Matrix.det_mul
Matrix.det_transpose

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.