From 354d0e707c413500f40eabd9bdc3bc737fd2b054 Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Sun, 9 Aug 2026 05:46:55 -0400 Subject: [PATCH 1/2] Release v0.7.0 --- .agents/PLAN.md | 26 +- .agents/SPEC.md | 22 +- .agents/audit/dependency-dag.md | 135 +- .agents/audit/fidelity.md | 67 +- .agents/inventory/carlet-chapter10.yaml | 1411 +++++++++++++++++ AGENTS.md | 13 +- CryptBoolean.lean | 1 + .../OddDimensionBestNonlinearity.lean | 28 +- .../Chapter04/OddWeightingNonlinearity.lean | 4 +- CryptBoolean/Carlet/Chapter10.lean | 26 + .../Carlet/Chapter10/AlgebraicImmunity.lean | 960 +++++++++++ .../Carlet/Chapter10/ElementarySymmetric.lean | 400 +++++ CryptBoolean/Carlet/Chapter10/Krawtchouk.lean | 316 ++++ CryptBoolean/Carlet/Chapter10/LowDegree.lean | 483 ++++++ .../Carlet/Chapter10/Nonlinearity.lean | 1164 ++++++++++++++ CryptBoolean/Carlet/Chapter10/Normality.lean | 495 ++++++ .../Carlet/Chapter10/NumericalDegree.lean | 592 +++++++ .../Carlet/Chapter10/Periodicity.lean | 190 +++ .../Carlet/Chapter10/PrimeDegree.lean | 423 +++++ .../Carlet/Chapter10/Propagation.lean | 449 ++++++ .../Carlet/Chapter10/RotationSymmetric.lean | 481 ++++++ CryptBoolean/Carlet/Chapter10/Symmetric.lean | 217 +++ README.md | 6 +- .../CryptBooleanBlueprint/Blueprint.lean | 15 +- .../Carlet/Chapter10.lean | 36 + .../Carlet/Chapter10/AlgebraicImmunity.lean | 36 + .../Carlet/Chapter10/Fourier.lean | 38 + .../Carlet/Chapter10/Nonlinearity.lean | 155 ++ .../Carlet/Chapter10/Representation.lean | 148 ++ .../Carlet/Chapter10/Resiliency.lean | 61 + .../Carlet/Chapter10/RotationMatriochka.lean | 68 + .../CryptBooleanBlueprint/Site.lean | 37 + .../scripts/check_statement_style.py | 4 +- blueprint-verso/scripts/validate_manifest.py | 10 +- lakefile.lean | 2 +- 35 files changed, 8475 insertions(+), 44 deletions(-) create mode 100644 .agents/inventory/carlet-chapter10.yaml create mode 100644 CryptBoolean/Carlet/Chapter10.lean create mode 100644 CryptBoolean/Carlet/Chapter10/AlgebraicImmunity.lean create mode 100644 CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Krawtchouk.lean create mode 100644 CryptBoolean/Carlet/Chapter10/LowDegree.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Nonlinearity.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Normality.lean create mode 100644 CryptBoolean/Carlet/Chapter10/NumericalDegree.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Periodicity.lean create mode 100644 CryptBoolean/Carlet/Chapter10/PrimeDegree.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Propagation.lean create mode 100644 CryptBoolean/Carlet/Chapter10/RotationSymmetric.lean create mode 100644 CryptBoolean/Carlet/Chapter10/Symmetric.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/AlgebraicImmunity.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Fourier.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Nonlinearity.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Representation.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Resiliency.lean create mode 100644 blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/RotationMatriochka.lean diff --git a/.agents/PLAN.md b/.agents/PLAN.md index 1c84b24..75dfaa4 100644 --- a/.agents/PLAN.md +++ b/.agents/PLAN.md @@ -8,8 +8,8 @@ Plancherel, relative Hamming distance, balancedness, restrictions, ANF, algebrai functions, and derivatives needed by CryptBoolean. FABL is the canonical owner of those shared APIs; this project imports them directly and adds only source-facing or cross-representation laws. -The current Blueprint baseline contains 294 source-facing statement nodes: 291 formalized nodes -associated with 1882 proved Lean declarations and 3 visibly open nodes, connected by 713 reviewed +The current Blueprint baseline contains 317 source-facing statement nodes: 314 formalized nodes +associated with 2158 proved Lean declarations and 3 visibly open nodes, connected by 772 reviewed dependency edges. Chapter 2 contributes 41 formalized nodes, 174 declarations, and 56 incoming edges. Chapter 3 contributes 7 formalized nodes, 32 declarations, and 19 incoming edges. Chapter 4 contributes 73 formalized nodes, 568 declarations, and 159 incoming edges. Chapter @@ -17,7 +17,8 @@ edges. Chapter 4 contributes 73 formalized nodes, 568 declarations, and 159 inco 6 contributes 70 formalized nodes, 441 declarations, and 189 incoming edges. Chapter 7 contributes 39 formalized nodes, 224 declarations, and 114 incoming edges. Chapter 8 contributes 14 formalized nodes, 131 declarations, and 42 incoming edges. Chapter 9 contributes 19 formalized nodes, 109 -declarations, and 64 incoming edges. These counts are a synchronized verification contract shared +declarations, and 64 incoming edges. Chapter 10 contributes 23 formalized nodes, +276 declarations, and 59 incoming edges. These counts are a synchronized verification contract shared by the inventories, Verso sources, `blueprint-verso/scripts/validate_manifest.py`, and `AGENTS.md`. @@ -80,13 +81,14 @@ tooling pipeline runs, and no local filesystem path appears in package metadata. ## Phase 1 - Complete Carlet inventory -Status: in progress. Chapters 2--9 are source-reviewed and Blueprint-synchronized under +Status: complete. Chapters 2--10 are source-reviewed and Blueprint-synchronized under `.agents/inventory/`. Chapter 6 has 70 promoted mathematical statements and 18 additional source-recovery records; Chapter 7 has 39 promoted mathematical statements and 10 additional source-recovery records; Chapter 8 has 14 promoted mathematical statements and 5 additional source-recovery records; Chapter 9 has 19 promoted mathematical statements and 10 additional +source-recovery records; Chapter 10 has 23 promoted mathematical statements and 9 additional source-recovery records. These recovery records preserve cited or underspecified families that are -not promoted to Blueprint nodes. Chapter 10 is not yet inventoried. +not promoted to Blueprint nodes. Read Chapters 2--10 in full and create one Blueprint node per in-scope item. Record full statements, source locations, representation decisions, and mathematical dependencies. Mark referenced results @@ -305,12 +307,24 @@ source-recovery records rather than theorem evidence. ## Phase 10 - Chapter 10 symmetric functions +Status: complete. All 23 reviewed source statements are formalized by 276 associated declarations +with 59 reviewed dependency edges. + - symmetric-function representation and elementary-symmetric ANF; - Walsh transform and nonlinearity; - resiliency and algebraic immunity; - rotation-symmetric and Matriochka-symmetric superclasses. -This phase reuses the general criteria and does not redefine them for symmetric functions. +The completed layer reuses the Chapter 2 numerical and algebraic normal forms, FABL Krawtchouk +polynomials, Chapter 5 restriction/normality bounds, Chapter 6 bent and direct-sum theorems, +Chapter 7 resiliency bounds, Chapter 8 propagation rigidity, and Chapter 9 majority immunity. It +also contains a checked fast-Walsh certificate for the nine-variable rotation-symmetric function +of nonlinearity 241. + +The odd-dimensional optimal-nonlinearity classification and its two window consequences are closed +through the complete-quadratic normal form and complementary-pair restrictions. The +odd-dimensional optimal-immunity uniqueness theorem is closed by constructing low-degree symmetric +annihilators and inductively forcing the two half-threshold weight profiles. ## Phase 11 - Carlet closure diff --git a/.agents/SPEC.md b/.agents/SPEC.md index aceac83..cb8a539 100644 --- a/.agents/SPEC.md +++ b/.agents/SPEC.md @@ -32,8 +32,8 @@ PDFs, manifests, graphs, and caches are not sources of truth. ## Current verified baseline -The reviewed Blueprint contains 294 source-facing statements, of which 291 are associated with -1882 proved Lean declarations and 3 remain visibly open, connected by 713 mathematical dependency +The reviewed Blueprint contains 317 source-facing statements, of which 314 are associated with +2158 proved Lean declarations and 3 remain visibly open, connected by 772 mathematical dependency edges. Chapter 2 contributes 41 formalized statements, 174 declarations, and 56 incoming edges. Chapter 3 contributes 7 formalized statements, 32 declarations, and 19 incoming edges. Chapter 4 contributes 73 formalized statements, 568 declarations, and 159 incoming edges. @@ -41,7 +41,8 @@ Chapter 5 contributes 31 statements (28 formalized and 3 open), 203 declarations edges. Chapter 6 contributes 70 formalized statements, 441 declarations, and 189 incoming edges. Chapter 7 contributes 39 formalized statements, 224 declarations, and 114 incoming edges. Chapter 8 contributes 14 formalized statements, 131 declarations, and 42 incoming edges. Chapter 9 -contributes 19 formalized statements, 109 declarations, and 64 incoming edges. +contributes 19 formalized statements, 109 declarations, and 64 incoming edges. Chapter 10 +contributes 23 formalized statements, 276 declarations, and 59 incoming edges. The completed Chapter 2 frontier includes Proposition 5's numerical-normal-form integrality criterion, the full raw Poisson formula, affine invariance, restriction recovery, the @@ -100,6 +101,15 @@ cover algebraic-immunity consequences for weight, normality, and nonlinearity, h bounds, optimal majority and threshold families, the trace-power cyclic-run estimate, and the Carlet--Feng construction with its degree and nonlinearity bounds. +The Chapter 10 inventory is source-reviewed and Blueprint-synchronized. Its 23 formalized nodes +cover symmetric weight profiles, Relations (71)--(73), elementary-symmetric numerical and +algebraic normal forms, binomial interpolation, power-of-two periodicity, Krawtchouk/Walsh +formulas, even and odd normality, Theorems 16 and 17, numerical-degree and prime bounds, rotation +symmetry, the explicit nine-variable nonlinearity-241 witness and its bent extensions, and +Matriochka symmetry. The odd-dimensional optimal symmetric-nonlinearity classification, its two +high-nonlinearity window consequences, and the optimal-algebraic-immunity uniqueness theorem are +also complete. + Chapter 2 has no open node: the finite-field coordinate theorem identifies ANF degree with the maximum binary weight in the univariate support, cyclotomic-orbit noncancellation closes Carlet Proposition 3, and the trace-pairing coordinate theorem is compiled. Chapter 3 likewise has no open node: the @@ -123,6 +133,12 @@ dimension ranges, all three odd quotient-coordinate forms, the inclusive order-c endpoints, cyclic rather than linear binary runs, the corrected `n>=2` Carlet--Feng domain, and the survey's exact real nonlinearity inequality. +Chapter 10's fidelity record uses a finite truncated periodicity condition, restores +“nonconstant” in the Relation (73) conjectural sequel, claims cyclic invariance only for the +explicit nine-variable seed, and separates the seed's proved Walsh certificate from empirical +optimality searches. The classification endpoints retain the source hypotheses and exact integer +thresholds. + Source-facing splits remain explicit in Chapter 4. Rodier's one-sided lower endpoint and sharp interval have distinct nodes, as do the finite Hamming-ball and Plotkin lemmas and the resulting higher-order asymptotic estimate. The Reed--Muller coset-distance theorem diff --git a/.agents/audit/dependency-dag.md b/.agents/audit/dependency-dag.md index 27f1193..9cca3d5 100644 --- a/.agents/audit/dependency-dag.md +++ b/.agents/audit/dependency-dag.md @@ -20,7 +20,8 @@ spine. The current baseline is: | Carlet Chapter 7 | 39 | 39 | 0 | 224 | 114 | | Carlet Chapter 8 | 14 | 14 | 0 | 131 | 42 | | Carlet Chapter 9 | 19 | 19 | 0 | 109 | 64 | -| **Total** | **294** | **291** | **3** | **1882** | **713** | +| Carlet Chapter 10 | 23 | 23 | 0 | 276 | 59 | +| **Total** | **317** | **314** | **3** | **2158** | **772** | An item marked `[open]` has a complete mathematical statement but no Lean association. In the tables below, `consumer <- prerequisite-1, prerequisite-2` denotes one incoming edge from each @@ -1182,10 +1183,131 @@ carlet-9-carlet-feng-nonlinearity carlet-2-trace-pairing-coordinates ``` +## Chapter 10 reviewed dependency DAG + +Chapter 10 contributes 23 promoted statements, all with proved associations. The following is the +complete reviewed 59-edge graph. + +### Symmetric representations and transforms + +```text +carlet-10-def-symmetric + <- carlet-2-def-boolean-function, carlet-2-def-support-weight +carlet-10-rel-71-nnf + <- carlet-10-def-symmetric, carlet-2-nnf-existence-uniqueness, + carlet-2-prop-4-nnf-mobius +carlet-10-univariate-binomial-representation + <- carlet-10-rel-71-nnf +carlet-10-rel-72-anf + <- carlet-10-rel-71-nnf, carlet-2-anf-existence-uniqueness +carlet-10-low-degree-classification + <- carlet-10-rel-72-anf, carlet-2-def-algebraic-degree, + carlet-2-def-affine-functions, carlet-6-rel-56-complete-quadratic +carlet-10-power-two-periodicity + <- carlet-10-rel-72-anf, carlet-2-def-algebraic-degree +carlet-10-krawtchouk-fourier-walsh + <- carlet-10-def-symmetric, carlet-2-pseudoboolean-fourier, + carlet-2-def-walsh-transform +``` + +### Normality, propagation, and nonlinearity + +```text +carlet-10-even-middle-layer-normality + <- carlet-10-def-symmetric, carlet-5-def-4-normality +carlet-10-theorem-16 + <- carlet-10-def-symmetric, carlet-10-low-degree-classification, + carlet-4-def-propagation-criteria +carlet-10-even-bent-symmetric-classification + <- carlet-10-theorem-16, carlet-6-def-7-bent, + carlet-6-rel-56-complete-quadratic +carlet-10-odd-weak-normality-bound + <- carlet-10-def-symmetric, carlet-5-def-4-normality, + carlet-5-affine-flat-restriction-bound +carlet-10-theorem-17 + <- carlet-10-def-symmetric, carlet-5-rel-42-restriction-nonlinearity, + carlet-4-def-nonlinearity +carlet-10-odd-optimal-nonlinearity-classification + <- carlet-10-theorem-17, carlet-10-low-degree-classification, + carlet-6-rel-56-complete-quadratic +carlet-10-high-nonlinearity-quadratic-window + <- carlet-10-theorem-17, carlet-10-even-bent-symmetric-classification, + carlet-10-odd-optimal-nonlinearity-classification, + carlet-10-low-degree-classification +carlet-10-high-nonlinearity-quadratic-or-odd-window + <- carlet-10-theorem-17, carlet-10-even-bent-symmetric-classification, + carlet-10-odd-optimal-nonlinearity-classification, + carlet-2-def-support-weight +``` + +### Numerical degree, resiliency, and algebraic immunity + +```text +carlet-10-numerical-degree-half-bound + <- carlet-10-univariate-binomial-representation +carlet-10-rel-73 + <- carlet-10-univariate-binomial-representation +carlet-10-prime-successor-full-numerical-degree + <- carlet-10-def-symmetric, carlet-10-rel-73, + carlet-7-prop-32-nnf-characterization +carlet-10-largest-prime-numerical-degree-bound + <- carlet-10-def-symmetric, carlet-10-rel-73, + carlet-7-prop-32-nnf-characterization +carlet-10-odd-optimal-ai-uniqueness + <- carlet-10-def-symmetric, carlet-9-majority-parameters, + carlet-4-def-annihilator-algebraic-immunity +``` + +### Rotation and Matriochka symmetry + +```text +carlet-10-def-rotation-symmetric + <- carlet-10-def-symmetric +carlet-10-rotation-symmetric-above-quadratic + <- carlet-10-def-rotation-symmetric, + carlet-4-odd-dimension-quadratic-covering-bounds, + carlet-6-direct-sum, carlet-6-rel-56-complete-quadratic +carlet-10-def-matriochka-symmetric + <- carlet-10-def-symmetric +``` + +Only the explicit nine-variable seed in the rotation-symmetric existence statement is asserted to +be invariant under the full cyclic coordinate action. Its direct sums with complete quadratic bent +blocks retain the exact nonlinearity formulas but need not be rotation symmetric on all coordinates. +The seven generic fast-Walsh certificate declarations associated with this statement are reusable +finite-Walsh verification infrastructure whose direct source-facing use is the certified seed; they +do not create an additional Blueprint statement. + +### Chapter 10 source-recovery boundary + +Nine reviewed inventory records remain outside the promoted 23-node graph and contribute neither +manifest nodes nor dependency edges: + +- `carlet-10-symmetric-filter-implementation` lacks an LFSR state, correlation statistic, and + circuit or runtime cost model; +- `carlet-10-additional-propagation-nonlinearity-families` and + `carlet-10-additional-resiliency-families` require theorem-complete statements from the cited + primary sources; +- `carlet-10-numerical-degree-conjecture` is explicitly conjectural, and + `carlet-10-numerical-degree-finite-checks` lacks dimension ranges, extremizing profiles, and + independently checkable certificates; +- `carlet-10-even-optimal-ai-families` omits the dimension ranges, profiles, and equivalence-class + data needed for a classification; +- `carlet-10-rotation-bent-correlation-families` lacks exact parameterized theorems, while + `carlet-10-rotation-dihedral-finite-searches` lacks the functions and exhaustive-search + certificates needed for its claimed optima; and +- `carlet-10-matriochka-complexity-and-parameters` combines an unspecified cost comparison with an + explicitly open cryptographic-parameter program. + +The numerical-degree conjecture's Relation (73) reformulation is deliberately corrected from the +printed “no binary solution” to “no nonconstant binary solution”: constant weight profiles are +immediate solutions. This conjectural specialization uses the nonnegative degree bound `d=n-4` +and is therefore stated only from dimension four onward. + ## Remaining proof frontier -Three source statements remain open, all in the analytic Chapter 5 character-sum branch. Their complete -statements remain visible without placeholder associations: +Three source statements remain open, all in the Chapter 5 analytic character-sum branch. Their +complete statements remain visible without placeholder associations: - `carlet-5-theorem-7-weil-bound` and `carlet-5-weil-nonlinearity-bound` require the analytic additive-character Weil estimate. The trace-pairing coordinate identification and the @@ -1196,7 +1318,8 @@ statements remain visible without placeholder associations: Four further Chapter 5 citation-recovery records are intentionally outside the 31-node graph until their primary-source parameters support complete statements; they do not affect the manifest -counts or edges. +counts or edges. The nine Chapter 10 recovery records listed above likewise remain outside the +23-node graph. Proposition 12 is closed: Chapter 3's affine-flat and equality-case slice layer proves the exact source classification. Chapter 4 is closed: Rodier's interval, the exact dimension-seven maximum, @@ -1208,7 +1331,9 @@ reviewed frontier. Chapter 6 is closed: all 70 nodes have proved associations, w source-recovery records remain outside the graph until their cited statements or certificates can be recovered faithfully. Chapter 7 is closed: all 39 nodes have proved associations, while its ten source-recovery records preserve citation-only or underspecified construction and counting -families. +families. Chapters 8 and 9 are closed with 14 and 19 formalized nodes. Chapter 10 is closed with all +23 nodes formalized; its nine recovery records preserve incomplete, conjectural, empirical, or +operational source claims without changing the graph. ## Machine verification diff --git a/.agents/audit/fidelity.md b/.agents/audit/fidelity.md index cbc480b..ae9393c 100644 --- a/.agents/audit/fidelity.md +++ b/.agents/audit/fidelity.md @@ -25,10 +25,11 @@ The generated manifest currently verifies the following baseline: | Carlet Chapter 7 | 39 | 39 | 0 | 224 | 114 | | Carlet Chapter 8 | 14 | 14 | 0 | 131 | 42 | | Carlet Chapter 9 | 19 | 19 | 0 | 109 | 64 | -| **Total** | **294** | **291** | **3** | **1882** | **713** | +| Carlet Chapter 10 | 23 | 23 | 0 | 276 | 59 | +| **Total** | **317** | **314** | **3** | **2158** | **772** | The manifest count is an association count, not a claim that every printed result in Carlet -Chapters 2--9 is complete. Coverage outside the reviewed nodes remains governed by the +Chapters 2--10 is complete. Coverage outside the reviewed nodes remains governed by the inventories under `.agents/inventory/`. ## Corrected source mappings @@ -115,6 +116,19 @@ inventories under `.agents/inventory/`. | `carlet-9-trace-power-run-bound` | Carlet p. 134 and reference [282] bound the algebraic immunity of a trace monomial by the cyclic one-run count of its exponent. | The formal run count joins the first and last binary digits, is invariant under cyclotomic rotation, and retains the printed floor and ceiling placements. The multiplier construction is proved through an explicit cyclic full-adder and then transported to a nonzero finite-field trace product. | | `carlet-9-theorem-15` | Carlet pp. 139--140 gives the Carlet--Feng support construction and optimal algebraic immunity. | The domain is corrected to `n>=2`, the range of the cited primary theorem. At `n=1`, the survey's printed positive-integer domain makes the support endpoint and Relation (70) invalid. | | `carlet-9-carlet-feng-nonlinearity` | Carlet p. 140 prints `nl(f) >= 2^(n-1)-n ln(2) 2^(n/2)-1`; the cited primary theorem gives a stronger logarithmic expression. | The associated theorem proves the survey inequality over the reals by a multiplicative-character Fourier expansion, exact nontrivial Gauss-sum magnitude, a cyclic interval estimate, Jordan's sine inequality, and a finite harmonic-log bound. The stronger primary formula remains a fidelity note rather than replacing the source-facing statement. | +| `carlet-10-def-symmetric` | Carlet pp. 140--141 defines symmetry by coordinate-permutation invariance and identifies symmetric functions with functions of Hamming weight. | The associated declarations prove permutation invariance, equality on weight layers, and existence and uniqueness of the finite profile `f^#:{0,...,n}->F_2` as equivalent formulations. No infinite profile is introduced. | +| `carlet-10-univariate-binomial-representation` | Carlet pp. 141--142 represents the weight profile by its binomial-basis polynomial and identifies its degree with numerical degree. | The real polynomial, the rational polynomial with integral Relation (71) coefficients, their coefficientwise scalar-extension identity, exact evaluation, exact degree, and interpolation uniqueness are all associated. `booleanRealEmbedding_apply_eq_val` supplies the pointwise binary-to-real cast used to compare the two representations. | +| `carlet-10-power-two-periodicity` | Carlet p. 142 states that algebraic degree at most `2^t-1` is equivalent to period `2^t` of the symmetric weight profile. | A finite `n`-variable profile has no values beyond weight `n`. The formal equivalence therefore quantifies exactly over pairs `r,r+2^t` that both lie in `0,...,n`; it does not manufacture an infinite extension of the profile. | +| `carlet-10-krawtchouk-fourier-walsh` | Carlet p. 143 gives the generating-polynomial, signed binomial, layer-transform, and symmetric Walsh formulas. | The associated FABL coefficient and negative-coordinate generating-polynomial theorems are composed with local exact layer and signed-profile theorems. The final declaration states the literal signed Krawtchouk sum for the raw Walsh transform; the zero-frequency correction remains an intermediate equivalent form. | +| `carlet-10-rel-73` | Carlet Relation (73), p. 145 gives the alternating binomial equations characterizing a numerical-degree bound. | `relation_73_functionNumericalDegree_le_iff_int` is associated as the literal integer theorem for every `d- + The 23 source-facing items below retain the theorem-complete mathematics + from Carlet pages 140--147: the symmetric weight profile, Relations + (71)--(73), the Krawtchouk transform, normality and nonlinearity results, + Theorems 16 and 17, resiliency bounds, the odd-dimensional optimal- + immunity classification, and the rotation-symmetric and Matriochka + superclasses. Nine additional records preserve qualitative implementation + claims, citation-only result families, the open numerical-degree + conjecture, finite searches without certificates, and underspecified even- + dimensional immunity families. The finite weight profile replaces the + source's informal infinite periodic sequence by its exact truncated + periodicity condition. Empirical searches are not promoted as theorem + evidence, and the repeated optimal-immunity theorem for majority is reused + from Chapter 9 rather than duplicated. +items: + - id: carlet-10-def-symmetric + kind: definition + location: >- + Symmetric Boolean functions (Carlet, Chapter 10 introduction, + pp. 140--141) + statement: |- + Let n be a nonnegative integer and let f:V_n -> F_2. The following are + equivalent: + + 1. f is invariant under every permutation of its n input coordinates; + 2. f(x)=f(y) whenever w_H(x)=w_H(y); + 3. there is a unique function f^#:{0,...,n}->F_2 such that + + f(x)=f^#(w_H(x)) + + for every x in V_n. + + A function satisfying these conditions is symmetric, and f^# is its + weight profile. + formal_status: formalized + declarations: + - CryptBoolean.IsSymmetricBooleanFunction + - CryptBoolean.positiveCoordinateCount_binaryCubeSignEquiv + - CryptBoolean.negativeCoordinateCount_binaryCubeSignEquiv + - CryptBoolean.supportCardIndex + - CryptBoolean.supportCardIndex_val + - CryptBoolean.canonicalWeightInput + - CryptBoolean.canonicalWeightInput_support_card + - CryptBoolean.supportCardIndex_canonicalWeightInput + - CryptBoolean.symmetricWeightProfile + - CryptBoolean.isSymmetricBooleanFunction_iff_eq_of_support_card_eq + - CryptBoolean.IsSymmetricBooleanFunction.eq_of_support_card_eq + - CryptBoolean.IsSymmetricBooleanFunction.eq_profile + - CryptBoolean.isSymmetricBooleanFunction_iff_eq_profile + - CryptBoolean.isSymmetricBooleanFunction_iff_existsUnique_weightProfile + - CryptBoolean.symmetricWeightProfileNat + - CryptBoolean.symmetricRealWeightProfile + - CryptBoolean.symmetricWeightProfileNat_supportCardIndex + - CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_profile + fidelity_note: >- + Carlet defines symmetry by invariance under the symmetric group and + immediately gives the equivalent Hamming-weight representation. The + uniqueness of the profile is implicit because every weight from zero + through n occurs in V_n. + reuse_note: >- + Reuse FABL's coordinate-permutation predicate and its characterization + by equal positive-coordinate counts, transported through the binary/ + sign-cube equivalence. Reuse the canonical Hamming-weight theorem rather + than introducing a second coordinate-count definition. + dependencies: + - carlet-2-def-boolean-function + - carlet-2-def-support-weight + + - id: carlet-10-rel-71-nnf + kind: theorem + location: Relation (71) (Carlet, Section 10.1, p. 141) + statement: |- + For 0<=r<=n, let phi_r:V_n->F_2 be the indicator of the vectors of + Hamming weight r. The coefficient of the monomial x_I in the numerical + normal form of phi_r is zero when r>|I| and otherwise is + + (-1)^(|I|-r) binom(|I|,r). + + For 0<=i<=n, define the i-th elementary symmetric pseudo-Boolean + function + + S_i(x)=sum_(I subseteq {1,...,n}, |I|=i) product_(j in I) x_j. + + If f is symmetric with weight profile f^#, identify F_2 with {0,1} in + the integers and set + + c_i=sum_(r=0)^i f^#(r)(-1)^(i-r) binom(i,r). + + Then the numerical normal form of f is + + f(x)=sum_(i=0)^n c_i S_i(x), + + and its numerical degree is max{i | c_i != 0}, with value zero for the + zero function. + formal_status: formalized + declarations: + - CryptBoolean.weightLayerIndicator + - CryptBoolean.weightLayerIndicator_apply_self + - CryptBoolean.isSymmetricBooleanFunction_weightLayerIndicator + - CryptBoolean.IsSymmetricBooleanFunction.sum_weightLayerIndicator + - CryptBoolean.symmetricWeightProfileNat_weightLayerIndicator + - CryptBoolean.symmetricRealWeightProfile_weightLayerIndicator + - CryptBoolean.elementarySymmetricNumericalCoefficients + - CryptBoolean.elementarySymmetricNumerical + - CryptBoolean.symmetricNumericalExpansion + - CryptBoolean.elementarySymmetricNumerical_apply + - CryptBoolean.numericalEval_cardCoefficients_eq_symmetricNumericalExpansion + - CryptBoolean.symmetricNumericalCoefficient + - CryptBoolean.numericalCoeff_eq_symmetricNumericalCoefficient + - CryptBoolean.numericalCoeff_booleanRealEmbedding_weightLayerIndicator + - CryptBoolean.symmetricNumericalExpansion_symmetricNumericalCoefficient_eq + - CryptBoolean.relation_71_symmetricNumericalExpansion + fidelity_note: >- + The printed coefficient sum runs from r=0 to n. Writing it through i is + the identical total form under the standard convention binom(i,r)=0 + for r>i and avoids a negative natural exponent in (-1)^(i-r). The + coefficients and equality live in the integer-valued numerical normal + form, not in the algebraic normal form over F_2. + reuse_note: >- + Reuse the Chapter 2 numerical normal form, its Mobius coefficient + formula, support cardinality, and the existing elementary finite sums. + The new layer is the symmetry reduction from all subsets to their + cardinalities. + dependencies: + - carlet-10-def-symmetric + - carlet-2-nnf-existence-uniqueness + - carlet-2-prop-4-nnf-mobius + + - id: carlet-10-univariate-binomial-representation + kind: theorem + location: >- + Univariate representation following Relation (71) (Carlet, + Section 10.1, pp. 141--142) + statement: |- + Let f:V_n->F_2 be symmetric, let f^# be its weight profile, and let + c_0,...,c_n be the coefficients in Relation (71). For an indeterminate + z, put + + binom(z,i)=z(z-1)...(z-i+1)/i!, binom(z,0)=1, + + and + + P_f(z)=sum_(i=0)^n c_i binom(z,i). + + Then P_f(r)=f^#(r) for every integer 0<=r<=n. It is the unique rational + polynomial of degree at most n with those n+1 prescribed values, and + + deg(P_f)=deg_NNF(f). + + Moreover S_i(x)=binom(w_H(x),i), so the multivariate numerical normal + form of f is obtained by substituting z=w_H(x) in P_f. + formal_status: formalized + declarations: + - CryptBoolean.functionNumericalDegree_le_dimension + - CryptBoolean.binomialBasisPolynomial + - CryptBoolean.binomialBasisPolynomialRat + - CryptBoolean.map_binomialBasisPolynomialRat + - CryptBoolean.eval_binomialBasisPolynomial_nat + - CryptBoolean.natDegree_binomialBasisPolynomial + - CryptBoolean.eval_binomialBasisPolynomialRat_nat + - CryptBoolean.natDegree_binomialBasisPolynomialRat + - CryptBoolean.symmetricProfilePolynomial + - CryptBoolean.symmetricProfilePolynomialRat + - CryptBoolean.map_symmetricProfilePolynomialRat + - CryptBoolean.booleanRealEmbedding_eq_zero_iff + - CryptBoolean.booleanRealEmbedding_eq_one_iff + - CryptBoolean.booleanRealEmbedding_apply_eq_val + - CryptBoolean.eval_symmetricProfilePolynomial + - CryptBoolean.eval_symmetricProfilePolynomialRat + - CryptBoolean.natDegree_symmetricProfilePolynomial_le + - CryptBoolean.natDegree_symmetricProfilePolynomial_eq + - CryptBoolean.natDegree_symmetricProfilePolynomialRat_eq + - CryptBoolean.eq_symmetricProfilePolynomial_of_natDegree_le_of_eval_eq + - CryptBoolean.eq_symmetricProfilePolynomialRat_of_natDegree_le_of_eval_eq + fidelity_note: >- + The source writes the binomial-basis and falling-factorial forms of the + same polynomial. Its degree is Carlet's numerical degree and is kept + distinct from algebraic degree over F_2. + reuse_note: >- + Reuse Relation (71), Mathlib's descending Pochhammer and polynomial + interpolation uniqueness, and the existing numerical-degree API. + dependencies: + - carlet-10-rel-71-nnf + + - id: carlet-10-rel-72-anf + kind: theorem + location: Relation (72) (Carlet, Section 10.1, p. 142) + statement: |- + For 0<=i<=n define the i-th elementary symmetric Boolean function + + sigma_i(x)=sum_(I subseteq {1,...,n}, |I|=i) + product_(j in I) x_j in F_2. + + Then + + sigma_i(x)=binom(w_H(x),i) mod 2. + + Write j preceq i when every one-bit of j is also a one-bit of i. If f + is symmetric with weight profile f^#, then its algebraic normal form is + + f(x)=sum_(i=0)^n lambda_i sigma_i(x), + + where + + lambda_i=sum_(j preceq i) f^#(j) in F_2. + + Conversely, + + f^#(i)=sum_(j preceq i) lambda_j in F_2. + + Thus the two transforms are inverse, and the algebraic degree of f is + max{i | lambda_i=1}, with value zero for the zero function. + formal_status: formalized + declarations: + - CryptBoolean.elementarySymmetricANFCoefficients + - CryptBoolean.elementarySymmetricBoolean + - CryptBoolean.symmetricANFExpansion + - CryptBoolean.elementarySymmetricBoolean_apply + - CryptBoolean.isSymmetricBooleanFunction_elementarySymmetricBoolean + - CryptBoolean.anfCoeff_elementarySymmetricBoolean + - CryptBoolean.anfEval_cardCoefficients_eq_symmetricANFExpansion + - CryptBoolean.symmetricANFCoefficient + - CryptBoolean.anfCoeff_eq_symmetricANFCoefficient + - CryptBoolean.symmetricANFExpansion_symmetricANFCoefficient_eq + - CryptBoolean.relation_72_symmetricANFExpansion + - CryptBoolean.functionAlgebraicDegree_le_iff_symmetricANFCoefficient + - CryptBoolean.BitCovers + - CryptBoolean.natCast_choose_eq_one_iff_bitCovers + - CryptBoolean.symmetricANFCoefficient_involution + references: [255] + fidelity_note: >- + The bit-cover order and both directions of the involutive Mobius + transform are explicit. Lucas' theorem supplies the parity of the + binomial coefficient; it is mathematical infrastructure rather than a + competing Boolean-function representation. + reuse_note: >- + Reuse the canonical Chapter 2 ANF coefficients and algebraic degree. + Mathlib's Lucas theorem or its binary specialization should discharge + the binomial-parity step. + dependencies: + - carlet-10-rel-71-nnf + - carlet-2-anf-existence-uniqueness + + - id: carlet-10-low-degree-classification + kind: classification + location: >- + Linear and quadratic symmetric functions (Carlet, Section 10.1, + p. 142) + statement: |- + Let p_n(x)=x_1+...+x_n and + + q_n(x)=sum_(1<=i0, a symmetric f:V_n->F_2 has algebraic degree exactly one if and + only if + + f=p_n+b + + for some b in F_2. Equivalently, + + f^#(r+1)=f^#(r)+1 + + for every 0<=r=2, f has algebraic degree exactly two if and only if + + f=q_n+a p_n+b + + for some a,b in F_2. Equivalently, + + f^#(r)=binom(r,2)+a r+b mod 2 + + for 0<=r<=n, or equivalently + + f^#(r+2)=f^#(r)+1 + + for every 0<=r<=n-2. + formal_status: formalized + declarations: + - CryptBoolean.symmetricAffineNormalForm + - CryptBoolean.symmetricQuadraticNormalForm + - CryptBoolean.isSymmetricBooleanFunction_symmetricAffineNormalForm + - CryptBoolean.isSymmetricBooleanFunction_symmetricQuadraticNormalForm + - CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm + - CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm + - CryptBoolean.elementarySymmetricBoolean_zero + - CryptBoolean.elementarySymmetricBoolean_one_eq_coordinateSum + - CryptBoolean.elementarySymmetricBoolean_two_eq_completeQuadraticBit + - CryptBoolean.anfCoeff_smul + - CryptBoolean.anfCoeff_symmetricAffineNormalForm + - CryptBoolean.anfCoeff_symmetricQuadraticNormalForm + - CryptBoolean.symmetricAffineNormalForm_eq_coordinateSum_add_constant + - CryptBoolean.symmetricQuadraticNormalForm_eq_completeQuadratic_add_coordinateSum + - CryptBoolean.exists_symmetricAffineNormalForm_of_degree_le_one + - CryptBoolean.functionAlgebraicDegree_eq_one_iff_exists_symmetricAffineNormalForm + - CryptBoolean.exists_symmetricQuadraticLayerNormalForm_of_degree_le_two + - CryptBoolean.functionAlgebraicDegree_eq_two_iff_exists_symmetricQuadraticNormalForm + - CryptBoolean.symmetricWeightProfileNat_symmetricAffineNormalForm_succ + - CryptBoolean.symmetricWeightProfileNat_symmetricQuadraticNormalForm_add_two + - CryptBoolean.exists_symmetricAffineNormalForm_of_profile_succ + - CryptBoolean.exists_symmetricQuadraticNormalForm_of_profile_add_two + - CryptBoolean.functionAlgebraicDegree_eq_one_iff_profile_succ + - CryptBoolean.functionAlgebraicDegree_eq_two_iff_profile_add_two + fidelity_note: >- + The positive-arity and n>=2 domains make the printed exact-degree + classifications nonvacuous. In particular, the two-step recurrence is + not used as an exact-degree criterion when its quantified range is + empty. + reuse_note: >- + Reuse Relation (72), the canonical algebraic-degree and affine-function + APIs, and the complete quadratic function already formalized with + Relation (56). + dependencies: + - carlet-10-rel-72-anf + - carlet-2-def-algebraic-degree + - carlet-2-def-affine-functions + - carlet-6-rel-56-complete-quadratic + + - id: carlet-10-power-two-periodicity + kind: theorem + location: >- + Degree and profile periodicity (Carlet, Section 10.1, p. 142) + statement: |- + Let f:V_n->F_2 be symmetric with weight profile f^#, and let t>0. Then + + deg_alg(f)<=2^t-1 + + if and only if + + f^#(r+2^t)=f^#(r) + + for every r with r+2^t<=n. + + Equivalently, the finite word + + f^#(0),f^#(1),...,f^#(n) + + is the restriction of a sequence having period 2^t. + formal_status: formalized + declarations: + - CryptBoolean.symmetricANFCoefficient_add_two_pow + - CryptBoolean.functionAlgebraicDegree_le_two_pow_sub_one_iff_profile_periodic + references: [48] + fidelity_note: >- + Carlet writes the sequence (f^#(r))_(r>=0), although the profile was + defined only on {0,...,n}. The displayed finite periodicity is the exact + domain-correct interpretation. Period 2^t means a period, not + necessarily the least period; when 2^t>n the condition and degree bound + are both automatic. + reuse_note: >- + Reuse Relation (72) and the canonical algebraic degree. The proof is a + finite binary-Mobius calculation and introduces no infinite extension + into the production definition. + dependencies: + - carlet-10-rel-72-anf + - carlet-2-def-algebraic-degree + + - id: carlet-10-krawtchouk-fourier-walsh + kind: theorem-family + location: >- + Fourier and Walsh transforms (Carlet, Section 10.2, p. 143) + statement: |- + For 0<=r<=n let phi_r be the indicator of the weight-r layer of V_n. + If a in V_n has Hamming weight l, then its raw pseudo-Boolean Fourier + coefficient is + + hat(phi_r)(a)=K_(n,r)(l) + =sum_(j=0)^n (-1)^j binom(l,j) + binom(n-l,r-j). + + The Krawtchouk values are characterized by + + sum_(r=0)^n K_(n,r)(l) z^r + =(1-z)^l (1+z)^(n-l). + + Consequently, if f is symmetric with weight profile f^#, then every + raw Fourier and Walsh coefficient depends only on l=w_H(a), and + + hat(f)(a)=sum_(r=0)^n f^#(r) K_(n,r)(l), + + W_f(a)=sum_(r=0)^n (-1)^(f^#(r)) K_(n,r)(l). + formal_status: formalized + declarations: + - CryptBoolean.sum_weightLayer_vectorWalshCharacter_eq_krawtchoukValue + - CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_krawtchoukValue + - FABL.coeff_krawtchoukGeneratingPolynomial + - FABL.krawtchoukGeneratingPolynomial_eq_negativeCount + - CryptBoolean.krawtchoukValue_binaryCubeSignEquiv_eq_signedChooseSum + - CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_signedChooseSum + - CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_coeff + - CryptBoolean.rawFourierTransform_booleanRealEmbedding_weightLayerIndicator_eq_eval + - CryptBoolean.walshTransform_weightLayerIndicator_cast_eq_krawtchoukValue + - CryptBoolean.IsSymmetricBooleanFunction.booleanRealEmbedding_eq_sum_weightLayerIndicator + - CryptBoolean.IsSymmetricBooleanFunction.rawFourierTransform_eq_sum_krawtchoukValue + - CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_krawtchoukValue + - CryptBoolean.sum_krawtchoukValue_binaryCubeSignEquiv + - CryptBoolean.IsSymmetricBooleanFunction.walshTransform_cast_eq_sum_signed_krawtchoukValue + references: [95, 255] + fidelity_note: >- + The transforms are Carlet's unnormalized sums. Binomial coefficients + outside their natural range are zero. FABL's Krawtchouk API uses the + equivalent sign-cube elementary-symmetric convention, so an explicit + binary/sign and index-orientation theorem is required before reuse. + reuse_note: >- + Reuse the raw pseudo-Boolean Fourier transform, the raw Walsh transform, + their Boolean sign relation, and FABL's Krawtchouk generating + polynomial and negative-coordinate-count evaluation. + dependencies: + - carlet-10-def-symmetric + - carlet-2-pseudoboolean-fourier + - carlet-2-def-walsh-transform + + - id: carlet-10-even-middle-layer-normality + kind: theorem + location: >- + Even-dimensional middle-layer restriction (Carlet, Section 10.3, + p. 143 and footnote 55) + statement: |- + Let n>0 be even and define the n/2-dimensional affine flat + + A={x in V_n | x_(i+n/2)=x_i+1 for 1<=i<=n/2}. + + Every point of A has Hamming weight n/2. Hence every Boolean function + that is constant on the full middle layer + + {x in V_n | w_H(x)=n/2} + + is constant on A and is n/2-normal. In particular, every symmetric + Boolean function on V_n is n/2-normal. + formal_status: formalized + declarations: + - CryptBoolean.complementaryPairDirectionLinearMap + - CryptBoolean.complementaryPairDirectionLinearMap_apply_append + - CryptBoolean.complementaryPairDirectionLinearMap_injective + - CryptBoolean.complementaryPairDirectionSubspace + - CryptBoolean.complementaryPairDirectionLinearEquiv + - CryptBoolean.complementaryPairDirectionLinearEquiv_apply_coe + - CryptBoolean.complementaryPairBase + - CryptBoolean.complementaryPairPoint_append + - CryptBoolean.card_f₂Support_complementaryPairPoint + - CryptBoolean.finrank_complementaryPairDirectionSubspace + - CryptBoolean.isConstantOnAffineFlat_of_coordinateRestriction_eq_const + - CryptBoolean.card_f₂Support_eq_middle_of_mem_complementaryPairAffineFlat + - CryptBoolean.isKNormal_even_of_constant_on_middleLayer + - CryptBoolean.IsSymmetricBooleanFunction.isConstantOnComplementaryPairFlat_even + - CryptBoolean.IsSymmetricBooleanFunction.isKNormal_even + fidelity_note: >- + The general middle-layer statement is Carlet's footnote 55 and the + symmetric case is its immediate specialization. The affine flat and its + dimension are explicit, so normality is witnessed rather than inferred + from a cardinality alone. + reuse_note: >- + Reuse fixed-dimensional normality, affine-flat coordinate models, and + the symmetric weight-profile characterization. + dependencies: + - carlet-10-def-symmetric + - carlet-5-def-4-normality + + - id: carlet-10-even-bent-symmetric-classification + kind: classification + location: >- + Savicky's classification of bent symmetric functions (Carlet, + Section 10.3, p. 143) + statement: |- + Let n>0 be even, let + + q_n(x)=sum_(1<=iF_2 be symmetric. Then f is bent if and only if + + f=q_n+a p_n+b + + for some a,b in F_2. Equivalently, the four bent symmetric functions + are q_n, q_n+1, q_n+p_n, and q_n+p_n+1. Each has nonlinearity + + 2^(n-1)-2^(n/2-1). + formal_status: formalized + declarations: + - CryptBoolean.isBent_completeQuadraticBit_add_affineFunction_smul_fullDirection + - CryptBoolean.symmetric_isBent_iff_completeQuadraticBit_add_affineFunction_smul_fullDirection + - CryptBoolean.nonlinearity_eq_two_pow_sub_two_pow_half_of_symmetric_isBent + references: [319] + fidelity_note: >- + The source phrases this as the complete list of bent symmetric + functions in even dimension. Writing the affine perturbation as + a p_n+b records all four functions without identifying complements; + the displayed nonlinearity is the standard bent value. + reuse_note: >- + Derive the classification from Theorem 16 and the Chapter 6 complete- + quadratic bent theorem. Reuse the canonical bentness and nonlinearity + APIs without defining a symmetric-specific version of either. + dependencies: + - carlet-10-theorem-16 + - carlet-6-def-7-bent + - carlet-6-rel-56-complete-quadratic + + - id: carlet-10-theorem-16 + kind: theorem + location: Theorem 16 (Carlet, Section 10.3, pp. 143--144) + statement: |- + Let n>0 be even and let f:V_n->F_2 be symmetric. Then f satisfies + PC(2) if and only if + + f=q_n+a p_n+b + + for some a,b in F_2, where + + q_n(x)=sum_(1<=i- + The source includes every positive even n, including n=2. The canonical + PC(2) predicate quantifies over all nonzero directions of Hamming weight + at most two, exactly matching Carlet's convention. + reuse_note: >- + Reuse the Chapter 4 propagation predicate and the low-degree symmetric + classification. The proof needs only the pure derivative calculation + in every weight-two coordinate direction. + dependencies: + - carlet-10-def-symmetric + - carlet-10-low-degree-classification + - carlet-4-def-propagation-criteria + + - id: carlet-10-odd-weak-normality-bound + kind: theorem + location: >- + Odd-dimensional affine restriction and nonlinearity bound (Carlet, + Section 10.3, p. 144) + statement: |- + Let n>0 be odd and let f:V_n->F_2 be symmetric. Pair the first + (n-1)/2 coordinates with the next (n-1)/2 complementary coordinates + and leave the last coordinate free, obtaining the affine flat + + A={x in V_n | + x_(i+(n-1)/2)=x_i+1 for 1<=i<=(n-1)/2}. + + The flat A has dimension (n+1)/2, and f restricted to A is affine. + Consequently f is (n+1)/2-weakly-normal and + + nl(f)<=2^(n-1)-2^((n-1)/2). + formal_status: formalized + declarations: + - CryptBoolean.isAffineOnAffineFlat_of_coordinateRestriction_eq_affineFunction + - CryptBoolean.IsSymmetricBooleanFunction.isAffineOnComplementaryPairFlat_odd + - CryptBoolean.IsSymmetricBooleanFunction.isKWeaklyNormal_odd + - CryptBoolean.IsSymmetricBooleanFunction.nonlinearity_le_odd + fidelity_note: >- + On A the Hamming weight has one value on the hyperplane where the free + coordinate is zero and the adjacent value on its complement, so the + restriction is an arbitrary one-variable Boolean function and hence + affine. The n=1 endpoint is valid and gives nonlinearity zero. + reuse_note: >- + Reuse weak normality, affine-flat restriction, and Relation (42). The + symmetric weight-profile theorem supplies the two constant slices. + dependencies: + - carlet-10-def-symmetric + - carlet-5-def-4-normality + - carlet-5-affine-flat-restriction-bound + + - id: carlet-10-odd-optimal-nonlinearity-classification + kind: classification + location: >- + Odd-dimensional equality classification (Carlet, Section 10.3, + p. 144) + statement: |- + Let n>0 be odd and let f:V_n->F_2 be symmetric. Then + + nl(f)=2^(n-1)-2^((n-1)/2) + + if and only if + + f=q_n+a p_n+b + + for some a,b in F_2. Thus the only symmetric functions attaining the + odd-dimensional quadratic nonlinearity bound are q_n, q_n+1, + q_n+p_n, and q_n+p_n+1. + formal_status: formalized + declarations: + - CryptBoolean.completeQuadraticBit_odd_eq_hyperplaneExtension + - CryptBoolean.nonlinearity_completeQuadraticBit_odd + - CryptBoolean.symmetricQuadraticNormalForm_eq_completeQuadratic_add_affineFunction + - CryptBoolean.nonlinearity_symmetricQuadraticNormalForm_odd + - CryptBoolean.nonlinearity_eq_odd_quadraticBound_of_eq_symmetricQuadraticNormalForm + - CryptBoolean.completeQuadraticPolarFrequency_fullDirection_odd + - CryptBoolean.domainTranslate_completeQuadraticBit_add_affineFunction + - CryptBoolean.exists_affineFunction_hammingDistance_eq_nonlinearity + - CryptBoolean.exists_completeQuadraticBit_minimumAffineError_one_at_endpoints_odd + - CryptBoolean.hammingWeight_add_lt_of_support_nonempty_of_subset + - CryptBoolean.exists_symmetricQuadraticNormalForm_of_odd_optimal_nonlinearity + - CryptBoolean.symmetric_odd_optimal_nonlinearity_iff_symmetricQuadraticNormalForm + references: [262] + fidelity_note: >- + Carlet states the classification for positive odd n. At n=1 the four + displayed parameter pairs enumerate all four one-variable Boolean + functions and the bound is zero, so the endpoint is consistent. + reuse_note: >- + Reuse Theorem 17, the complete quadratic spectrum, the symmetric + low-degree classification, and the canonical nonlinearity/Walsh + identity. + dependencies: + - carlet-10-theorem-17 + - carlet-10-low-degree-classification + - carlet-6-rel-56-complete-quadratic + + - id: carlet-10-theorem-17 + kind: theorem + location: Theorem 17 (Carlet, Section 10.3, p. 144) + statement: |- + Let n>0, let f:V_n->F_2 be symmetric, and let l be an integer with + 0F_2 + + by + + h_l(y_1,...,y_(n-2l)) + =f(x_1,...,x_l,x_1+1,...,x_l+1, + y_1,...,y_(n-2l)), + + where x_1,...,x_l are arbitrary. Equivalently, + + h_l^#(r)=f^#(r+l) for 0<=r<=n-2l. + + This definition is independent of the arbitrary x_i, and + + nl(f)<=2^(n-1)-2^(n-l-1)+2^l nl(h_l). + formal_status: formalized + declarations: + - CryptBoolean.complementaryPairRestriction + - CryptBoolean.IsSymmetricBooleanFunction.eq_complementaryPairRestriction + - CryptBoolean.IsSymmetricBooleanFunction.isSymmetric_complementaryPairRestriction + - CryptBoolean.symmetricWeightProfileNat_complementaryPairRestriction + - CryptBoolean.coordinateAffineSubspaceRestriction_complementaryPair_eq_directSum + - CryptBoolean.theorem_17_nonlinearity_complementaryPairRestriction + references: [65] + fidelity_note: >- + The source writes 0