Fix the positive branch of the determinant square root
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_sqrt_det · theorem · Teaching coverage
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.
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.
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)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.
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.
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.
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.
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.
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]
ringSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| n>=3,kappa>=4 and an arbitrary real orthogonal O; the positive determinant branch is proved in the source. | Exactly these binders; positivity, invertibility and all estimates are derived inside the proof. | same | No convenience premise or restriction to SO(n) is introduced. The continuous path is represented on the same real interval; its nonsingularity uses squared norms rather than a separately stated reverse-triangle lower bound. |
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.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: The pointwise content is made explicit; no expectation theorem is being certified and no almost-everywhere exception is introduced. — A2.SS2.p1, Eq15, A2.SS2.SSS1.p2 versus module introduction, actual binders and lesson scope.
- scopes: A disclosed proof-route change establishes the required positive determinant conclusion without separately formalizing the quantitative source norm estimate. No semantic weakening of Eq17 or Eq18 results. — The source proves ||(aI−tO)v||≥(a−t)||v||≥2||v|| on 0≤t≤sqrt(κ)−1, then uses invertibility and continuity. Lean proves the same required nonsingularity by a squared-coordinate-norm kernel contradiction and continuity. This is a valid alternate route to the sign conclusion; the quantitative norm inequality itself is not a separately formalized theorem in the supplied module. The English lesson explicitly discloses this distinction. Its claim that the estimate is retained elsewhere in the source graph is outside these permitted review inputs and is not independently certified here. I checked the full packet module, including private shiftedOrthogonal_det_pos: from 0≤b<a and t∈[0,b], a>0 and a²−t²>0. Orthogonality gives (Ov)·(Ov)=v·v. A zero determinant yields a nonzero kernel vector, av=tOv, and hence (a²−t²)(v·v)=0, contradicting v·v>0. The continuous determinant path starts at det(aI)=a^n>0; an endpoint ≤0 would cross zero by IVT. Thus its endpoint is positive for every orthogonal O, without any determinant-component restriction. Instantiating a=sqrt(κ)+1,b=sqrt(κ)−1 uses κ≥4 to obtain sqrt(κ)≥2; these are derived facts, not additional source binders.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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.singleBlockPrecisionAutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.singleBlockPrecision_factorization
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.