The literal full precision, including its residual identity block
AutoSamplingTheory.ExampleCases.GaussianComplexity.DeterminantFamily.blockPrecision · def · Teaching coverage
Mathematical statement
Within the standing range kappa≥4 and 3≤n≤d, put k=floor(d/n). For every tuple of k real orthogonal n by n matrices, define the d by d precision as diag(A_O1,...,A_Ok,I_(d-kn)), where A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O^T).
Lean statement · blockPrecision
Coordinates are Fin d with the exact quotient/remainder adapter; dotProduct represents the Euclidean quadratic form.
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.
noncomputable def blockPrecision {d n : ℕ} (κ : ℝ)
(O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin d) (Fin d) ℝProof roadmap
- 1Use consecutive coordinates
Mathlib indexes equal blocks by (inner coordinate, block). Swap these indices before flattening, so the original coordinate is inner+n*block. The residual coordinate starts at k*n.
- 2Retain the residual identity
Euclidean division gives d=k*n+r with r=d mod n=d-k*n. Reindex the literal block diagonal to Fin d. When r=0, Fin0 is empty and no residual coordinate is introduced.
Full assumptions and notation
All objects and hypotheses
- d and n are natural dimensions; kappa is a real number.
- n≥3, n≤d and kappa≥4 are the source standing range.
- O is a tuple indexed by Fin(d/n), with each matrix in the full real orthogonal group on Fin n.
- The literal algebraic definition extends to every natural d,n and real kappa; spectral and minimizer theorems retain the source range.
Construction and meaning
1. Use consecutive coordinates
Mathlib indexes equal blocks by (inner coordinate, block). Swap these indices before flattening, so the original coordinate is inner+n*block. The residual coordinate starts at k*n.
Corresponding Lean step
The private blockCoordinates uses prodComm, finProdFinEquiv, sumCongr, finSumFinEquiv and finCongr.
2. Retain the residual identity
Euclidean division gives d=k*n+r with r=d mod n=d-k*n. Reindex the literal block diagonal to Fin d. When r=0, Fin0 is empty and no residual coordinate is introduced.
Corresponding Lean step
blockPrecision applies Matrix.reindex to fromBlocks (blockDiagonal ...) 0 0 1; no padding or fallback replaces the residual block.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · blockPrecision
The adjacent checked Lean body supplies the actual matrix assembly and all internal dependencies.
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.
noncomputable def blockPrecision {d n : ℕ} (κ : ℝ)
(O : Fin (d / n) → Matrix.orthogonalGroup (Fin n) ℝ) : Matrix (Fin d) (Fin d) ℝ :=
Matrix.reindex (blockCoordinates d n) (blockCoordinates d n)
(Matrix.fromBlocks (Matrix.blockDiagonal (fun j => singleBlockPrecision κ (O j)))
0 0 (1 : Matrix (Fin (d % n)) (Fin (d % n)) ℝ))Source assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| n>=3,n<=d,kappa>=4; k=floor(d/n); residual d-k*n. | The theorem retains n>=3,n<=d,kappa>=4; Fin(d/n) blocks and Fin(d%n) residual, with contiguous coordinate equivalence. | same | Euclidean division identifies d%n with d-k*n. Real Hermitianity and universal dot-product bounds express source symmetry and Loewner bounds; no Pi norm or entrywise matrix order is used. |
| The source introduces the formula in its standing range. | The same literal block expression is defined for all natural d,n and real kappa. | generalization | This is an algebraic carrier extension with no invented off-source fallback. It asserts no spectral or minimizer conclusion outside the standing range. |
Only determinant-family regularity and the quadratic minimum in Lemma3.4/B.8. Gaussian normalization, Haar posterior laws, oracle indistinguishability, test separation and both main complexity lower bounds remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The definition explicitly extends the same algebraic formula beyond the source standing range; its theorems retain that range. — This extension is explicitly disclosed in candidate assumptions and has exactly the same restriction to the source domain; n=0 gives I_d and is outside the claimed regularity range.
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
- Only determinant-family regularity and the quadratic minimum in Lemma3.4/B.8. Gaussian normalization, Haar posterior laws, oracle indistinguishability, test separation and both main complexity lower bounds remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Matrix.blockDiagonal
- Matrix.fromBlocks
- Matrix.reindex
- finProdFinEquiv
- finSumFinEquiv
- Nat.div_add_mod
Mathematical sources
- Source block family and full regularity lemma — Literal equation(5), block quadratic bounds and unique minimum only.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.