From 992ee1d04b373900d7677ab3e510b34d2a3c6e62 Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Tue, 28 Jul 2026 15:10:02 -0400 Subject: [PATCH] Release v0.5.1 --- .agents/PLAN.md | 17 +- .agents/SPEC.md | 17 +- .agents/audit/dependency-dag.md | 50 +- .agents/audit/fidelity.md | 29 +- .agents/inventory/carlet-chapter06.yaml | 642 ++++++++++--- AGENTS.md | 15 +- .../Carlet/Chapter02/Foundations.lean | 47 + .../FiveVariableMaximumNonlinearity.lean | 33 +- CryptBoolean/Carlet/Chapter06.lean | 9 + .../Chapter06/AdditionalDecompositions.lean | 828 +++++++++++++++++ .../Carlet/Chapter06/CayleyGraph.lean | 177 ++++ CryptBoolean/Carlet/Chapter06/DualAffine.lean | 28 + .../Carlet/Chapter06/FlatSwitching.lean | 8 +- .../Chapter06/HadamardDifferenceSet.lean | 220 +++++ .../Chapter06/HyperplaneRestriction.lean | 4 +- .../Carlet/Chapter06/IndirectSum.lean | 27 - .../Carlet/Chapter06/MaioranaMcFarland.lean | 30 +- .../Chapter06/MaioranaMcFarlandBalance.lean | 145 +++ .../MaioranaMcFarlandBentSubspace.lean | 165 ++++ .../Chapter06/MaioranaMcFarlandCounting.lean | 28 - CryptBoolean/Carlet/Chapter06/NestedBent.lean | 57 +- .../Carlet/Chapter06/NormalExtension.lean | 7 - .../Carlet/Chapter06/PSapCounting.lean | 202 ++++ .../Carlet/Chapter06/SecondaryClasses.lean | 873 ++++++++++++++++++ .../Chapter06/SecondarySpecializations.lean | 246 +++++ .../Carlet/Chapter06/SupportCode.lean | 4 +- .../Chapter06/SupportCodeAlternatives.lean | 127 +++ README.md | 4 +- .../Carlet/Chapter06/Bentness.lean | 48 + .../Carlet/Chapter06/Constructions.lean | 27 +- .../Carlet/Chapter06/Counting.lean | 17 +- .../Chapter06/DecompositionsCounting.lean | 23 +- .../Carlet/Chapter06/Duality.lean | 2 +- .../Chapter06/SecondaryConstructions.lean | 64 +- .../scripts/check_statement_style.py | 4 +- blueprint-verso/scripts/validate_manifest.py | 12 +- lakefile.lean | 2 +- 37 files changed, 3924 insertions(+), 314 deletions(-) create mode 100644 CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean create mode 100644 CryptBoolean/Carlet/Chapter06/CayleyGraph.lean create mode 100644 CryptBoolean/Carlet/Chapter06/HadamardDifferenceSet.lean create mode 100644 CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean create mode 100644 CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean create mode 100644 CryptBoolean/Carlet/Chapter06/PSapCounting.lean create mode 100644 CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean create mode 100644 CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean create mode 100644 CryptBoolean/Carlet/Chapter06/SupportCodeAlternatives.lean diff --git a/.agents/PLAN.md b/.agents/PLAN.md index a1f2607..6e1ca54 100644 --- a/.agents/PLAN.md +++ b/.agents/PLAN.md @@ -8,13 +8,13 @@ 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 209 source-facing statement nodes: 206 formalized nodes -associated with 1338 proved Lean declarations and 3 visibly open nodes, connected by 467 reviewed +The current Blueprint baseline contains 222 source-facing statement nodes: 219 formalized nodes +associated with 1418 proved Lean declarations and 3 visibly open nodes, connected by 493 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 5 contributes 31 nodes (28 formalized and 3 open), 203 declarations, and 70 incoming edges. Chapter -6 contributes 57 formalized nodes, 361 declarations, and 163 incoming edges. These counts are a +6 contributes 70 formalized nodes, 441 declarations, and 189 incoming edges. These counts are a synchronized verification contract shared by the inventories, Verso sources, `blueprint-verso/scripts/validate_manifest.py`, and `AGENTS.md`. @@ -78,7 +78,7 @@ tooling pipeline runs, and no local filesystem path appears in package metadata. ## Phase 1 - Complete Carlet inventory Status: in progress. Chapters 2--6 are source-reviewed and Blueprint-synchronized under -`.agents/inventory/`. Chapter 6 has 57 promoted mathematical statements and 19 additional +`.agents/inventory/`. Chapter 6 has 70 promoted mathematical statements and 18 additional source-recovery records covering cited or underspecified families that are not yet promoted to Blueprint nodes. Chapters 7--10 are not yet inventoried. @@ -213,10 +213,13 @@ bent/resilient construction phases. ## Phase 6 - Chapter 6 bent functions -Status: complete. All 57 reviewed nodes are formalized by 361 proved declarations with 163 -reviewed dependency edges. The completed surface includes bentness and its dual, the Rothaus bound +Status: complete. All 70 reviewed nodes are formalized by 441 proved declarations with 189 +reviewed dependency edges. The completed surface includes bentness, its Hadamard-matrix, +difference-set, and strongly regular Cayley-graph characterizations, its dual, the Rothaus bound and Relation (47), the reusable McEliece--Ax character-sum divisibility theorem, primary and -secondary constructions, decompositions and counting, NNF, geometric and second-order +secondary constructions including Classes D₀, D, and C and two further Theorem 10 +specializations, hyperplane and codimension-two decompositions, the exact `PS_ap` count, NNF, +geometric and second-order characterizations, the hyper-bent partial-spread family, partially bent and plateaued superclasses, normal extensions, and the explicit finite-field Kerdock construction and code parameters. diff --git a/.agents/SPEC.md b/.agents/SPEC.md index 9219683..b8fd23b 100644 --- a/.agents/SPEC.md +++ b/.agents/SPEC.md @@ -32,13 +32,13 @@ PDFs, manifests, graphs, and caches are not sources of truth. ## Current verified baseline -The reviewed Blueprint contains 209 source-facing statements, of which 206 are associated with -1338 proved Lean declarations and 3 remain visibly open, connected by 467 mathematical dependency +The reviewed Blueprint contains 222 source-facing statements, of which 219 are associated with +1418 proved Lean declarations and 3 remain visibly open, connected by 493 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. Chapter 5 contributes 31 statements (28 formalized and 3 open), 203 declarations, and 70 incoming -edges. Chapter 6 contributes 57 formalized statements, 361 declarations, and 163 incoming edges. +edges. Chapter 6 contributes 70 formalized statements, 441 declarations, and 189 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 @@ -67,10 +67,13 @@ trace-character/nonlinearity reduction. The quadratic trace representation is cl and even dimensions. The three open nodes preserve the complete analytic source statements for the Weil character-sum bound, its nonlinearity corollary, and the reciprocal character-sum bound. -The Chapter 6 inventory is source-reviewed and Blueprint-synchronized. Its 57 formalized nodes -cover the spectral and derivative characterizations of bentness, duality, the Rothaus and -McEliece--Ax algebraic-degree bounds, primary and secondary constructions, decompositions and -counting, NNF, geometric and second-order characterizations, hyper-bent functions, partially bent +The Chapter 6 inventory is source-reviewed and Blueprint-synchronized. Its 70 formalized nodes +cover the spectral, derivative, Hadamard-matrix, difference-set, and strongly regular Cayley-graph characterizations of bentness, +duality, the balanced-hyperplane and codimension-two decomposition theorems, the Rothaus and +McEliece--Ax algebraic-degree bounds, primary and secondary constructions including Classes D₀, +D, and C and the two promoted Theorem 10 specializations, decompositions, the exact `PS_ap` +count, NNF, +geometric and second-order characterizations, hyper-bent functions, partially bent and plateaued superclasses, normal extensions, and the explicit finite-field Kerdock family and code parameters. The proofs reuse FABL's canonical Fourier, ANF, degree, affine, and derivative interfaces and the Chapter 2--5 Walsh, Reed--Muller, nonlinearity, quadratic, trace, restriction, diff --git a/.agents/audit/dependency-dag.md b/.agents/audit/dependency-dag.md index 94d7124..dfafe47 100644 --- a/.agents/audit/dependency-dag.md +++ b/.agents/audit/dependency-dag.md @@ -16,8 +16,8 @@ spine. The current baseline is: | Carlet Chapter 3 | 7 | 7 | 0 | 32 | 19 | | Carlet Chapter 4 | 73 | 73 | 0 | 568 | 159 | | Carlet Chapter 5 | 31 | 28 | 3 | 203 | 70 | -| Carlet Chapter 6 | 57 | 57 | 0 | 361 | 163 | -| **Total** | **209** | **206** | **3** | **1338** | **467** | +| Carlet Chapter 6 | 70 | 70 | 0 | 441 | 189 | +| **Total** | **222** | **219** | **3** | **1418** | **493** | 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 @@ -621,7 +621,7 @@ rational-function estimate. Across the four Chapter 5 families, the reviewed cou ## Chapter 6: bent functions -Chapter 6 has 57 reviewed statements, all formalized by 361 proved declarations with 163 incoming +Chapter 6 has 70 reviewed statements, all formalized by 441 proved declarations with 189 incoming statement edges. Its graph reuses the Chapter 2 raw Walsh, Fourier, NNF, Poisson, derivative, and trace layers; the Chapter 3 Reed--Muller layer; the Chapter 4 nonlinearity, propagation, support-code, and linear-structure layers; and the Chapter 5 quadratic, restriction, trace, and @@ -638,9 +638,16 @@ carlet-6-lemma-2-walsh-congruence carlet-6-theorem-8-perfect-nonlinearity <- carlet-6-def-7-bent, carlet-2-rel-25-wiener-khinchin, carlet-4-def-propagation-criteria +carlet-6-hadamard-difference-set-characterizations + <- carlet-6-def-7-bent, carlet-6-theorem-8-perfect-nonlinearity, + carlet-2-def-support-weight +carlet-6-bent-cayley-strongly-regular + <- carlet-6-hadamard-difference-set-characterizations carlet-6-prop-16-support-code <- carlet-6-def-7-bent, carlet-4-resiliency-support-dual-distance, carlet-2-balanced-zero-walsh, carlet-2-parseval +carlet-6-support-code-alternate-characterizations + <- carlet-6-prop-16-support-code carlet-6-dual <- carlet-6-def-7-bent, carlet-2-def-walsh-transform, carlet-2-fourier-inversion @@ -686,6 +693,10 @@ carlet-6-maiorana-mcfarland carlet-6-prop-20-general-maiorana-mcfarland <- carlet-6-maiorana-mcfarland, carlet-5-affine-flat-restriction-bound, carlet-6-def-7-bent +carlet-6-maiorana-mcfarland-balanced-map + <- carlet-6-prop-20-general-maiorana-mcfarland +carlet-6-half-dimensional-bent-subspace + <- carlet-6-maiorana-mcfarland carlet-6-partial-spread-construction <- carlet-6-theorem-12-geometric-characterization @@ -696,10 +707,21 @@ carlet-6-rothaus-construction carlet-6-theorem-9-flat-switching <- carlet-6-theorem-8-perfect-nonlinearity, carlet-6-rel-46-dual-poisson, carlet-2-prop-11-walsh-divisibility, carlet-3-prop-12 +carlet-6-class-d-zero + <- carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching +carlet-6-class-d + <- carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching +carlet-6-class-c + <- carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching carlet-6-theorem-10-slice-construction <- carlet-6-def-7-bent, carlet-6-dual carlet-6-indirect-sum <- carlet-6-theorem-10-slice-construction +carlet-6-maiorana-mcfarland-bent-family-extension + <- carlet-6-theorem-10-slice-construction, carlet-6-maiorana-mcfarland +carlet-6-class-d-zero-four-block + <- carlet-6-theorem-10-slice-construction, carlet-6-maiorana-mcfarland, + carlet-6-class-d-zero carlet-6-prop-21-permutation-reindexing <- carlet-6-def-7-bent, carlet-2-def-hamming-distance carlet-6-prop-22-three-function-identity @@ -713,18 +735,30 @@ carlet-6-theorem-11-hyperplane-restrictions carlet-6-hyperplane-restriction-plateaued <- carlet-6-theorem-11-hyperplane-restrictions, carlet-6-def-plateaued, carlet-4-rel-35-nonlinearity-walsh +carlet-6-balanced-hyperplane-derivative-restrictions + <- carlet-6-theorem-11-hyperplane-restrictions, + carlet-6-theorem-8-perfect-nonlinearity +carlet-6-codimension-two-restrictions + <- carlet-6-theorem-10-slice-construction, carlet-6-dual, + carlet-6-quadratic-bent-characterization, + carlet-6-prop-24-second-order-characterization ``` The flat-switching proof composes the Chapter 2 Walsh-divisibility theorem with the Chapter 3 -minimum-weight affine-flat classification. The general slice construction owns the indirect-sum -and Rothaus specializations. The hyperplane decomposition uses the exact restriction-square -identity rather than introducing a second spectral normalization. +minimum-weight affine-flat classification. Classes D₀, D, and C combine its converse with the +canonical Maiorana--McFarland family. The general slice construction owns the indirect-sum, +Maiorana--McFarland bent-family, four-block class-D₀, and Rothaus specializations. The hyperplane decomposition uses the exact restriction-square +identity. The codimension-two result composes raw Fourier involution, bent duality, Parseval, and +the two-variable quadratic radical criterion without introducing a second spectral normalization. ### Counting and three characterizations ```text carlet-6-maiorana-mcfarland-count <- carlet-6-maiorana-mcfarland +carlet-6-psap-count + <- carlet-6-prop-25-psap-hyper-bent, + carlet-4-resiliency-support-dual-distance carlet-6-naive-bent-count-bound <- carlet-6-prop-18-rothaus-degree-bound, carlet-3-reed-muller-dimension @@ -840,7 +874,7 @@ constructs such a family and proves its parameters; the separate coordinate theo self-dual-normal-basis identity under its explicit Frobenius, trace, and trace-pairing hypotheses without conflating it with the coordinate-invariant construction. -These Chapter 6 families contain exactly 163 incoming statement edges. +These Chapter 6 families contain exactly 189 incoming statement edges. ## Remaining proof frontier @@ -864,7 +898,7 @@ and the sharp higher-order upper bound are associated with their complete produc their mathematical ingredients remain separately visible in the graph. Chapter 5's quadratic normal form, quadratic trace representation, Relation (42), random-nonnormality limit, and trace-character reduction are closed; the three analytic open nodes above define the remaining -reviewed frontier. Chapter 6 is closed: all 57 nodes have proved associations, while its nineteen +reviewed frontier. Chapter 6 is closed: all 61 nodes have proved associations, while its eighteen source-recovery records remain outside the graph until their cited statements or certificates can be recovered faithfully. diff --git a/.agents/audit/fidelity.md b/.agents/audit/fidelity.md index 07b3d1d..7a5764f 100644 --- a/.agents/audit/fidelity.md +++ b/.agents/audit/fidelity.md @@ -21,11 +21,11 @@ The generated manifest currently verifies the following baseline: | Carlet Chapter 3 | 7 | 7 | 0 | 32 | 19 | | Carlet Chapter 4 | 73 | 73 | 0 | 568 | 159 | | Carlet Chapter 5 | 31 | 28 | 3 | 203 | 70 | -| Carlet Chapter 6 | 57 | 57 | 0 | 361 | 163 | -| **Total** | **209** | **206** | **3** | **1338** | **467** | +| Carlet Chapter 6 | 66 | 66 | 0 | 421 | 181 | +| **Total** | **222** | **219** | **3** | **1418** | **493** | The manifest count is an association count, not a claim that every printed result in Carlet -Chapters 2--6 is complete. Coverage outside these 209 reviewed nodes remains governed by the +Chapters 2--6 is complete. Coverage outside these 222 reviewed nodes remains governed by the inventories under `.agents/inventory/`. ## Corrected source mappings @@ -77,7 +77,13 @@ inventories under `.agents/inventory/`. | `carlet-5-covering-sequence-resiliency` | Carlet p. 74 derives correlation-immunity and resiliency orders from the minimum nonzero transform-fiber weight and gives converses at the first failed order. | The forward and converse declarations retain the stated minimum and nontrivial-level conditions on every feasible order. The Walsh-zero coefficient sequence is constructed explicitly from its defining formula. | | `carlet-5-derivative-space-partial-covering-sequence` | Carlet p. 74: a nonzero binary space of derivatives has pointwise integer sum zero or half its cardinality, and a minimal representative direction set gives a nontrivial partial covering sequence. | Ten declarations model the finite Boolean-function subspace, prove the half-cardinality dichotomy, choose one direction per derivative, prove the resulting derivative map is bijective and the representative set has cardinality `|D|`, and establish the two-level partial-covering property with nonzero upper level. | | `carlet-5-theorem-6-weight-corollary` | Carlet p. 76 divides by a nonzero level `rho` to write `W_f(0)=(1-rho'/rho) sum_(x in A)(-1)^f(x)`. | The associated theorem proves the equivalent integer identity `rho W_f(0)=(rho-rho') sum_(x in A)(-1)^f(x)`, valid even at `rho=0`; the printed quotient follows under its stated nonzero hypothesis. | +| `carlet-6-hadamard-difference-set-characterizations` | Carlet p. 78: bentness is equivalent to the translation sign matrix being Hadamard and to the support being a difference set in the additive binary cube. | The matrix identity is proved directly through autocorrelation. The difference-set predicate exposes the exact nonzero-difference multiplicity and Hadamard parameter; its positive even-dimensional theorem composes the derivative characterization with one shared Hamming support identity. | | `carlet-6-prop-16-support-code` | Carlet Proposition 16, p. 79: the support of a bent function generates the ambient space and yields a binary linear code with dual distance at least three. | The printed unrestricted statement is false in dimension two: a weight-one bent function has singleton support. The formal node makes the necessary `n>=4` hypothesis explicit and proves both spanning and the dual-distance conclusion. | +| `carlet-6-support-code-alternate-characterizations` | Carlet p. 79 reports two further iff criteria: full dimension with two nonzero weights summing to the length, and even length with two nonzero weights including `2^(n-2)`. | Both converses are false as printed. A complement-of-one-point function on `V_4` satisfies the first condition with weights `7,8`, while a nonconstant linear function satisfies the second with length `8` and weights `4,8`; their zero-frequency Walsh values prove that neither is bent. | +| `carlet-6-maiorana-mcfarland-balanced-map` | Carlet p. 85: every bent representation `f(x,y)=x dot phi(y)+g(y)` has a balanced, uniformly distributed map `phi`. | The formal predicate states the exact fiber cardinality `2^(s-r)`. Relation (49) gives constant-magnitude raw character sums on each fiber, and raw Plancherel proves uniformity directly without importing a parallel vectorial Fourier layer. | +| `carlet-6-half-dimensional-bent-subspace` | Carlet p. 86: in every positive even dimension `2m`, an `m`-dimensional linear space of Boolean functions exists whose nonzero members are bent. | Binary coordinates identify `V_m` with `GF(2^m)`. Multiplication by each field parameter gives a linear family of Maiorana--McFarland functions; nonzero multiplication is bijective, so the existing Maiorana--McFarland criterion proves bentness, and injectivity gives exact dimension `m`. | +| `carlet-6-balanced-hyperplane-derivative-restrictions` | Carlet p. 97: if all nonzero derivatives in a fixed hyperplane are balanced, both hyperplane-coset restrictions are bent. | A linear equivalence presents the arbitrary hyperplane as the zero last-coordinate slice. The proof decomposes autocorrelation into the two restrictions and uses raw Fourier inversion plus the integral two-squares lemma to force both Walsh magnitudes. | +| `carlet-6-codimension-two-restrictions` | Carlet p. 97: four codimension-two coset restrictions of a bent function have the same Walsh-magnitude set, and all four are bent exactly when the indicated second derivative of the dual is one. | After choosing coordinates, Fourier involution gives the exact raw scaling between restriction coefficients and two-variable dual slices. Their bent-or-affine Walsh profiles and Parseval prove equality of magnitude sets; the two-variable quadratic radical criterion proves the second-derivative equivalence. | | `carlet-6-prop-18-rothaus-degree-bound` | Carlet Proposition 18, p. 83 gives degree at most `n/2` for even `n>=4`; the following sentence treats `n=2`. | The main theorem retains `n>=4`. A separate declaration proves that every two-variable bent function has algebraic degree exactly two, and the same conclusions are applied independently to the dual. | | `carlet-6-prop-19` | Carlet Proposition 19, Relation (47), p. 83 relates the algebraic degrees `d` and `d_tilde` of a bent function and its dual by `(n/2-d) >= (n/2-d_tilde)/(d_tilde-1)`. | One associated declaration proves the reusable McEliece--Ax divisibility `2^ceil(n/d) | sum_x (-1)^f(x)` for every positive degree bound `d`; the second composes it with Relation (46), an exact top-ANF-slice valuation, the dual degree bound, and the separate `n=2` case to prove the source's rational inequality. | | `carlet-6-partial-spread-construction` | Carlet pp. 86--88 constructs the `PS^-` and `PS^+` bent families from a spread of `V_{2m}`. | The formal statement uses `m>=2`, the smallest range in which the two printed support-cardinality choices and the stated nonzero-subspace geometry are simultaneously valid. No degenerate low-dimensional family is silently admitted. | @@ -123,11 +129,10 @@ needs an explicit fidelity decision: ### Chapter 6 source-recovery boundary -Nineteen Chapter 6 records remain outside the promoted Blueprint graph. They preserve the source +Eighteen Chapter 6 records remain outside the promoted Blueprint graph. They preserve the source boundary without manufacturing declarations from survey prose or incomplete citations: -- equivalent Hadamard, difference-set, and Cayley-graph characterizations; alternate support-code, - derivative-moment, and geometric/GPS descriptions; +- Cayley-graph characterizations and derivative-moment and geometric/GPS descriptions; - explicit low-degree trace and power families, the `D`, `C`, Dobbertin, vectorial almost-bent, power-sum, homogeneous, and additional primary-class structural results; - cited specializations of the secondary constructions, additional decomposition and counting @@ -177,12 +182,12 @@ source mathematics. | Chapter 5 flat restrictions and normality | `carlet-5-flat-indicator-walsh-nonlinearity`, `carlet-5-rel-42-restriction-nonlinearity`, `carlet-5-affine-flat-restriction-bound`, `carlet-5-def-4-normality`, `carlet-5-random-nonnormality` | Corrected codimension-one flat value, total restriction inequalities, the full equality case, exact fixed-dimension normality predicates, the finite certificate bound, and the exact floored logarithmic random-nonnormality limit | 44 | | Chapter 5 covering sequences | 9 formalized nodes from `carlet-5-def-5-covering-sequence` through `carlet-5-theorem-6-weight-corollary` | Exact integer covering and partial-covering definitions, Walsh characterization, balancedness/resiliency consequences, regular families, the derivative-space representative construction, Theorem 6, and its division-free weight identity | 56 | | Chapter 5 trace-character reduction | `carlet-5-trace-character-sum-walsh` | Reuse of the shared Chapter 2 trace-pairing coordinate theorem, the exact complete-sum Walsh identity, and the conditional maximum-Walsh/nonlinearity reduction | 6 | -| Chapter 6 bentness, duality, and algebraic degree | 14 formalized nodes from `carlet-6-def-7-bent` through `carlet-6-prop-19` | Exact Walsh and derivative characterizations, dual isometry, derivative and Poisson identities, NNF divisibility, the quadratic criterion, the Rothaus bound including dimension two, and Relation (47) through the reusable McEliece--Ax theorem | 43 | -| Chapter 6 constructions and decompositions | 13 formalized nodes from `carlet-6-maiorana-mcfarland` through `carlet-6-hyperplane-restriction-plateaued` | Exact Maiorana--McFarland and partial-spread primary families, flat switching, slicing, direct, indirect, Rothaus, permutation, and three-function constructions, and the hyperplane restriction formulas | 77 | -| Chapter 6 counting and characterizations | 6 formalized nodes from `carlet-6-maiorana-mcfarland-count` through `carlet-6-prop-24-second-order-characterization` | Exact finite counting bounds and NNF, geometric, generalized partial-spread, and second-order characterizations using the canonical raw Fourier normalization | 67 | +| Chapter 6 bentness, duality, and algebraic degree | 17 formalized nodes from `carlet-6-def-7-bent` through `carlet-6-prop-19` | Exact Walsh, derivative, Hadamard-matrix, difference-set, and strongly regular Boolean-Cayley characterizations; finite counterexamples to the two printed alternate support-code converses; dual isometry, derivative and Poisson identities, NNF divisibility, the quadratic criterion, the Rothaus bound including dimension two, and Relation (47) through the reusable McEliece--Ax theorem | 67 | +| Chapter 6 constructions and decompositions | 22 formalized nodes from `carlet-6-maiorana-mcfarland` through `carlet-6-codimension-two-restrictions` | Exact Maiorana--McFarland and partial-spread primary families, uniformity of the Maiorana--McFarland frequency map, the half-dimensional linear space of bent functions, flat switching, Classes D₀, D, and C, the Maiorana--McFarland bent-family extension, the four-block class-D₀ construction, slicing, direct, indirect, Rothaus, permutation, and three-function constructions, the hyperplane restriction formulas, and the balanced-hyperplane and codimension-two decomposition consequences | 125 | +| Chapter 6 counting and characterizations | 7 formalized nodes from `carlet-6-maiorana-mcfarland-count` through `carlet-6-prop-24-second-order-characterization` | Exact Maiorana--McFarland and `PS_ap` counts, the finite naive bound, and NNF, geometric, generalized partial-spread, and second-order characterizations using the canonical raw Fourier normalization | 75 | | Chapter 6 hyper-bent functions and superclasses | 14 formalized nodes from `carlet-6-def-hyper-bent` through `carlet-6-plateaued-coset-orphan` | Exact field/cube coordinate equivalence, subfield-intersection and `PS_ap` construction, partially bent decomposition, uncertainty equality, partial-bent duality, corrected partial-bent type formula and two counterexamples, and plateaued support, derivative, and corrected orphan results | 97 | | Chapter 6 normal extensions and Kerdock codes | 10 formalized nodes from `carlet-6-def-8-normal-extension` through `carlet-6-kerdock-field-construction` | Exact coordinate-invariant extension relation, duality, composition, replacement, and direct-sum/normality results with the affine-flat correction; complete quadratic functions; conditional Kerdock parameters; the explicit trace family; and its separately hypothesized self-dual-normal-coordinate identity | 77 | -| **Total** | **206 items** | | **1338** | +| **Total** | **219 items** | | **1418** | The following distinctions are part of the fidelity boundary: @@ -265,7 +270,7 @@ The following distinctions are part of the fidelity boundary: the self-dual-normal-coordinate identity remain distinct. The identity lists its Frobenius, trace, and trace-pairing hypotheses, while the construction uses the Chapter 5 quadratic-trace polar formula and does not assume those coordinates. -- The nineteen Chapter 6 source-recovery records remain outside the 57-node graph rather than +- The eighteen Chapter 6 source-recovery records remain outside the 61-node graph rather than being weakened into statements without recoverable primary-source parameters or certificates. - Definitions, normalization laws, source propositions, and derived consequences have separate Blueprint nodes when their quantifiers or conclusions differ. @@ -285,7 +290,7 @@ Chapter 3 has no open node: Proposition 12's affine-flat and equality-case slice formalized. Chapter 4 has no open node: its former frontier statements are associated with complete declarations while their principal mathematical ingredients retain independent nodes. Chapter 2 has no open node: the binary-degree formula and Proposition 3 are formalized. Chapter 6 has no open -node: all 57 reviewed statements have proved associations. The four Chapter 5 citation-recovery +node: all 63 reviewed statements have proved associations. The four Chapter 5 citation-recovery records remain outside the 31-node Chapter 5 graph until their source statements are complete. ## Verification perimeter diff --git a/.agents/inventory/carlet-chapter06.yaml b/.agents/inventory/carlet-chapter06.yaml index e8ef610..34cdc3a 100644 --- a/.agents/inventory/carlet-chapter06.yaml +++ b/.agents/inventory/carlet-chapter06.yaml @@ -2,20 +2,20 @@ source: carlet-2010 chapter: 6 status: source-reviewed summary: - statements: 57 - source_statements: 57 - core_items: 57 - blueprint_ready_statements: 57 - source_recovery_items: 19 - total_records: 76 - formalized: 57 + statements: 70 + source_statements: 70 + core_items: 70 + blueprint_ready_statements: 70 + source_recovery_items: 18 + total_records: 88 + formalized: 70 open: 0 - declarations: 361 - dependency_edges: 163 + declarations: 441 + dependency_edges: 189 scope_note: >- - The 57 source-facing items below have complete statements checked + The 70 source-facing items below have complete statements checked against Carlet pages 77--110 and are synchronized with the current Chapter 6 - Blueprint. The 19 records under source_recovery retain complete + Blueprint. The 18 records under source_recovery retain complete and incomplete cited families that have not been promoted to nodes. In particular, the Kerdock parameter theorem is conditional on a given representative family; only the separate finite-field construction states @@ -102,6 +102,78 @@ items: - carlet-2-rel-25-wiener-khinchin - carlet-4-def-propagation-criteria + - id: carlet-6-hadamard-difference-set-characterizations + kind: theorem-family + location: >- + Carlet, Section 6 opening discussion, p. 78 + statement: |- + Let n\ge2 be even and let f:V_n\to\mathbb F_2. The matrix + + H_f(x,y)=(-1)^{f(x+y)} + + is Hadamard if and only if f is bent. If S_f is the support of f and + + N_{S_f}(a)=|\{x\in S_f:x+a\in S_f\}|, + + then f is bent if and only if + + |S_f|\ge2^{n-2}\quad\text{and}\quad + N_{S_f}(a)=|S_f|-2^{n-2}\quad(a\ne0). + + Thus S_f is a Hadamard difference set in the additive group V_n. + formal_status: formalized + declarations: + - CryptBoolean.f₂BitWeight + - CryptBoolean.hammingNorm_eq_sum_f₂BitWeight + - CryptBoolean.hammingNorm_add_restrictSupport_identity + - CryptBoolean.bentSignMatrix + - CryptBoolean.bentSignMatrix_mul_conjTranspose_apply + - CryptBoolean.isBent_iff_bentSignMatrix_isHadamard + - CryptBoolean.differenceMultiplicity + - CryptBoolean.IsHadamardDifferenceSet + - CryptBoolean.differenceMultiplicity_support_eq_hammingNorm_restriction + - CryptBoolean.hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity + - CryptBoolean.isBent_iff_support_isHadamardDifferenceSet + fidelity_note: >- + The Hadamard-matrix equivalence is proved without extra dimension + assumptions. The difference-set equivalence retains the source's positive + even-dimensional domain and states the difference multiplicity and + parameters explicitly; the lower cardinality bound makes natural-number + subtraction faithful to the integer parameter formula. + reuse_note: >- + The proof composes the existing derivative characterization, the Chapter 4 + autocorrelation identity, and the Chapter 2 Hamming-weight API. The generic + support-restriction identity is also reused by the existing dimension-seven + nonlinearity proof. + dependencies: + - carlet-6-def-7-bent + - carlet-6-theorem-8-perfect-nonlinearity + - carlet-2-def-support-weight + + - id: carlet-6-bent-cayley-strongly-regular + kind: theorem + location: >- + Strong regularity of the Boolean Cayley graph (Carlet, p. 78) + statement: |- + Let n\ge2 be even, let f:V_n\to\mathbb F_2 be bent with f(0)=0, and + join distinct x,y\in V_n exactly when f(x+y)=1. If S_f is the support + of f, the resulting graph is strongly regular with parameters + + \left(2^n,\ |S_f|,\ |S_f|-2^{n-2},\ |S_f|-2^{n-2}\right). + formal_status: formalized + declarations: + - CryptBoolean.booleanCayleyGraph + - CryptBoolean.booleanCayleyGraph_adj + - CryptBoolean.card_commonNeighbors_booleanCayleyGraph + - CryptBoolean.degree_booleanCayleyGraph + - CryptBoolean.isSRGWith_booleanCayleyGraph_of_isBent + fidelity_note: >- + The source's strong-regularity sentence is made precise with the standard f(0)=0 Boolean-Cayley convention and the exact parameters forced by the preceding Hadamard difference-set identity. + reuse_note: >- + Common-neighbor counts are identified directly with the existing support difference multiplicity, and the graph itself is Mathlib's additive Cayley graph. + dependencies: + - carlet-6-hadamard-difference-set-characterizations + - id: carlet-6-prop-16-support-code kind: proposition location: >- @@ -140,6 +212,47 @@ items: - carlet-2-balanced-zero-walsh - carlet-2-parseval + - id: carlet-6-support-code-alternate-characterizations + kind: theorem-family + location: >- + Carlet, alternatives following Proposition 16, p. 79; corrected by + four-variable counterexamples + statement: |- + For the support code C_f, the following two reported converses are false + without additional hypotheses absent from the printed statements. + + First, let f_1:V_4\to\mathbb F_2 vanish at (1,0,0,0) and equal one + elsewhere. Then \dim C_{f_1}=4, its two nonzero weights are 7 and 8, + and 7+8=w_H(f_1)=15, but f_1 is not bent. + + Second, let f_2(x)=x_2+x_3 on V_4. Then w_H(f_2)=8 is even, the two + nonzero weights of C_{f_2} are 4 and 8, and 4=2^{4-2}, but f_2 is not + bent. + formal_status: formalized + references: [348] + declarations: + - CryptBoolean.finrank_supportCode_eq_n_iff_injective + - CryptBoolean.SupportCodeHasExactlyTwoNonzeroWeightValues + - CryptBoolean.HasSupportCodeWeightSumAlternative + - CryptBoolean.HasSupportCodeEvenLengthQuarterWeightAlternative + - CryptBoolean.supportCodeWeightSumCounterexample + - CryptBoolean.supportCodeQuarterWeightCounterexample + - CryptBoolean.supportCodeWeightSumAlternative_not_characterize_bent + - CryptBoolean.supportCodeEvenLengthQuarterWeightAlternative_not_characterize_bent + fidelity_note: >- + The survey prints both conditions as iff characterizations. Direct finite + verification in the same support-code model gives counterexamples to both + converses already in dimension four, so no strengthened theorem is + substituted. The exact two-nonzero-weight predicate requires distinct + positive occurring values and ignores the zero word, matching coding-theory + terminology. + reuse_note: >- + Both counterexamples reuse the existing support-code map, code dimension, + and word-weight declarations. The full-dimension/injectivity lemma was + exposed from the proof of Proposition 16 rather than duplicated. + dependencies: + - carlet-6-prop-16-support-code + - id: carlet-6-dual kind: definition location: >- @@ -225,6 +338,7 @@ items: - CryptBoolean.isBent_domainTranslate - CryptBoolean.isBent_domainTranslate_add_linear - CryptBoolean.bentDual_domainTranslate_add_linear + - CryptBoolean.bentDual_add_constant - CryptBoolean.walshTransform_zero_bentDual_derivative_add_linear fidelity_note: >- The complete domains, hypotheses, normalization, and conclusion match the reviewed source passage. @@ -449,9 +563,12 @@ items: \widetilde f(a,b)=b\mathbin\cdot\pi^{-1}(a)+g(\pi^{-1}(a)). formal_status: formalized declarations: + - CryptBoolean.booleanMaioranaMcFarlandPermutation + - CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks - CryptBoolean.isMaioranaMcFarland_of_eq_permutation - CryptBoolean.walshTransform_maioranaMcFarlandPermutation - CryptBoolean.isBent_of_maioranaMcFarlandPermutation + - CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation - CryptBoolean.bentDual_maioranaMcFarlandPermutation - CryptBoolean.isBent_iff_bijective_maioranaMcFarland fidelity_note: >- @@ -496,6 +613,68 @@ items: - carlet-5-affine-flat-restriction-bound - carlet-6-def-7-bent + - id: carlet-6-maiorana-mcfarland-balanced-map + kind: theorem + location: >- + Carlet, structural consequence after Proposition 20, p. 85 + statement: |- + Let n=r+s be even and suppose + + f_{\varphi,g}(x,y)=x\mathbin\cdot\varphi(y)+g(y) + + is bent on V_r\times V_s. Then r\le s and \varphi:V_s\to V_r is + balanced: for every a\in V_r, + + |\varphi^{-1}(a)|=2^{s-r}. + formal_status: formalized + references: [254] + declarations: + - CryptBoolean.IsBalancedCubeMap + - CryptBoolean.isBalancedCubeMap_of_isBent_maioranaMcFarlandGeneral + fidelity_note: >- + The predicate states Carlet's parenthetical meaning of balanced as uniform + distribution, including the exact fiber size. The dimension inequality is + derived from the bent fiber-character criterion rather than assumed. + reuse_note: >- + Relation (49) supplies the raw character sums on each fiber, and the + Chapter 2 raw Plancherel theorem forces every fiber to have cardinality + 2^{s-r}. No parallel vectorial Fourier normalization is introduced. + dependencies: + - carlet-6-prop-20-general-maiorana-mcfarland + + - id: carlet-6-half-dimensional-bent-subspace + kind: theorem + location: >- + Carlet, remark on linear spaces of bent functions, p. 86 + statement: |- + For every m>0, there exists an m-dimensional \mathbb F_2-linear + subspace B of the Boolean functions on V_{2m} such that every nonzero + member of B is bent. + formal_status: formalized + declarations: + - CryptBoolean.binaryGaloisFieldCoordinateEquiv + - CryptBoolean.fieldMultiplicationCubeMap + - CryptBoolean.fieldMaioranaMcFarlandFunction + - CryptBoolean.fieldMaioranaMcFarlandFunction_joinF₂CubeBlocks + - CryptBoolean.fieldMaioranaMcFarlandLinearMap + - CryptBoolean.fieldMultiplicationCubeMap_bijective + - CryptBoolean.isBent_fieldMaioranaMcFarlandFunction + - CryptBoolean.fieldMaioranaMcFarlandLinearMap_injective + - CryptBoolean.maioranaMcFarlandBentSubspace + - CryptBoolean.finrank_maioranaMcFarlandBentSubspace + - CryptBoolean.isBent_of_mem_maioranaMcFarlandBentSubspace + - CryptBoolean.exists_halfDimensionalBentSubspace + fidelity_note: >- + The theorem states existence in every positive even dimension and the + exact half-dimension, with nonzero membership quantified over a genuine + function submodule. + reuse_note: >- + Binary coordinates transport multiplication in GF(2^m) to an m-dimensional + linear family. Every nonzero multiplier is a permutation, so the existing + Maiorana--McFarland iff proves bentness of every nonzero member. + dependencies: + - carlet-6-maiorana-mcfarland + - id: carlet-6-partial-spread-construction kind: theorem location: >- @@ -606,6 +785,7 @@ items: - CryptBoolean.IsBalancedOnAffineFlat - CryptBoolean.IsConstantOrBalancedOnAffineFlat - CryptBoolean.affineFlatWalshSum + - CryptBoolean.affineFlatSubtypeEquiv - CryptBoolean.walshTransform_sub_flatSwitch - CryptBoolean.affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction - CryptBoolean.affineSubspaceRestrictionImbalance_bentDual_add_linear @@ -614,6 +794,7 @@ items: - CryptBoolean.isBent_flatSwitch_iff_derivative_balanced_on_affineFlat - CryptBoolean.isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced - CryptBoolean.derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_balanced + - CryptBoolean.bitSignInt_mul_self - CryptBoolean.two_pow_half_dvd_walshTransform_affineFlatRestriction - CryptBoolean.half_dimension_le_finrank_of_isBent_flatSwitch - CryptBoolean.functionAlgebraicDegree_affineFlatRestriction_le_of_isBent_flatSwitch @@ -628,6 +809,91 @@ items: - carlet-2-prop-11-walsh-divisibility - carlet-3-prop-12 + - id: carlet-6-class-d-zero + kind: theorem + location: >- + Class D_0 (Carlet, pp. 90--91) + statement: |- + Let \pi be a permutation of V_m. The function + + f(x,y)=x\mathbin\cdot\pi(y)+\delta_0(x) + + is bent on V_m\times V_m, and its dual is + + \widetilde f(a,b)=b\mathbin\cdot\pi^{-1}(a)+\delta_0(b). + formal_status: formalized + declarations: + - CryptBoolean.classDZero + - CryptBoolean.classDZero_append + - CryptBoolean.walshTransform_classDZero + - CryptBoolean.isBent_classDZero + - CryptBoolean.bentDual_classDZero_append + fidelity_note: >- + The permutation domain, zero-point correction, bentness, and inverse-permutation dual formula match the reviewed source passage. + reuse_note: >- + The proof reuses the canonical Boolean Maiorana--McFarland function, its exact Walsh spectrum, and affine-flat switching on the zero first-block flat. + dependencies: + - carlet-6-maiorana-mcfarland + - carlet-6-theorem-9-flat-switching + + - id: carlet-6-class-d + kind: theorem + location: >- + Class D (Carlet, pp. 90--91) + statement: |- + Let E_1,E_2 be subspaces of V_m and let \pi be a permutation such + that \pi(E_2)=E_1^\perp. Then + + f(x,y)=x\mathbin\cdot\pi(y)+ + \mathbf1_{E_1}(x)\mathbf1_{E_2}(y) + + is bent on V_m\times V_m. + formal_status: formalized + declarations: + - CryptBoolean.classD + - CryptBoolean.classD_append + - CryptBoolean.isBent_classD + fidelity_note: >- + The two subspaces, permutation-image condition, product indicator, and bentness conclusion match the reviewed source passage. + reuse_note: >- + The product indicator is the indicator of a half-dimensional product subspace, so the proof composes the canonical Maiorana--McFarland construction with the converse direction of affine-flat switching. + dependencies: + - carlet-6-maiorana-mcfarland + - carlet-6-theorem-9-flat-switching + + - id: carlet-6-class-c + kind: theorem + location: >- + Class C (Carlet, pp. 90--91) + statement: |- + Let L be a subspace of V_m and let \pi be a permutation such that + every inverse image \pi^{-1}(a+L^\perp) is an affine flat. Then + + f(x,y)=x\mathbin\cdot\pi(y)+\mathbf1_L(x) + + is bent. More generally, + + f_g(x,y)=x\mathbin\cdot\pi(y)+\mathbf1_L(x)+g(y) + + is bent whenever g restricts affinely to every + \pi^{-1}(a+L^\perp). + formal_status: formalized + declarations: + - CryptBoolean.HasAffinePerpendicularCosetPreimages + - CryptBoolean.IsAffineOnPerpendicularCosetPreimages + - CryptBoolean.isAffineOnPerpendicularCosetPreimages_zero + - CryptBoolean.classC + - CryptBoolean.classC_append + - CryptBoolean.isBent_classC + - CryptBoolean.isBent_classC_zero + fidelity_note: >- + The affine-preimage hypothesis, optional affine offset restrictions, and both bentness conclusions match the reviewed source passage. + reuse_note: >- + The proof uses the exact Maiorana--McFarland dual and Theorem 9's constant-or-balanced dual-coset criterion; arbitrary permutation reindexing is handled by genuine finite equivalences. + dependencies: + - carlet-6-maiorana-mcfarland + - carlet-6-theorem-9-flat-switching + - id: carlet-6-theorem-10-slice-construction kind: theorem location: >- @@ -641,7 +907,10 @@ items: \widetilde f(s,t)=\widetilde{\varphi_s}(t). formal_status: formalized declarations: + - CryptBoolean.finAppend_add - CryptBoolean.firstBlockSlice + - CryptBoolean.secondBlockSlice + - CryptBoolean.walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh - CryptBoolean.dualSliceFunction - CryptBoolean.walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction - CryptBoolean.isBent_iff_forall_isBent_dualSliceFunction @@ -679,6 +948,56 @@ items: dependencies: - carlet-6-theorem-10-slice-construction + - id: carlet-6-maiorana-mcfarland-bent-family-extension + kind: theorem + location: >- + Maiorana--McFarland bent-family extension (Carlet, p. 93) + statement: |- + Let \pi be a permutation of V_r, let g:V_r\to\mathbb F_2, and let + (h_y)_{y\in V_r} be a family of bent functions on V_m, where m is even. + Then + + F(x,y,z)=h_y(z)+x\mathbin\cdot\pi(y)+g(y) + + is bent on V_r\times V_r\times V_m. + formal_status: formalized + declarations: + - CryptBoolean.maioranaMcFarlandBentFamilyExtension + - CryptBoolean.maioranaMcFarlandBentFamilyExtension_append + - CryptBoolean.isBent_maioranaMcFarlandBentFamilyExtension + fidelity_note: >- + The indexed bent-family hypothesis and displayed formula match the reviewed source statement exactly. + reuse_note: >- + The proof specializes Theorem 10 and the exact Maiorana--McFarland dual formula; no second slice or spectral normalization is introduced. + dependencies: + - carlet-6-theorem-10-slice-construction + - carlet-6-maiorana-mcfarland + + - id: carlet-6-class-d-zero-four-block + kind: theorem + location: >- + Four-block class-D_0 construction (Carlet, p. 93) + statement: |- + Let r,s be positive, let \pi and \pi' be permutations of V_r and V_s, + respectively, and let h:V_s\to\mathbb F_2 be arbitrary. Then + + F(x,y,z,t)=x\mathbin\cdot\pi(y)+z\mathbin\cdot\pi'(t)+\delta_0(x)h(t) + + is bent on V_r\times V_r\times V_s\times V_s. + formal_status: formalized + declarations: + - CryptBoolean.classDZeroFourBlock + - CryptBoolean.classDZeroFourBlock_append + - CryptBoolean.isBent_classDZeroFourBlock + fidelity_note: >- + The displayed formula and arbitrary-function hypothesis match the source. The total Lean theorem also covers zero-dimensional coordinate pairs, where the same finite identity remains valid. + reuse_note: >- + The proof uses Theorem 10 to switch each first-block slice between the canonical Maiorana--McFarland and class-D_0 families, and identifies every dual slice with a second Maiorana--McFarland function. + dependencies: + - carlet-6-theorem-10-slice-construction + - carlet-6-maiorana-mcfarland + - carlet-6-class-d-zero + - id: carlet-6-prop-21-permutation-reindexing kind: proposition location: >- @@ -785,6 +1104,8 @@ items: declarations: - CryptBoolean.singletonF₂Cube - CryptBoolean.singletonF₂Cube_apply + - CryptBoolean.singletonF₂CubeLinearEquiv + - CryptBoolean.sum_singletonF₂Cube - CryptBoolean.walshTransform_append_singletonF₂Cube - CryptBoolean.linearHyperplaneRestriction - CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra @@ -828,6 +1149,60 @@ items: - carlet-6-def-plateaued - carlet-4-rel-35-nonlinearity-walsh + - id: carlet-6-balanced-hyperplane-derivative-restrictions + kind: theorem + location: >- + Balanced-derivative decomposition consequence (Carlet, p. 97) + statement: |- + Let f:V_{2k+1}\to\mathbb F_2, and let E be a linear hyperplane. If + D_u f is balanced for every nonzero u\in E, then the restrictions of + f to E and to its complementary coset are bent. + formal_status: formalized + declarations: + - CryptBoolean.isBent_linearHyperplaneRestriction_of_balanced_derivatives + fidelity_note: >- + A linear equivalence identifies an arbitrary hyperplane and its + complementary coset with the two coordinate slices. The compiled theorem + quantifies over that equivalence and proves both restrictions at once. + reuse_note: >- + The proof reuses the existing hyperplane slice, autocorrelation, balanced + derivative, raw Fourier, and bent-spectrum APIs. + dependencies: + - carlet-6-theorem-11-hyperplane-restrictions + - carlet-6-theorem-8-perfect-nonlinearity + + - id: carlet-6-codimension-two-restrictions + kind: theorem + location: >- + Codimension-two decomposition consequences (Carlet, p. 97) + statement: |- + Let f be bent on V_N, with N even, and let E\le V_N have codimension + two. The four restrictions of f to the cosets of E, under any fixed + linear coordinate identification with V_{N-2}, have the same set of + Walsh magnitudes. If E^\perp=\langle a,b\rangle, all four restrictions + are bent if and only if D_aD_b\widetilde f is the constant one function. + formal_status: formalized + references: [41] + declarations: + - CryptBoolean.four_mul_walshTransform_firstBlockSlice_eq + - CryptBoolean.walshMagnitudeSet + - CryptBoolean.walshMagnitudeSet_firstBlockSlice_eq + - CryptBoolean.isBent_firstBlockSlices_iff_bentDual_secondDerivative_eq_one + fidelity_note: >- + The declarations choose coordinates in which E is the first block and + E^\perp is represented by the last two coordinate directions. This is + exactly the source statement after the stated linear identification; + raw and normalized Walsh transforms are not conflated. + reuse_note: >- + The exact scaling identity composes Fourier involution with bent duality. + The magnitude-set theorem uses the complete two-variable Walsh profiles, + and the iff uses the existing quadratic-radical and second-derivative APIs. + dependencies: + - carlet-6-theorem-10-slice-construction + - carlet-6-dual + - carlet-6-quadratic-bent-characterization + - carlet-6-prop-24-second-order-characterization + - id: carlet-6-maiorana-mcfarland-count kind: theorem location: >- @@ -842,14 +1217,11 @@ items: formal_status: formalized declarations: - CryptBoolean.MaioranaMcFarlandParameters - - CryptBoolean.booleanMaioranaMcFarlandPermutation - - CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks - CryptBoolean.booleanMaioranaMcFarlandOfParameters - CryptBoolean.booleanMaioranaMcFarlandOfParameters_injective - CryptBoolean.card_maioranaMcFarlandParameters - CryptBoolean.originalMaioranaMcFarlandClass - CryptBoolean.card_originalMaioranaMcFarlandClass - - CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation - CryptBoolean.originalMaioranaMcFarlandClass_subset_bentFunctionFamily fidelity_note: >- The complete domains, hypotheses, normalization, and conclusion match the reviewed source passage. @@ -858,6 +1230,38 @@ items: dependencies: - carlet-6-maiorana-mcfarland + - id: carlet-6-psap-count + kind: theorem + location: >- + Number of PS_ap functions (Carlet, p. 97) + statement: |- + Let m\ge2. With field division defined at zero, the functions on + \mathbb F_{2^m}\times\mathbb F_{2^m} of the form + + f_g(x,y)=g(x/y), + + where g:\mathbb F_{2^m}\to\mathbb F_2 is balanced, are distinct bent + functions. Their number is + + \binom{2^m}{2^{m-1}}. + formal_status: formalized + declarations: + - CryptBoolean.PSapParameters + - CryptBoolean.card_psapParameters + - CryptBoolean.psapOfParameters + - CryptBoolean.psapOfParameters_coordinate + - CryptBoolean.psapOfParameters_injective + - CryptBoolean.psapClass + - CryptBoolean.card_psapClass + - CryptBoolean.isBent_psapOfParameters_comp_linearEquiv + fidelity_note: >- + The quotient convention, balanced parameter set, injectivity, bentness, and exact binomial cardinality match the reviewed source count. The positive half-dimension is made explicit. + reuse_note: >- + The proof combines the existing PS_ap hyper-bent construction with the Chapter 4 support-cardinality characterization of balancedness and Mathlib's fixed-cardinality finset count. + dependencies: + - carlet-6-prop-25-psap-hyper-bent + - carlet-4-resiliency-support-dual-distance + - id: carlet-6-naive-bent-count-bound kind: theorem location: >- @@ -1864,39 +2268,31 @@ items: - carlet-2-trace-pairing-coordinates source_recovery: - - id: carlet-6-hadamard-difference-set-cayley + - id: carlet-6-cayley-graph-characterization-reference kind: characterization-family location: >- - Carlet, Section 6 opening discussion and Section 6.6.3, pp. 78 and 100 + Carlet, Section 6.6.3, p. 100 source_claim: >- - For f : V_n -> F_2, bentness is equivalent to the matrix - H[x,y] = (-1)^(f(x+y)) being Hadamard and to supp(f) being a difference - set in the elementary Abelian 2-group V_n. The difference-set condition - implies that the Boolean Cayley graph G_f is strongly regular. Carlet later - reports a further characterization of bent functions through Cayley graphs. - statement_status: mixed-complete-equivalences-and-incomplete-cayley-reference + After the separately promoted strongly regular Boolean-Cayley theorem, + Carlet reports a further characterization of bent functions through + Cayley graphs without stating it. + statement_status: incomplete-cayley-reference formal_status: open declarations: [] - references: [18, 134, 202] + references: [18] first_release_scope: required-after-source-recovery fidelity_note: >- - The two equivalences are complete in the survey. The strongly regular - graph sentence omits its parameters, and the later Cayley-graph - characterization is only a citation. Neither is strengthened to an unstated - parameter theorem here. + The complete Hadamard-matrix, difference-set, and exact strongly regular + parameter results have been promoted separately. The later Cayley-graph + characterization remains only a citation. reuse_note: >- - The Walsh and derivative characterizations already provide the scalar - spectral content. Promotion should add explicit Hadamard-matrix, - difference-set, and strongly-regular-graph layers rather than encode those - objects as Boolean-function aliases. + The promoted Boolean Cayley graph and strongly regular parameter theorem + provide the reusable objects. Promotion should identify the exact theorem + direction before adding the cited characterization. blocker: >- - The repository has no reviewed design or graph API for these objects, and - reference [18] must be recovered for the exact Cayley parameters and the - later iff characterization. + Reference [18] must be recovered for the later iff characterization. dependencies: - - carlet-6-def-7-bent - - carlet-6-theorem-8-perfect-nonlinearity - - carlet-2-def-support-weight + - carlet-6-bent-cayley-strongly-regular - id: carlet-6-restricted-derivative-and-moment-families kind: theorem-family @@ -1930,33 +2326,6 @@ source_recovery: - carlet-4-def-propagation-criteria - carlet-2-parseval - - id: carlet-6-support-code-alternate-characterizations - kind: theorem-family - location: >- - Carlet, alternatives following Proposition 16, p. 79 - source_claim: >- - For the support code C_f, Carlet reports two further iff - characterizations of bentness: C_f has dimension n and exactly two - weights whose sum is w_H(f); and the length w_H(f) is even, C_f has - exactly two weights, and one of them is 2^(n-2). - statement_status: complete-source-statements - formal_status: open - declarations: [] - references: [348] - first_release_scope: required-after-source-recovery - fidelity_note: >- - The displayed alternatives are complete, but their small-dimension - conventions must be reconciled with the corrected n >= 4 range of the - existing Proposition 16 node. - reuse_note: >- - Both alternatives should reuse the existing support-code map, dimension, - and weight declarations rather than define a second code. - blocker: >- - No production declaration currently proves either alternative, including - the occurrence and zero-weight edge cases. - dependencies: - - carlet-6-prop-16-support-code - - id: carlet-6-quadratic-trace-families kind: construction-family location: >- @@ -2027,12 +2396,9 @@ source_recovery: location: >- Carlet, structural consequences for primary classes, pp. 85--87 source_claim: >- - Every bent function represented as - f_(phi,g)(x,y)=x dot phi(y)+g(y) has balanced phi; every six-variable - bent function is affinely equivalent to a member of the original - Maiorana--McFarland class; n/2-dimensional vector spaces of n-variable - Boolean functions whose nonzero elements are bent exist, while no such - space has dimension greater than n/2. For the partial-spread classes, + Every six-variable bent function is affinely equivalent to a member of the original + Maiorana--McFarland class; no vector space of n-variable Boolean functions + whose nonzero elements are bent has dimension greater than n/2. For the partial-spread classes, Carlet records the exact degree of PS^- members, the explicit PS_ap quotient form and self-duality, and a field-power/trace characterization of its completed class, while leaving a general ANF characterization of @@ -2040,24 +2406,24 @@ source_recovery: statement_status: mixed-complete-consequences-vectorial-bound-and-explicit-open-problem formal_status: open declarations: [] - references: [24, 81, 134, 254] + references: [24, 81, 134] first_release_scope: required-after-source-recovery fidelity_note: >- - The survey states these as several distinct consequences. The - balanced-vector-map and dimension bound use vectorial Boolean-function - theory, and the open PS ANF problem is not replaced by the explicit - PS_ap subclass. + The survey states these as several distinct consequences. The dimension + bound uses vectorial Boolean-function theory, and the open PS ANF problem + is not replaced by the explicit PS_ap subclass. The balanced-map + consequence and the matching half-dimensional existence construction have + been promoted separately. reuse_note: >- Promotion should specialize the general Maiorana--McFarland and partial-spread nodes and reuse affine equivalence, algebraic degree, and the field trace layer. blocker: >- - The six-variable affine classification, vectorial balance/dimension - bound, and completed-class trace characterization need independent - primary-source statements and proofs. + The six-variable affine classification, vector-space dimension bound, + and completed-class trace characterization need independent primary-source + statements and proofs. dependencies: - carlet-6-maiorana-mcfarland - - carlet-6-prop-20-general-maiorana-mcfarland - carlet-6-partial-spread-construction - carlet-6-dual @@ -2131,42 +2497,32 @@ source_recovery: - carlet-2-def-algebraic-degree - carlet-6-def-7-bent - - id: carlet-6-classes-d-and-c - kind: construction-family + - id: carlet-6-secondary-class-references + kind: citation-family location: >- - Carlet, secondary classes D_0, D, and C, pp. 90--91 + Carlet, further class D_0 consequences, pp. 90--91 source_claim: >- - For a permutation pi on V_(n/2), D_0 consists of - x dot pi(y)+delta_0(x) and has dual y dot pi^(-1)(x)+delta_0(y). - Class D consists of - x dot pi(y)+1_(E_1)(x)1_(E_2)(y) with pi(E_2)=E_1^perp. - Class C consists of x dot pi(y)+1_L(x) when every - pi^(-1)(a+L^perp) is an affine flat; under the same condition, - x dot pi(y)+1_L(x)+g(y) is bent whenever g restricts affinely to every - such flat. Carlet also records completion and six-variable consequences - for D_0. - statement_status: complete-source-specializations-with-cited-class-separation-claims + After giving the explicit D_0, D, and C constructions, Carlet records + cited consequences that D_0 lies outside the completed Maiorana--McFarland + and partial-spread classes and that its completed class covers all + six-variable bent functions. + statement_status: incomplete-cited-class-separation-claims formal_status: open declarations: [] references: [44, 53] first_release_scope: required-after-source-recovery fidelity_note: >- - The construction hypotheses and dual formula are explicit. Claims - that D_0 is outside completed M and PS classes and covers all six-variable - bent functions are retained as cited consequences, not inferred from the - generic switching theorem. + The explicit D_0, D, and C constructions and the D_0 dual formula have + been promoted as separate formalized items. This record retains only the + cited completed-class nonmembership and six-variable coverage claims. reuse_note: >- - The bentness constructions are direct specializations of the - Maiorana--McFarland and flat-switching nodes and should reuse their affine - flat indicators and dual laws. + Any recovered class-separation theorem should reuse the formalized D_0 + construction and future predicates for completed affine-equivalence classes. blocker: >- - No dedicated declarations instantiate Theorem 9 with these parameters, - and the completed-class nonmembership claims require formal affine-class - predicates not currently present. + The primary papers and formal affine-class predicates are required to + state the completed-class nonmembership and coverage claims faithfully. dependencies: - - carlet-6-maiorana-mcfarland - - carlet-6-theorem-9-flat-switching - - carlet-5-flat-indicator-walsh-nonlinearity + - carlet-6-class-d-zero - id: carlet-6-dobbertin-primary-class kind: construction-family @@ -2239,10 +2595,10 @@ source_recovery: location: >- Carlet, additional secondary constructions, pp. 92--94 source_claim: >- - Carlet records the normal extension of - Maiorana--McFarland type obtained by adjoining a y-indexed family of bent - functions, three explicit four-block families derived from Theorem 10, - and three Hou--Langevin consequences of Proposition 21, including the + After the separately promoted Maiorana--McFarland bent-family extension + and first four-block class-D_0 construction, Carlet gives two further + four-block quotient families derived from Theorem 10 and three + Hou--Langevin consequences of Proposition 21, including the degree-at-most-three derivative reindexing and a quadratic-form reindexing of x dot y+g(y). statement_status: mixed-complete-formulas-and-cited-examples @@ -2251,62 +2607,58 @@ source_recovery: references: [56, 78, 190, 194] first_release_scope: required-after-source-recovery fidelity_note: >- - The displayed construction formulas are complete, while the - additional examples in references [56,190,194] are only mentioned. - This record does not merge their distinct hypotheses into one theorem. + The two promoted formulas are now separate formalized items. The + remaining displayed quotient formulas are complete, while the additional + examples in references [56,190,194] are only mentioned. This record does + not merge their distinct hypotheses into one theorem. reuse_note: >- The complete displayed families are specializations of the slice construction or permutation reindexing and should be proved by those general combinators. blocker: >- - No public specialization declarations are associated, and the cited - example families require primary-source recovery. + The remaining quotient families require a reviewed finite-field division + convention, and the cited example families require primary-source + recovery. dependencies: - carlet-6-theorem-10-slice-construction - carlet-6-prop-21-permutation-reindexing - carlet-6-maiorana-mcfarland - - id: carlet-6-additional-decompositions - kind: theorem-family + - id: carlet-6-additional-decomposition-references + kind: citation-family location: >- Carlet, Section 6.4.3, p. 97 source_claim: >- - If an odd-variable function f has every derivative D_u f - balanced for nonzero u in a fixed hyperplane a^perp, then the restriction - of f to a^perp and its complementary coset is bent. For a bent f, the - four restrictions to the cosets of a codimension-two subspace have the - same sets of Walsh magnitudes; if its orthogonal complement is spanned by - a,b, all four restrictions are bent exactly when D_a D_b of the dual is - the constant one function. Carlet cites further decomposition results. - statement_status: complete-two-results-with-incomplete-further-family + After the two explicit decomposition consequences, Carlet cites further + results on decomposing bent functions without stating them. + statement_status: incomplete-cited-family formal_status: open declarations: [] - references: [41, 42, 100] + references: [42, 100] first_release_scope: required-after-source-recovery fidelity_note: >- - The two displayed consequences are complete. The phrase "more on - decomposing bent functions" contains no additional theorem statement and - remains unpromoted. + The balanced-hyperplane and codimension-two consequences have been + promoted as separate source-facing items. This record retains only the + unstated further family. reuse_note: >- - Both complete consequences should reuse the hyperplane-restriction, - dual, and second-derivative APIs. + Any recovered theorem should compose the existing decomposition, + restriction-spectrum, dual, and second-derivative results. blocker: >- - The codimension-two restriction spectrum and its iff criterion have no - associated declarations; the remaining cited family lacks statements. + The survey supplies no additional theorem statement; primary-source + recovery is required before another item can be promoted. dependencies: - - carlet-6-theorem-11-hyperplane-restrictions - - carlet-6-dual - - carlet-6-prop-24-second-order-characterization + - carlet-6-balanced-hyperplane-derivative-restrictions + - carlet-6-codimension-two-restrictions - id: carlet-6-additional-counting kind: counting-family location: >- Carlet, Section 6.5, pp. 97--98 source_claim: >- - Besides the exact Maiorana--McFarland count, Carlet gives - C(2^(n/2),2^(n/2-1)) for the PS_ap family, an affine-automorphism upper - estimate for the completed Maiorana--McFarland class, and states that an - efficient general lower bound remains open. He reports the approximate + Besides the separately promoted exact Maiorana--McFarland and PS_ap + counts, Carlet gives an affine-automorphism upper estimate for the + completed Maiorana--McFarland class and states that an efficient general + lower bound remains open. He reports the approximate exact counts B_6 approximately 2^32.3 and B_8 approximately 2^106.3, earlier and improved upper bounds for B_8, and an exponentially improved upper bound over the naive bound that divides it by approximately @@ -2317,12 +2669,13 @@ source_recovery: references: [81, 89, 125, 231, 232, 299] first_release_scope: required-after-source-recovery fidelity_note: >- - The PS_ap binomial count and the reported finite values are - explicit. The chapter gives only an approximate description of the [89] - upper bound and no efficient lower-bound theorem. + The PS_ap binomial count has been promoted as a separate formalized item. + The reported finite values are explicit, but the chapter gives only an + approximate description of the [89] upper bound and no efficient + lower-bound theorem. reuse_note: >- - The finite family counts should reuse the partial-spread and - Maiorana--McFarland parameter spaces; any global bound should reuse the + The remaining affine-completion estimate should reuse the + Maiorana--McFarland parameter space; any global bound should reuse the bent-function family and Reed--Muller degree count. blocker: >- The exact theorem behind reference [89], the exact integer values behind @@ -2331,7 +2684,6 @@ source_recovery: dependencies: - carlet-6-maiorana-mcfarland-count - carlet-6-naive-bent-count-bound - - carlet-6-partial-spread-construction - id: carlet-6-alternate-geometric-and-gps-translation kind: characterization-family diff --git a/AGENTS.md b/AGENTS.md index f597090..d74d918 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -28,8 +28,8 @@ matching Verso entry and production declaration. ## Current verified surface -The Blueprint baseline is 209 source-facing statement nodes: 206 formalized nodes associated with -1338 proved Lean declarations and 3 visibly open nodes, connected by 467 reviewed dependency +The Blueprint baseline is 222 source-facing statement nodes: 219 formalized nodes associated with +1418 proved Lean declarations and 3 visibly open nodes, connected by 493 reviewed dependency edges. - Chapter 2 contributes 41 formalized nodes, 174 declarations, and 56 incoming @@ -57,9 +57,14 @@ edges. and nonlinearity, the full restriction bound and its equality case, exact random nonnormality, covering-sequence consequences, quadratic trace representation, and the conditional character-sum/nonlinearity reduction. -- Chapter 6 contributes 57 formalized nodes, 361 declarations, and 163 incoming edges. It covers - bentness, duality, algebraic-degree bounds and Relation (47), primary and secondary - constructions, decompositions and counting, NNF, geometric and second-order characterizations, +- Chapter 6 contributes 70 formalized nodes, 441 declarations, and 189 incoming edges. It covers + bentness, its Hadamard-matrix, difference-set, and strongly regular Cayley-graph + characterizations, duality, + algebraic-degree bounds and Relation (47), primary and secondary constructions including + Classes D₀, D, and C, the Maiorana--McFarland bent-family extension and four-block + class-D₀ construction, hyperplane and codimension-two decompositions, the exact `PS_ap` count, + NNF, geometric and + second-order characterizations, hyper-bent functions, partially bent and plateaued superclasses, normal extensions, and the Kerdock field construction and parameters. The proof of Relation (47) includes the reusable McEliece--Ax character-sum divisibility theorem. diff --git a/CryptBoolean/Carlet/Chapter02/Foundations.lean b/CryptBoolean/Carlet/Chapter02/Foundations.lean index 9d88f1a..3734b26 100644 --- a/CryptBoolean/Carlet/Chapter02/Foundations.lean +++ b/CryptBoolean/Carlet/Chapter02/Foundations.lean @@ -56,6 +56,53 @@ theorem hammingWeight_eq_card_support (f : BooleanFunction n) : hammingWeight f = (support f).card := by exact FABL.hammingNorm_eq_card_f₂OneSupport f +/-- The natural-valued Hamming weight of a binary scalar. -/ +def f₂BitWeight (b : FABL.𝔽₂) : ℕ := + if b ≠ 0 then 1 else 0 + +/-- Hamming norm is the sum of the scalar binary weights. -/ +theorem hammingNorm_eq_sum_f₂BitWeight + {ι : Type*} [Fintype ι] (x : ι → FABL.𝔽₂) : + hammingNorm x = ∑ i, f₂BitWeight (x i) := by + simp [hammingNorm, f₂BitWeight, Finset.card_filter] + +/-- Hamming weight decomposes into the symmetric-difference weight and twice +the common-support weight. -/ +theorem hammingNorm_add_restrictSupport_identity + {ι : Type*} [Fintype ι] (x y : ι → FABL.𝔽₂) : + hammingNorm (x + y) + + 2 * hammingNorm (fun j : {i : ι // x i ≠ 0} ↦ y j.1) = + hammingNorm x + hammingNorm y := by + classical + have hrestricted : + (∑ i, if x i ≠ 0 then f₂BitWeight (y i) else 0) = + hammingNorm (fun j : {i : ι // x i ≠ 0} ↦ y j.1) := by + rw [hammingNorm_eq_sum_f₂BitWeight, ← Finset.sum_filter] + exact Finset.sum_subtype (Finset.univ.filter fun i ↦ x i ≠ 0) + (by simp) (fun i ↦ f₂BitWeight (y i)) + rw [hammingNorm_eq_sum_f₂BitWeight (x + y), + hammingNorm_eq_sum_f₂BitWeight x, hammingNorm_eq_sum_f₂BitWeight y, + ← hrestricted, Finset.mul_sum, + ← Finset.sum_add_distrib] + calc + ∑ i, (f₂BitWeight ((x + y) i) + + 2 * (if x i ≠ 0 then f₂BitWeight (y i) else 0)) = + ∑ i, (f₂BitWeight (x i) + f₂BitWeight (y i)) := by + apply Finset.sum_congr rfl + intro i _hi + by_cases hx : x i = 0 + · by_cases hy : y i = 0 + · simp [hx, hy, f₂BitWeight] + · have hyOne : y i = 1 := Fin.eq_one_of_ne_zero _ hy + simp [hx, hyOne, f₂BitWeight] + · have hxOne : x i = 1 := Fin.eq_one_of_ne_zero _ hx + by_cases hy : y i = 0 + · simp [hxOne, hy, f₂BitWeight] + · have hyOne : y i = 1 := Fin.eq_one_of_ne_zero _ hy + simp [hxOne, hyOne, f₂BitWeight] + _ = (∑ i, f₂BitWeight (x i)) + ∑ i, f₂BitWeight (y i) := + Finset.sum_add_distrib + /-- The binary cube has cardinality `2^n`. -/ theorem card_f₂Cube (n : ℕ) : Fintype.card (FABL.F₂Cube n) = 2 ^ n := by diff --git a/CryptBoolean/Carlet/Chapter04/FiveVariableMaximumNonlinearity.lean b/CryptBoolean/Carlet/Chapter04/FiveVariableMaximumNonlinearity.lean index 5720b03..d1d4a5d 100644 --- a/CryptBoolean/Carlet/Chapter04/FiveVariableMaximumNonlinearity.lean +++ b/CryptBoolean/Carlet/Chapter04/FiveVariableMaximumNonlinearity.lean @@ -29,13 +29,12 @@ private abbrev OneCoordinates {ι : Type*} (x : ι → FABL.𝔽₂) := private abbrev ZeroCoordinates {ι : Type*} (x : ι → FABL.𝔽₂) := {i : ι // x i = 0} -private def bitWeight (b : FABL.𝔽₂) : ℕ := - if b ≠ 0 then 1 else 0 +private abbrev bitWeight := f₂BitWeight private theorem hammingNorm_eq_sum_bitWeight {ι : Type*} [Fintype ι] (x : ι → FABL.𝔽₂) : hammingNorm x = ∑ i, bitWeight (x i) := by - simp [hammingNorm, bitWeight, Finset.card_filter] + exact hammingNorm_eq_sum_f₂BitWeight x private theorem card_oneCoordinates {ι : Type*} [Fintype ι] (x : ι → FABL.𝔽₂) : @@ -51,38 +50,12 @@ private theorem card_zeroCoordinates simp only [Finset.card_univ, not_ne_iff] at hpartition omega -private theorem bitWeight_add_intersection_identity (x y : FABL.𝔽₂) : - bitWeight (x + y) + 2 * (if x ≠ 0 then bitWeight y else 0) = - bitWeight x + bitWeight y := by - fin_cases x <;> fin_cases y <;> decide - -private theorem sum_ite_nonzero_eq_sum_oneCoordinates - {ι : Type*} [Fintype ι] (x y : ι → FABL.𝔽₂) : - (∑ i, if x i ≠ 0 then bitWeight (y i) else 0) = - ∑ j : OneCoordinates x, bitWeight (y j.1) := by - classical - rw [← Finset.sum_filter] - exact Finset.sum_subtype (Finset.univ.filter fun i ↦ x i ≠ 0) - (by simp) (fun i ↦ bitWeight (y i)) - private theorem hammingNorm_add_restrictOne_identity {ι : Type*} [Fintype ι] (x y : ι → FABL.𝔽₂) : hammingNorm (x + y) + 2 * hammingNorm (fun j : OneCoordinates x ↦ y j.1) = hammingNorm x + hammingNorm y := by - rw [hammingNorm_eq_sum_bitWeight, hammingNorm_eq_sum_bitWeight, - hammingNorm_eq_sum_bitWeight, hammingNorm_eq_sum_bitWeight, - ← sum_ite_nonzero_eq_sum_oneCoordinates x y, Finset.mul_sum, - ← Finset.sum_add_distrib] - calc - ∑ i, (bitWeight ((x + y) i) + - 2 * (if x i ≠ 0 then bitWeight (y i) else 0)) = - ∑ i, (bitWeight (x i) + bitWeight (y i)) := by - apply Finset.sum_congr rfl - intro i _hi - simpa using bitWeight_add_intersection_identity (x i) (y i) - _ = (∑ i, bitWeight (x i)) + ∑ i, bitWeight (y i) := - Finset.sum_add_distrib + exact hammingNorm_add_restrictSupport_identity x y private theorem bitWeight_add_one (x : FABL.𝔽₂) : bitWeight (x + 1) + bitWeight x = 1 := by diff --git a/CryptBoolean/Carlet/Chapter06.lean b/CryptBoolean/Carlet/Chapter06.lean index a6670e7..612ef12 100644 --- a/CryptBoolean/Carlet/Chapter06.lean +++ b/CryptBoolean/Carlet/Chapter06.lean @@ -5,7 +5,9 @@ Authors: Asher Yan with Codex -/ module +public import CryptBoolean.Carlet.Chapter06.AdditionalDecompositions public import CryptBoolean.Carlet.Chapter06.Bentness +public import CryptBoolean.Carlet.Chapter06.CayleyGraph public import CryptBoolean.Carlet.Chapter06.CompleteQuadratic public import CryptBoolean.Carlet.Chapter06.DegreeBounds public import CryptBoolean.Carlet.Chapter06.DegreeRelation @@ -19,6 +21,7 @@ public import CryptBoolean.Carlet.Chapter06.DualPoisson public import CryptBoolean.Carlet.Chapter06.FlatSwitching public import CryptBoolean.Carlet.Chapter06.FourierUncertainty public import CryptBoolean.Carlet.Chapter06.GeometricCharacterization +public import CryptBoolean.Carlet.Chapter06.HadamardDifferenceSet public import CryptBoolean.Carlet.Chapter06.HyperBent public import CryptBoolean.Carlet.Chapter06.HyperBentPartialSpread public import CryptBoolean.Carlet.Chapter06.HyperplaneRestriction @@ -27,6 +30,8 @@ public import CryptBoolean.Carlet.Chapter06.Kerdock public import CryptBoolean.Carlet.Chapter06.KerdockCoordinateIdentity public import CryptBoolean.Carlet.Chapter06.KerdockFieldConstruction public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarland +public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandBalance +public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandBentSubspace public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandCounting public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandGeneral public import CryptBoolean.Carlet.Chapter06.McElieceAx @@ -39,6 +44,7 @@ public import CryptBoolean.Carlet.Chapter06.PartialBentCounterexamples public import CryptBoolean.Carlet.Chapter06.PartiallyBent public import CryptBoolean.Carlet.Chapter06.PartialSpreads public import CryptBoolean.Carlet.Chapter06.PermutationReindex +public import CryptBoolean.Carlet.Chapter06.PSapCounting public import CryptBoolean.Carlet.Chapter06.Plateaued public import CryptBoolean.Carlet.Chapter06.PlateauedOrphan public import CryptBoolean.Carlet.Chapter06.PlateauedSecondOrder @@ -46,7 +52,10 @@ public import CryptBoolean.Carlet.Chapter06.PlateauedSupport public import CryptBoolean.Carlet.Chapter06.QuadraticBent public import CryptBoolean.Carlet.Chapter06.Rothaus public import CryptBoolean.Carlet.Chapter06.SecondOrderCharacterization +public import CryptBoolean.Carlet.Chapter06.SecondaryClasses +public import CryptBoolean.Carlet.Chapter06.SecondarySpecializations public import CryptBoolean.Carlet.Chapter06.SupportCode +public import CryptBoolean.Carlet.Chapter06.SupportCodeAlternatives public import CryptBoolean.Carlet.Chapter06.ThreeFunctionBent public import CryptBoolean.Carlet.Chapter06.ThreeFunctionIdentity public import CryptBoolean.Carlet.Chapter06.WalshCongruence diff --git a/CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean b/CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean new file mode 100644 index 0000000..f8b61a6 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/AdditionalDecompositions.lean @@ -0,0 +1,828 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter05.QuadraticNormalForm +public import CryptBoolean.Carlet.Chapter06.HyperplaneRestriction +public import CryptBoolean.Carlet.Chapter06.QuadraticBent +public import CryptBoolean.Carlet.Chapter06.SecondOrderCharacterization + +/-! +# Additional decompositions of bent functions + +Carlet Section 6.4.3: bent restrictions arising from balanced hyperplane +derivatives, and the spectra of restrictions to four codimension-two cosets. +-/ + +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {n : ℕ} + +private def standardHyperplaneDirection (u : FABL.F₂Cube n) : + FABL.F₂Cube (n + 1) := + Fin.append u (singletonF₂Cube 0) + +private theorem autocorrelation_standardHyperplaneDirection + (f : BooleanFunction (n + 1)) (u : FABL.F₂Cube n) : + autocorrelation f (standardHyperplaneDirection u) = + autocorrelation (firstBlockSlice f (singletonF₂Cube 0)) u + + autocorrelation (firstBlockSlice f (singletonF₂Cube 1)) u := by + classical + rw [autocorrelation] + calc + ∑ z : FABL.F₂Cube (n + 1), + realSignView + (FABL.booleanDerivative f (standardHyperplaneDirection u)) z = + ∑ p : FABL.F₂Cube n × FABL.F₂Cube 1, + realSignView + (FABL.booleanDerivative f (standardHyperplaneDirection u)) + (Fin.append p.1 p.2) := by + exact (Fintype.sum_equiv (Fin.appendEquiv n 1) + (fun p ↦ realSignView + (FABL.booleanDerivative f (standardHyperplaneDirection u)) + (Fin.append p.1 p.2)) + (fun z ↦ realSignView + (FABL.booleanDerivative f (standardHyperplaneDirection u)) z) + (fun _ ↦ rfl)).symm + _ = ∑ y : FABL.F₂Cube 1, ∑ x : FABL.F₂Cube n, + realSignView (FABL.booleanDerivative (firstBlockSlice f y) u) x := by + rw [Fintype.sum_prod_type, Finset.sum_comm] + apply Finset.sum_congr rfl + intro y _hy + apply Finset.sum_congr rfl + intro x _hx + simp only [realSignView_booleanDerivative, standardHyperplaneDirection] + rw [← finAppend_add] + rw [show singletonF₂Cube 0 = 0 by rfl, add_zero] + simp [realSignView, FABL.realSignEncodedFunction, + FABL.signEncodedFunction, firstBlockSlice] + _ = autocorrelation (firstBlockSlice f (singletonF₂Cube 0)) u + + autocorrelation (firstBlockSlice f (singletonF₂Cube 1)) u := by + rw [sum_singletonF₂Cube] + rfl + +private theorem sq_add_sq_two_pow (k : ℕ) (x y : ℤ) + (h : x ^ 2 + y ^ 2 = (2 : ℤ) ^ (2 * k + 1)) : + x.natAbs = 2 ^ k ∧ y.natAbs = 2 ^ k := by + induction k generalizing x y with + | zero => + norm_num at h ⊢ + have hxLower : -1 ≤ x := by nlinarith [sq_nonneg (x + 1)] + have hxUpper : x ≤ 1 := by nlinarith [sq_nonneg (x - 1)] + have hyLower : -1 ≤ y := by nlinarith [sq_nonneg (y + 1)] + have hyUpper : y ≤ 1 := by nlinarith [sq_nonneg (y - 1)] + interval_cases x <;> interval_cases y + all_goals norm_num at h + all_goals norm_num + | succ k ih => + have hrightEven : Even ((2 : ℤ) ^ (2 * (k + 1) + 1)) := by + exact Even.pow_of_ne_zero (by decide) (by omega) + rcases Int.even_or_odd x with hx | hx + · rcases Int.even_or_odd y with hy | hy + · obtain ⟨x', rfl⟩ := hx + obtain ⟨y', rfl⟩ := hy + have h' : x' ^ 2 + y' ^ 2 = (2 : ℤ) ^ (2 * k + 1) := by + rw [show 2 * (k + 1) + 1 = (2 * k + 1) + 2 by omega, + pow_add] at h + norm_num at h ⊢ + nlinarith + obtain ⟨hx', hy'⟩ := ih x' y' h' + constructor + · rw [← two_mul x', Int.natAbs_mul, hx', pow_succ] + exact Nat.mul_comm _ _ + · rw [← two_mul y', Int.natAbs_mul, hy', pow_succ] + exact Nat.mul_comm _ _ + · have hleftOdd : Odd (x ^ 2 + y ^ 2) := + hx.pow_of_ne_zero (by decide) |>.add_odd hy.pow + exact (Int.not_odd_iff_even.mpr (h ▸ hrightEven) hleftOdd).elim + · rcases Int.even_or_odd y with hy | hy + · have hleftOdd : Odd (x ^ 2 + y ^ 2) := + hx.pow.add_even (hy.pow_of_ne_zero (by decide)) + exact (Int.not_odd_iff_even.mpr (h ▸ hrightEven) hleftOdd).elim + · have hxEight : 8 ∣ x ^ 2 - 1 := + Int.eight_dvd_sq_sub_one_of_odd hx + have hyEight : 8 ∣ y ^ 2 - 1 := + Int.eight_dvd_sq_sub_one_of_odd hy + have hleftEight : 8 ∣ x ^ 2 + y ^ 2 - 2 := by + rw [show x ^ 2 + y ^ 2 - 2 = + (x ^ 2 - 1) + (y ^ 2 - 1) by ring] + exact dvd_add hxEight hyEight + have hrightEight : 8 ∣ (2 : ℤ) ^ (2 * (k + 1) + 1) := by + rw [show 2 * (k + 1) + 1 = 3 + 2 * k by omega, pow_add] + norm_num + have : 8 ∣ (2 : ℤ) := by + rw [h] at hleftEight + simpa using dvd_sub hrightEight hleftEight + norm_num at this + +private theorem isBent_firstBlockSlices_of_balanced_hyperplane_derivatives + (k : ℕ) (f : BooleanFunction (2 * k + 1)) + (hbalanced : ∀ u : FABL.F₂Cube (2 * k), u ≠ 0 → + IsBalanced + (FABL.booleanDerivative f (standardHyperplaneDirection u))) : + ∀ b : FABL.𝔽₂, + IsBent (firstBlockSlice f (singletonF₂Cube b)) := by + classical + let h₀ := firstBlockSlice f (singletonF₂Cube 0) + let h₁ := firstBlockSlice f (singletonF₂Cube 1) + have hsumZero (u : FABL.F₂Cube (2 * k)) (hu : u ≠ 0) : + autocorrelation h₀ u + autocorrelation h₁ u = 0 := by + rw [← autocorrelation_standardHyperplaneDirection] + exact (isBalanced_booleanDerivative_iff_autocorrelation_eq_zero + f (standardHyperplaneDirection u)).mp (hbalanced u hu) + have hmagnitudes (a : FABL.F₂Cube (2 * k)) : + (walshTransform h₀ a).natAbs = 2 ^ k ∧ + (walshTransform h₁ a).natAbs = 2 ^ k := by + have hsquaresReal : + (walshTransform h₀ a : ℝ) ^ 2 + + (walshTransform h₁ a : ℝ) ^ 2 = + (2 : ℝ) ^ (2 * k + 1) := by + rw [← rawFourierTransform_autocorrelation, + ← rawFourierTransform_autocorrelation, + rawFourierTransform, rawFourierTransform] + rw [← Finset.sum_add_distrib] + rw [Finset.sum_eq_single 0] + · have hcharacter : FABL.vectorWalshCharacter a 0 = 1 := by simp + rw [hcharacter, autocorrelation_zero, autocorrelation_zero, + mul_one] + rw [pow_succ] + ring + · intro u _hu hu0 + rw [← add_mul, hsumZero u hu0, zero_mul] + · simp + have hsquaresInt : + walshTransform h₀ a ^ 2 + walshTransform h₁ a ^ 2 = + (2 : ℤ) ^ (2 * k + 1) := by + exact_mod_cast hsquaresReal + exact sq_add_sq_two_pow k _ _ hsquaresInt + have hbent₀ : IsBent h₀ := + (isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half h₀).2 (by + intro a + simpa using (hmagnitudes a).1) + have hbent₁ : IsBent h₁ := + (isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half h₁).2 (by + intro a + simpa using (hmagnitudes a).2) + intro b + fin_cases b + · exact hbent₀ + · exact hbent₁ + +private def linearHyperplaneDirection (k : ℕ) + (L : FABL.F₂Cube (2 * k + 1) ≃ₗ[FABL.𝔽₂] + FABL.F₂Cube (2 * k + 1)) + (u : FABL.F₂Cube (2 * k)) : FABL.F₂Cube (2 * k + 1) := + L (standardHyperplaneDirection u) + +/-- If every nonzero derivative in a hyperplane is balanced, both coset +restrictions are bent. -/ +theorem isBent_linearHyperplaneRestriction_of_balanced_derivatives + (k : ℕ) (f : BooleanFunction (2 * k + 1)) + (L : FABL.F₂Cube (2 * k + 1) ≃ₗ[FABL.𝔽₂] + FABL.F₂Cube (2 * k + 1)) + (hbalanced : ∀ u : FABL.F₂Cube (2 * k), u ≠ 0 → + IsBalanced + (FABL.booleanDerivative f + (L (Fin.append u (singletonF₂Cube 0))))) + (b : FABL.𝔽₂) : + IsBent (linearHyperplaneRestriction f L b) := by + apply isBent_firstBlockSlices_of_balanced_hyperplane_derivatives + k (f ∘ L) _ b + intro u hu + apply (isBalanced_booleanDerivative_iff_autocorrelation_eq_zero _ _).2 + have hlinear : + L.toAffineEquiv.linear (standardHyperplaneDirection u) = + L (standardHyperplaneDirection u) := by + rfl + have hauto : + autocorrelation (f ∘ L) (standardHyperplaneDirection u) = + autocorrelation f (L (standardHyperplaneDirection u)) := by + simpa [hlinear] using autocorrelation_comp_affineEquiv + f L.toAffineEquiv (standardHyperplaneDirection u) + rw [hauto] + apply (isBalanced_booleanDerivative_iff_autocorrelation_eq_zero _ _).1 + simpa [linearHyperplaneDirection, standardHyperplaneDirection] using + hbalanced u hu + +private def f₂CubeTwoBasis (i : Fin 2) : FABL.F₂Cube 2 := + Pi.single i 1 + +private theorem f₂CubeTwoBasis_apply (i j : Fin 2) : + f₂CubeTwoBasis i j = if i = j then 1 else 0 := by + classical + simp [f₂CubeTwoBasis, Pi.single_apply, eq_comm] + +private theorem secondBooleanDerivative_eq_quadraticPolarKernel + (f : BooleanFunction n) + (hdegree : FABL.functionAlgebraicDegree f ≤ 2) + (a e x : FABL.F₂Cube n) : + secondBooleanDerivative f a e x = quadraticPolarKernel f a e := by + have hderivativeDegree : + FABL.functionAlgebraicDegree (FABL.booleanDerivative f e) ≤ 1 := + (FABL.functionAlgebraicDegree_booleanDerivative_le f e).trans (by omega) + obtain ⟨d, u, hu⟩ := + FABL.exists_affineFunction_of_functionAlgebraicDegree_le_one + (FABL.booleanDerivative f e) hderivativeDegree + rw [secondBooleanDerivative, hu, FABL.booleanDerivative, + FABL.affineFunction] + rw [quadraticPolarKernel_comm, + quadraticPolarKernel_eq_dotProduct_of_derivative_eq_affine + f e a d u hu] + simp only [FABL.affineFunction, FABL.f₂DotProduct] + rw [dotProduct_add] + abel_nf + simp [two_smul, ZModModule.add_self] + +private theorem f₂CubeTwo_eq_basis_sum (x : FABL.F₂Cube 2) : + x = x 0 • f₂CubeTwoBasis 0 + x 1 • f₂CubeTwoBasis 1 := by + simpa [f₂CubeTwoBasis, Fin.sum_univ_two] using + (pi_eq_sum_univ' x) + +private theorem quadraticRadical_eq_bot_iff_basis_cross_eq_one + (f : BooleanFunction 2) + (hdegree : FABL.functionAlgebraicDegree f ≤ 2) : + quadraticRadical f hdegree = ⊥ ↔ + quadraticPolarKernel f (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 1) = 1 := by + let e₀ := f₂CubeTwoBasis 0 + let e₁ := f₂CubeTwoBasis 1 + have h₀₀ : quadraticPolarKernel f e₀ e₀ = 0 := by + simpa [e₀] using quadraticPolar_isAlt f hdegree e₀ + have h₁₁ : quadraticPolarKernel f e₁ e₁ = 0 := by + simpa [e₁] using quadraticPolar_isAlt f hdegree e₁ + have h₀₀' : quadraticPolarKernel f (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 0) = 0 := by + simpa [e₀] using h₀₀ + have h₁₁' : quadraticPolarKernel f (f₂CubeTwoBasis 1) + (f₂CubeTwoBasis 1) = 0 := by + simpa [e₁] using h₁₁ + constructor + · intro hradical + have hne : quadraticPolarKernel f (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 1) ≠ 0 := by + intro hcross + have hcross' : quadraticPolarKernel f e₀ e₁ = 0 := by + simpa [e₀, e₁] using hcross + have he₀ : e₀ ∈ quadraticRadical f hdegree := by + rw [mem_quadraticRadical_iff] + intro b + rw [f₂CubeTwo_eq_basis_sum b, + quadraticPolarKernel_add_right f hdegree, + quadraticPolarKernel_smul_right f hdegree, + quadraticPolarKernel_smul_right f hdegree] + change b 0 • quadraticPolarKernel f e₀ e₀ + + b 1 • quadraticPolarKernel f e₀ e₁ = 0 + rw [h₀₀, hcross'] + simp + rw [hradical] at he₀ + have he₀Zero : e₀ = 0 := by simpa using he₀ + have := congrFun he₀Zero 0 + simp [e₀, f₂CubeTwoBasis] at this + exact Fin.eq_one_of_ne_zero _ hne + · intro hcross + apply le_antisymm + · intro a ha + have ha₀ := (mem_quadraticRadical_iff f hdegree a).mp ha e₀ + have ha₁ := (mem_quadraticRadical_iff f hdegree a).mp ha e₁ + have h₁₀ : quadraticPolarKernel f e₁ e₀ = 1 := by + rw [quadraticPolarKernel_comm, hcross] + have h₁₀' : quadraticPolarKernel f (f₂CubeTwoBasis 1) + (f₂CubeTwoBasis 0) = 1 := by + simpa [e₀, e₁] using h₁₀ + have hvalue₀ : quadraticPolarKernel f a e₀ = a 1 := by + change quadraticPolarKernel f a (f₂CubeTwoBasis 0) = a 1 + rw [f₂CubeTwo_eq_basis_sum a, + quadraticPolarKernel_add_left f hdegree, + quadraticPolarKernel_smul_left f hdegree, + quadraticPolarKernel_smul_left f hdegree] + simp only [Pi.add_apply, Pi.smul_apply] + simp only [f₂CubeTwoBasis_apply] + rw [h₀₀', h₁₀'] + simp + have hvalue₁ : quadraticPolarKernel f a e₁ = a 0 := by + change quadraticPolarKernel f a (f₂CubeTwoBasis 1) = a 0 + rw [f₂CubeTwo_eq_basis_sum a, + quadraticPolarKernel_add_left f hdegree, + quadraticPolarKernel_smul_left f hdegree, + quadraticPolarKernel_smul_left f hdegree] + simp only [Pi.add_apply, Pi.smul_apply] + simp only [f₂CubeTwoBasis_apply] + rw [hcross, h₁₁'] + simp + rw [hvalue₀] at ha₀ + rw [hvalue₁] at ha₁ + have haZero : a = 0 := by + funext i + fin_cases i + · exact ha₁ + · exact ha₀ + simp [haZero] + · exact bot_le + +private theorem isBent_two_iff_secondBooleanDerivative_basis_eq_one + (f : BooleanFunction 2) : + IsBent f ↔ + secondBooleanDerivative f (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 1) = 1 := by + let hdegree := FABL.functionAlgebraicDegree_le_dimension f + rw [isBent_iff_quadraticRadical_eq_bot f hdegree, + quadraticRadical_eq_bot_iff_basis_cross_eq_one f hdegree] + constructor + · intro hcross + funext x + rw [secondBooleanDerivative_eq_quadraticPolarKernel f hdegree, + hcross] + rfl + · intro hsecond + have hvalue := congrFun hsecond 0 + simpa [secondBooleanDerivative_eq_quadraticPolarKernel f hdegree] + using hvalue + +/-- The Walsh coefficient of a codimension-two restriction is the two-bit +Walsh coefficient of the corresponding dual slice, with exact raw scaling. -/ +theorem four_mul_walshTransform_firstBlockSlice_eq + (f : BooleanFunction (n + 2)) (hf : IsBent f) + (a : FABL.F₂Cube n) (y : FABL.F₂Cube 2) : + (4 : ℝ) * (walshTransform (firstBlockSlice f y) a : ℝ) = + (2 : ℝ) ^ ((n + 2) / 2) * + (walshTransform (secondBlockSlice (bentDual f) a) y : ℝ) := by + let φ : FABL.F₂Cube 2 → ℝ := + fun t ↦ (walshTransform (firstBlockSlice f t) a : ℝ) + have hambient (t : FABL.F₂Cube 2) : + rawFourierTransform φ t = + (2 : ℝ) ^ ((n + 2) / 2) * + realSignView (secondBlockSlice (bentDual f) a) t := by + rw [← walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh] + have hdual := congrArg (fun z : ℤ ↦ (z : ℝ)) + (walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual + f hf (Fin.append a t)) + have hsign : + (bitSignInt (bentDual f (Fin.append a t)) : ℝ) = + realSignView (secondBlockSlice (bentDual f) a) t := by + rw [bitSignInt_cast] + simp [secondBlockSlice, realSignView, FABL.realSignEncodedFunction, + FABL.signEncodedFunction, FABL.signValue_signEncode_eq_binarySign] + simpa only [Int.cast_mul, Int.cast_pow, Int.cast_ofNat, hsign] using hdual + calc + (4 : ℝ) * (walshTransform (firstBlockSlice f y) a : ℝ) = + rawFourierTransform (rawFourierTransform φ) y := by + rw [rawFourierTransform_involution] + norm_num [φ] + _ = rawFourierTransform + (fun t ↦ (2 : ℝ) ^ ((n + 2) / 2) * + realSignView (secondBlockSlice (bentDual f) a) t) y := by + congr 1 + funext t + exact hambient t + _ = (2 : ℝ) ^ ((n + 2) / 2) * + (walshTransform (secondBlockSlice (bentDual f) a) y : ℝ) := by + exact rawFourierTransform_const_mul_realSignView + (secondBlockSlice (bentDual f) a) _ y + +private theorem two_mul_walshTransform_firstBlockSlice_eq + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (a : FABL.F₂Cube n) (y : FABL.F₂Cube 2) : + 2 * walshTransform (firstBlockSlice f y) a = + (2 ^ (n / 2) : ℤ) * + walshTransform (secondBlockSlice (bentDual f) a) y := by + have hhalf : (n + 2) / 2 = n / 2 + 1 := by + rcases hn with ⟨k, hk⟩ + omega + have hreal := four_mul_walshTransform_firstBlockSlice_eq f hf a y + have hint : + (4 : ℤ) * walshTransform (firstBlockSlice f y) a = + (2 : ℤ) ^ ((n + 2) / 2) * + walshTransform (secondBlockSlice (bentDual f) a) y := by + exact_mod_cast hreal + rw [hhalf, pow_succ] at hint + apply mul_left_cancel₀ (by norm_num : (2 : ℤ) ≠ 0) + calc + 2 * (2 * walshTransform (firstBlockSlice f y) a) = + 4 * walshTransform (firstBlockSlice f y) a := by ring + _ = (2 ^ (n / 2) * 2) * + walshTransform (secondBlockSlice (bentDual f) a) y := hint + _ = 2 * ((2 ^ (n / 2) : ℤ) * + walshTransform (secondBlockSlice (bentDual f) a) y) := by ring + +private theorem two_mul_natAbs_walshTransform_firstBlockSlice_eq + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (a : FABL.F₂Cube n) (y : FABL.F₂Cube 2) : + 2 * (walshTransform (firstBlockSlice f y) a).natAbs = + 2 ^ (n / 2) * + (walshTransform (secondBlockSlice (bentDual f) a) y).natAbs := by + have h := congrArg Int.natAbs + (two_mul_walshTransform_firstBlockSlice_eq f hf hn a y) + norm_num [Int.natAbs_mul, Int.natAbs_pow] at h + exact h + +private theorem forall_isBent_firstBlockSlice_iff_secondBlockSlice_bentDual + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) : + (∀ y, IsBent (firstBlockSlice f y)) ↔ + ∀ a, IsBent (secondBlockSlice (bentDual f) a) := by + constructor + · intro hslices a + apply (isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half + (secondBlockSlice (bentDual f) a)).2 + intro y + have hscale := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn a y + rw [natAbs_walshTransform_eq_two_pow_half_of_isBent + (firstBlockSlice f y) (hslices y) a] at hscale + rw [show 2 * 2 ^ (n / 2) = 2 ^ (n / 2) * 2 by omega] at hscale + norm_num + exact (Nat.mul_left_cancel (Nat.two_pow_pos _) hscale).symm + · intro hdualSlices y + apply (isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half + (firstBlockSlice f y)).2 + intro a + have hscale := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn a y + rw [natAbs_walshTransform_eq_two_pow_half_of_isBent + (secondBlockSlice (bentDual f) a) (hdualSlices a) y] at hscale + norm_num at hscale + rw [Nat.mul_comm (2 ^ (n / 2)) 2] at hscale + exact Nat.mul_left_cancel (by omega) hscale + +private theorem secondBooleanDerivative_secondBlockSlice + (f : BooleanFunction (n + 2)) (a : FABL.F₂Cube n) + (u v y : FABL.F₂Cube 2) : + secondBooleanDerivative (secondBlockSlice f a) u v y = + secondBooleanDerivative f (Fin.append 0 u) (Fin.append 0 v) + (Fin.append a y) := by + rw [secondBooleanDerivative_apply, secondBooleanDerivative_apply] + simp only [secondBlockSlice] + have hyu : Fin.append a y + Fin.append 0 u = + Fin.append a (y + u) := by + rw [← finAppend_add] + simp + have hyv : Fin.append a y + Fin.append 0 v = + Fin.append a (y + v) := by + rw [← finAppend_add] + simp + have hyuv : Fin.append a y + Fin.append 0 u + Fin.append 0 v = + Fin.append a (y + u + v) := by + calc + Fin.append a y + Fin.append 0 u + Fin.append 0 v = + Fin.append a (y + u) + Fin.append 0 v := by rw [hyu] + _ = Fin.append (a + 0) (y + u + v) := by + rw [finAppend_add] + _ = Fin.append a (y + u + v) := by simp + rw [hyuv, hyu, hyv] + +/-- The four codimension-two coordinate restrictions of a bent function are +bent exactly when the dual has constant second derivative one in the two +orthogonal coordinate directions. -/ +theorem isBent_firstBlockSlices_iff_bentDual_secondDerivative_eq_one + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) : + (∀ y, IsBent (firstBlockSlice f y)) ↔ + secondBooleanDerivative (bentDual f) + (Fin.append 0 (Pi.single 0 1)) + (Fin.append 0 (Pi.single 1 1)) = 1 := by + rw [forall_isBent_firstBlockSlice_iff_secondBlockSlice_bentDual + f hf hn] + constructor + · intro hslices + funext z + let a := ((Fin.appendEquiv n 2).symm z).1 + let y := ((Fin.appendEquiv n 2).symm z).2 + have hz : Fin.append a y = z := + (Fin.appendEquiv n 2).apply_symm_apply z + rw [← hz] + change secondBooleanDerivative (bentDual f) + (Fin.append 0 (f₂CubeTwoBasis 0)) + (Fin.append 0 (f₂CubeTwoBasis 1)) (Fin.append a y) = _ + rw [← secondBooleanDerivative_secondBlockSlice] + have hsecond := + (isBent_two_iff_secondBooleanDerivative_basis_eq_one + (secondBlockSlice (bentDual f) a)).1 (hslices a) + simpa [f₂CubeTwoBasis] using congrFun hsecond y + · intro hsecond a + apply (isBent_two_iff_secondBooleanDerivative_basis_eq_one + (secondBlockSlice (bentDual f) a)).2 + funext y + rw [secondBooleanDerivative_secondBlockSlice] + have hvalue := congrFun hsecond (Fin.append a y) + simpa [f₂CubeTwoBasis] using hvalue + +private theorem twoVariableWalshMagnitudeProfile (g : BooleanFunction 2) : + (∀ y, (walshTransform g y).natAbs = 2) ∨ + ∃ u, ∀ y, (walshTransform g y).natAbs = if y = u then 4 else 0 := by + let hdegree := FABL.functionAlgebraicDegree_le_dimension g + by_cases hg : IsBent g + · left + intro y + simpa using natAbs_walshTransform_eq_two_pow_half_of_isBent g hg y + · right + have hcrossNe : quadraticPolarKernel g (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 1) ≠ 1 := by + intro hcross + apply hg + exact (isBent_iff_quadraticRadical_eq_bot g hdegree).2 + ((quadraticRadical_eq_bot_iff_basis_cross_eq_one + g hdegree).2 hcross) + have hcross : quadraticPolarKernel g (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 1) = 0 := by + by_contra hne + exact hcrossNe (Fin.eq_one_of_ne_zero _ hne) + have hdiag₀ : quadraticPolarKernel g (f₂CubeTwoBasis 0) + (f₂CubeTwoBasis 0) = 0 := by + simpa using quadraticPolar_isAlt g hdegree (f₂CubeTwoBasis 0) + have hdiag₁ : quadraticPolarKernel g (f₂CubeTwoBasis 1) + (f₂CubeTwoBasis 1) = 0 := by + simpa using quadraticPolar_isAlt g hdegree (f₂CubeTwoBasis 1) + have hpolar : ∀ x y, quadraticPolarKernel g x y = 0 := by + intro x y + have h₀y : quadraticPolarKernel g (f₂CubeTwoBasis 0) y = 0 := by + rw [f₂CubeTwo_eq_basis_sum y, + quadraticPolarKernel_add_right g hdegree, + quadraticPolarKernel_smul_right g hdegree, + quadraticPolarKernel_smul_right g hdegree, + hdiag₀, hcross] + simp + have h₁y : quadraticPolarKernel g (f₂CubeTwoBasis 1) y = 0 := by + rw [f₂CubeTwo_eq_basis_sum y, + quadraticPolarKernel_add_right g hdegree, + quadraticPolarKernel_smul_right g hdegree, + quadraticPolarKernel_smul_right g hdegree, + quadraticPolarKernel_comm g (f₂CubeTwoBasis 1) + (f₂CubeTwoBasis 0), hcross, + hdiag₁] + simp + rw [f₂CubeTwo_eq_basis_sum x, + quadraticPolarKernel_add_left g hdegree, + quadraticPolarKernel_smul_left g hdegree, + quadraticPolarKernel_smul_left g hdegree, h₀y, h₁y] + simp + obtain ⟨c, u, rfl⟩ := + exists_affineFunction_of_quadraticPolarKernel_eq_zero g hpolar + refine ⟨u, fun y ↦ ?_⟩ + rw [walshTransform_affineFunction] + by_cases hy : y = u + · subst y + simp only [if_pos, Int.natAbs_mul, Int.natAbs_pow] + rw [bitSignInt_eq_if_one] + split <;> norm_num + · simp [hy] + +private theorem sum_sq_walshTransform_secondBlockSlice_bentDual + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (y : FABL.F₂Cube 2) : + (∑ a : FABL.F₂Cube n, + (walshTransform (secondBlockSlice (bentDual f) a) y : ℝ) ^ 2) = + 4 * (2 : ℝ) ^ n := by + have hhalf : (n + 2) / 2 = n / 2 + 1 := by + rcases hn with ⟨k, hk⟩ + omega + have hfactor : ((2 : ℝ) ^ ((n + 2) / 2)) ^ 2 = + 4 * (2 : ℝ) ^ n := by + rw [hhalf, pow_succ] + calc + ((2 : ℝ) ^ (n / 2) * 2) ^ 2 = + 4 * (((2 : ℝ) ^ (n / 2)) ^ 2) := by ring + _ = 4 * (2 : ℝ) ^ (2 * (n / 2)) := by + rw [show ((2 : ℝ) ^ (n / 2)) ^ 2 = + (2 : ℝ) ^ (2 * (n / 2)) by + rw [mul_comm, pow_mul]] + _ = 4 * (2 : ℝ) ^ n := by + congr 2 + rcases hn with ⟨k, hk⟩ + omega + have hscaled : + 16 * ∑ a : FABL.F₂Cube n, + (walshTransform (firstBlockSlice f y) a : ℝ) ^ 2 = + ((2 : ℝ) ^ ((n + 2) / 2)) ^ 2 * + ∑ a : FABL.F₂Cube n, + (walshTransform + (secondBlockSlice (bentDual f) a) y : ℝ) ^ 2 := by + rw [Finset.mul_sum, Finset.mul_sum] + apply Finset.sum_congr rfl + intro a _ha + have hpoint := + four_mul_walshTransform_firstBlockSlice_eq f hf a y + calc + 16 * (walshTransform (firstBlockSlice f y) a : ℝ) ^ 2 = + (4 * (walshTransform (firstBlockSlice f y) a : ℝ)) ^ 2 := by + ring + _ = ((2 : ℝ) ^ ((n + 2) / 2) * + (walshTransform + (secondBlockSlice (bentDual f) a) y : ℝ)) ^ 2 := by + rw [hpoint] + _ = ((2 : ℝ) ^ ((n + 2) / 2)) ^ 2 * + (walshTransform + (secondBlockSlice (bentDual f) a) y : ℝ) ^ 2 := by ring + rw [sum_walshTransform_sq_eq_two_pow_sq, hfactor] at hscaled + apply mul_left_cancel₀ (by positivity : 4 * (2 : ℝ) ^ n ≠ 0) + calc + (4 * (2 : ℝ) ^ n) * + ∑ a : FABL.F₂Cube n, + (walshTransform + (secondBlockSlice (bentDual f) a) y : ℝ) ^ 2 = + 16 * ((2 : ℝ) ^ n) ^ 2 := hscaled.symm + _ = (4 * (2 : ℝ) ^ n) * (4 * (2 : ℝ) ^ n) := by ring + +private theorem intCast_sq_eq_natAbsCast_sq (z : ℤ) : + (z : ℝ) ^ 2 = (z.natAbs : ℝ) ^ 2 := by + calc + (z : ℝ) ^ 2 = |(z : ℝ)| ^ 2 := (sq_abs _).symm + _ = (z.natAbs : ℝ) ^ 2 := by + rw [← Int.cast_abs, ← Nat.cast_natAbs] + +private theorem exists_secondBlockSlice_bentDual_walshMagnitude_four + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (a : FABL.F₂Cube n) + (haffine : ∃ u, ∀ y, + (walshTransform (secondBlockSlice (bentDual f) a) y).natAbs = + if y = u then 4 else 0) + (z : FABL.F₂Cube 2) : + ∃ b, (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs = 4 := by + classical + by_contra hnone + push Not at hnone + obtain ⟨u, hu⟩ := haffine + have haZero : + (walshTransform (secondBlockSlice (bentDual f) a) z).natAbs = 0 := by + rw [hu] + by_cases hzu : z = u + · have hzFour := hu z + rw [if_pos hzu] at hzFour + exact (hnone a hzFour).elim + · rw [if_neg hzu] + have hstrict : + (∑ b : FABL.F₂Cube n, + (walshTransform + (secondBlockSlice (bentDual f) b) z : ℝ) ^ 2) < + ∑ _b : FABL.F₂Cube n, (4 : ℝ) := by + apply Finset.sum_lt_sum + · intro b _hb + rcases twoVariableWalshMagnitudeProfile + (secondBlockSlice (bentDual f) b) with hbent | ⟨v, hv⟩ + · rw [intCast_sq_eq_natAbsCast_sq, hbent] + norm_num + · have hbZero : + (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs = 0 := by + rw [hv] + by_cases hzv : z = v + · have hzFour := hv z + rw [if_pos hzv] at hzFour + exact (hnone b hzFour).elim + · rw [if_neg hzv] + rw [intCast_sq_eq_natAbsCast_sq, hbZero] + norm_num + · refine ⟨a, Finset.mem_univ a, ?_⟩ + rw [intCast_sq_eq_natAbsCast_sq, haZero] + norm_num + rw [sum_sq_walshTransform_secondBlockSlice_bentDual f hf hn z, + Finset.sum_const, Finset.card_univ, card_f₂Cube, nsmul_eq_mul] at hstrict + norm_num only [Nat.cast_pow, Nat.cast_ofNat] at hstrict + nlinarith + +private theorem exists_secondBlockSlice_bentDual_walshMagnitude_zero + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (a : FABL.F₂Cube n) + (haffine : ∃ u, ∀ y, + (walshTransform (secondBlockSlice (bentDual f) a) y).natAbs = + if y = u then 4 else 0) + (z : FABL.F₂Cube 2) : + ∃ b, (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs = 0 := by + classical + by_contra hnone + push Not at hnone + obtain ⟨u, hu⟩ := haffine + have haFour : + (walshTransform (secondBlockSlice (bentDual f) a) z).natAbs = 4 := by + rw [hu] + by_cases hzu : z = u + · rw [if_pos hzu] + · have hzZero := hu z + rw [if_neg hzu] at hzZero + exact (hnone a hzZero).elim + have hstrict : + (∑ _b : FABL.F₂Cube n, (4 : ℝ)) < + ∑ b : FABL.F₂Cube n, + (walshTransform + (secondBlockSlice (bentDual f) b) z : ℝ) ^ 2 := by + apply Finset.sum_lt_sum + · intro b _hb + rcases twoVariableWalshMagnitudeProfile + (secondBlockSlice (bentDual f) b) with hbent | ⟨v, hv⟩ + · rw [intCast_sq_eq_natAbsCast_sq, hbent] + norm_num + · have hbFour : + (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs = 4 := by + rw [hv] + by_cases hzv : z = v + · rw [if_pos hzv] + · have hzZero := hv z + rw [if_neg hzv] at hzZero + exact (hnone b hzZero).elim + rw [intCast_sq_eq_natAbsCast_sq, hbFour] + norm_num + · refine ⟨a, Finset.mem_univ a, ?_⟩ + rw [intCast_sq_eq_natAbsCast_sq, haFour] + norm_num + rw [sum_sq_walshTransform_secondBlockSlice_bentDual f hf hn z, + Finset.sum_const, Finset.card_univ, card_f₂Cube, nsmul_eq_mul] at hstrict + norm_num only [Nat.cast_pow, Nat.cast_ofNat] at hstrict + nlinarith + +private theorem exists_secondBlockSlice_bentDual_same_walshMagnitude + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (a : FABL.F₂Cube n) (y z : FABL.F₂Cube 2) : + ∃ b, (walshTransform + (secondBlockSlice (bentDual f) a) y).natAbs = + (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs := by + rcases twoVariableWalshMagnitudeProfile + (secondBlockSlice (bentDual f) a) with hbent | haffine + · exact ⟨a, (hbent y).trans (hbent z).symm⟩ + · obtain ⟨u, hu⟩ := haffine + by_cases hyu : y = u + · obtain ⟨b, hb⟩ := + exists_secondBlockSlice_bentDual_walshMagnitude_four + f hf hn a ⟨u, hu⟩ z + refine ⟨b, ?_⟩ + rw [hu, if_pos hyu, hb] + · obtain ⟨b, hb⟩ := + exists_secondBlockSlice_bentDual_walshMagnitude_zero + f hf hn a ⟨u, hu⟩ z + refine ⟨b, ?_⟩ + rw [hu, if_neg hyu, hb] + +/-- The set of magnitudes occurring in the raw Walsh spectrum. -/ +def walshMagnitudeSet (f : BooleanFunction n) : Finset ℕ := + Finset.univ.image fun a ↦ (walshTransform f a).natAbs + +/-- The four codimension-two coordinate restrictions of a bent function have +the same set of raw Walsh magnitudes. -/ +theorem walshMagnitudeSet_firstBlockSlice_eq + (f : BooleanFunction (n + 2)) (hf : IsBent f) (hn : Even n) + (y z : FABL.F₂Cube 2) : + walshMagnitudeSet (firstBlockSlice f y) = + walshMagnitudeSet (firstBlockSlice f z) := by + classical + apply Finset.Subset.antisymm + · intro q hq + rw [walshMagnitudeSet] at hq ⊢ + simp only [Finset.mem_image, Finset.mem_univ, true_and] at hq ⊢ + obtain ⟨a, rfl⟩ := hq + obtain ⟨b, hmagnitude⟩ := + exists_secondBlockSlice_bentDual_same_walshMagnitude + f hf hn a y z + refine ⟨b, ?_⟩ + have hy := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn a y + have hz := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn b z + have htwice : + 2 * (walshTransform (firstBlockSlice f y) a).natAbs = + 2 * (walshTransform (firstBlockSlice f z) b).natAbs := by + calc + 2 * (walshTransform (firstBlockSlice f y) a).natAbs = + 2 ^ (n / 2) * + (walshTransform + (secondBlockSlice (bentDual f) a) y).natAbs := hy + _ = 2 ^ (n / 2) * + (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs := by + rw [hmagnitude] + _ = 2 * (walshTransform (firstBlockSlice f z) b).natAbs := hz.symm + exact (Nat.mul_left_cancel (by omega) htwice).symm + · intro q hq + rw [walshMagnitudeSet] at hq ⊢ + simp only [Finset.mem_image, Finset.mem_univ, true_and] at hq ⊢ + obtain ⟨b, rfl⟩ := hq + obtain ⟨a, hmagnitude⟩ := + exists_secondBlockSlice_bentDual_same_walshMagnitude + f hf hn b z y + refine ⟨a, ?_⟩ + have hz := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn b z + have hy := two_mul_natAbs_walshTransform_firstBlockSlice_eq + f hf hn a y + have htwice : + 2 * (walshTransform (firstBlockSlice f z) b).natAbs = + 2 * (walshTransform (firstBlockSlice f y) a).natAbs := by + calc + 2 * (walshTransform (firstBlockSlice f z) b).natAbs = + 2 ^ (n / 2) * + (walshTransform + (secondBlockSlice (bentDual f) b) z).natAbs := hz + _ = 2 ^ (n / 2) * + (walshTransform + (secondBlockSlice (bentDual f) a) y).natAbs := by + rw [hmagnitude] + _ = 2 * (walshTransform (firstBlockSlice f y) a).natAbs := hy.symm + exact (Nat.mul_left_cancel (by omega) htwice).symm + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/CayleyGraph.lean b/CryptBoolean/Carlet/Chapter06/CayleyGraph.lean new file mode 100644 index 0000000..ccfadc5 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/CayleyGraph.lean @@ -0,0 +1,177 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.HadamardDifferenceSet +public import Mathlib.Combinatorics.SimpleGraph.Cayley +public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular + +/-! +# Boolean Cayley graphs of bent functions + +The support difference-set parameters give the exact strongly regular graph +parameters for a bent function normalized by `f 0 = 0`. +-/ + +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {n : ℕ} + +/-- The additive Cayley graph generated by the support of a Boolean function. -/ +def booleanCayleyGraph (f : BooleanFunction n) : + SimpleGraph (FABL.F₂Cube n) := + SimpleGraph.addCayley (↑(support f) : Set (FABL.F₂Cube n)) + +noncomputable local instance booleanCayleyGraphDecidableRel + (f : BooleanFunction n) : DecidableRel (booleanCayleyGraph f).Adj := + Classical.decRel _ + +/-- Two distinct vertices are adjacent exactly when their sum lies in the +Boolean support. -/ +theorem booleanCayleyGraph_adj + (f : BooleanFunction n) (x y : FABL.F₂Cube n) : + (booleanCayleyGraph f).Adj x y ↔ x ≠ y ∧ f (x + y) = 1 := by + simp [booleanCayleyGraph, SimpleGraph.addCayley_adj, mem_support, + ZModModule.neg_eq_self, add_comm] + +private theorem ne_of_boolean_sum_eq_one + (f : BooleanFunction n) (hfZero : f 0 = 0) + {x y : FABL.F₂Cube n} (hxy : f (x + y) = 1) : + x ≠ y := by + intro h + subst y + rw [ZModModule.add_self, hfZero] at hxy + exact zero_ne_one hxy + +private noncomputable def differenceCommonNeighborEquiv + (f : BooleanFunction n) (hfZero : f 0 = 0) + (v w : FABL.F₂Cube n) : + {x : FABL.F₂Cube n // + x ∈ (support f).filter fun x ↦ x + (v + w) ∈ support f} ≃ + (booleanCayleyGraph f).commonNeighbors v w where + toFun x := by + refine ⟨v + x.1, ?_⟩ + have hx := Finset.mem_filter.mp x.2 + have hxOne : f x.1 = 1 := (mem_support f x.1).1 hx.1 + have hshiftOne : f (x.1 + (v + w)) = 1 := + (mem_support f (x.1 + (v + w))).1 hx.2 + change (booleanCayleyGraph f).Adj v (v + x.1) ∧ + (booleanCayleyGraph f).Adj w (v + x.1) + constructor + · apply (booleanCayleyGraph_adj f v (v + x.1)).2 + have hsum : v + (v + x.1) = x.1 := by + rw [← add_assoc, ZModModule.add_self, zero_add] + exact ⟨ne_of_boolean_sum_eq_one f hfZero (by simpa [hsum] using hxOne), + by simpa [hsum] using hxOne⟩ + · apply (booleanCayleyGraph_adj f w (v + x.1)).2 + have hsum : w + (v + x.1) = x.1 + (v + w) := by ac_rfl + exact ⟨ne_of_boolean_sum_eq_one f hfZero + (by simpa [hsum] using hshiftOne), + by simpa [hsum] using hshiftOne⟩ + invFun z := by + refine ⟨v + z.1, ?_⟩ + have hz := z.2 + change (booleanCayleyGraph f).Adj v z.1 ∧ + (booleanCayleyGraph f).Adj w z.1 at hz + have hv := (booleanCayleyGraph_adj f v z.1).1 hz.1 + have hw := (booleanCayleyGraph_adj f w z.1).1 hz.2 + rw [Finset.mem_filter] + refine ⟨(mem_support f (v + z.1)).2 hv.2, ?_⟩ + apply (mem_support f ((v + z.1) + (v + w))).2 + have hsum : (v + z.1) + (v + w) = w + z.1 := by + rw [show (v + z.1) + (v + w) = (v + v) + (z.1 + w) by ac_rfl, + ZModModule.add_self, zero_add, add_comm] + simpa [hsum] using hw.2 + left_inv x := by + apply Subtype.ext + change v + (v + x.1) = x.1 + rw [← add_assoc, ZModModule.add_self, zero_add] + right_inv z := by + apply Subtype.ext + change v + (v + z.1) = z.1 + rw [← add_assoc, ZModModule.add_self, zero_add] + +/-- Common neighbors in the Boolean Cayley graph are counted by the +corresponding support difference multiplicity. -/ +theorem card_commonNeighbors_booleanCayleyGraph + (f : BooleanFunction n) (hfZero : f 0 = 0) + (v w : FABL.F₂Cube n) : + Nat.card ((booleanCayleyGraph f).commonNeighbors v w) = + differenceMultiplicity (support f) (v + w) := by + classical + rw [differenceMultiplicity] + calc + Nat.card ((booleanCayleyGraph f).commonNeighbors v w) = + Nat.card + {x : FABL.F₂Cube n // + x ∈ (support f).filter fun x ↦ x + (v + w) ∈ support f} := + Nat.card_congr + (differenceCommonNeighborEquiv f hfZero v w).symm + _ = ((support f).filter fun x ↦ + x + (v + w) ∈ support f).card := + Nat.subtype_card _ (fun _ ↦ Iff.rfl) + +/-- The Boolean Cayley graph has degree equal to the support size when the +origin is outside the support. -/ +theorem degree_booleanCayleyGraph + (f : BooleanFunction n) (hfZero : f 0 = 0) + (v : FABL.F₂Cube n) : + (booleanCayleyGraph f).degree v = (support f).card := by + have hcommon := card_commonNeighbors_booleanCayleyGraph f hfZero v v + have hfilter : + (support f).filter (fun x ↦ f x = 1) = support f := by + ext x + simp [mem_support] + rw [← SimpleGraph.card_neighborSet_eq_degree] + rw [← Nat.card_eq_fintype_card] + simpa [SimpleGraph.commonNeighbors, differenceMultiplicity, + ZModModule.add_self, hfilter] using hcommon + +/-- A bent function normalized by `f(0)=0` has a strongly regular Boolean +Cayley graph with its exact Hadamard difference-set parameters. -/ +theorem isSRGWith_booleanCayleyGraph_of_isBent + (f : BooleanFunction n) (hnEven : Even n) (hn : 2 ≤ n) + (hfZero : f 0 = 0) (hf : IsBent f) : + (booleanCayleyGraph f).IsSRGWith + (2 ^ n) (support f).card + ((support f).card - 2 ^ (n - 2)) + ((support f).card - 2 ^ (n - 2)) := by + classical + let G := booleanCayleyGraph f + have hDifferenceSet := + (isBent_iff_support_isHadamardDifferenceSet f hnEven hn).1 hf + refine + { card := card_f₂Cube n + regular := ?_ + of_adj := ?_ + of_not_adj := ?_ } + · intro v + exact degree_booleanCayleyGraph f hfZero v + · intro v w hvw + have hvwNe : v ≠ w := hvw.ne + have hdirection : v + w ≠ 0 := by + intro hzero + apply hvwNe + exact (add_eq_zero_iff_eq_neg.mp hzero).trans + (ZModModule.neg_eq_self w) + rw [← Nat.card_eq_fintype_card, + card_commonNeighbors_booleanCayleyGraph f hfZero] + exact hDifferenceSet.2 (v + w) hdirection + · intro v w hvw _hnotAdjacent + have hdirection : v + w ≠ 0 := by + intro hzero + apply hvw + exact (add_eq_zero_iff_eq_neg.mp hzero).trans + (ZModModule.neg_eq_self w) + rw [← Nat.card_eq_fintype_card, + card_commonNeighbors_booleanCayleyGraph f hfZero] + exact hDifferenceSet.2 (v + w) hdirection + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/DualAffine.lean b/CryptBoolean/Carlet/Chapter06/DualAffine.lean index 298b47b..7b1aaa6 100644 --- a/CryptBoolean/Carlet/Chapter06/DualAffine.lean +++ b/CryptBoolean/Carlet/Chapter06/DualAffine.lean @@ -102,6 +102,34 @@ theorem bentDual_domainTranslate_add_linear apply bitSignInt_injective exact_mod_cast hsignReal +/-- Adding a constant to a bent function adds the same constant to its dual. -/ +theorem bentDual_add_constant + (f : BooleanFunction n) (hf : IsBent f) (c : FABL.𝔽₂) + (a : FABL.F₂Cube n) : + bentDual (f + FABL.affineFunction c 0) a = bentDual f a + c := by + have hg : IsBent (f + FABL.affineFunction c 0) := + (isBent_add_affineFunction_iff f c 0).2 hf + have hdualG := + walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual + (f + FABL.affineFunction c 0) hg a + have hshift := walshTransform_add_affineFunction f c 0 a + have hdualF := + walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual f hf a + apply bitSignInt_injective + apply mul_left_cancel₀ (by positivity : (2 ^ (n / 2) : ℤ) ≠ 0) + calc + (2 ^ (n / 2) : ℤ) * + bitSignInt (bentDual (f + FABL.affineFunction c 0) a) = + walshTransform (f + FABL.affineFunction c 0) a := hdualG.symm + _ = bitSignInt c * walshTransform f (a + 0) := hshift + _ = bitSignInt c * + ((2 ^ (n / 2) : ℤ) * bitSignInt (bentDual f a)) := by + rw [add_zero, hdualF] + _ = (2 ^ (n / 2) : ℤ) * + (bitSignInt (bentDual f a) * bitSignInt c) := by ring + _ = (2 ^ (n / 2) : ℤ) * bitSignInt (bentDual f a + c) := by + rw [bitSignInt_add] + /-- Carlet Relation (45): the two derivative-linear sums have equal imbalance. -/ theorem walshTransform_zero_bentDual_derivative_add_linear (f : BooleanFunction n) (hf : IsBent f) (a b : FABL.F₂Cube n) : diff --git a/CryptBoolean/Carlet/Chapter06/FlatSwitching.lean b/CryptBoolean/Carlet/Chapter06/FlatSwitching.lean index f262122..4fe2237 100644 --- a/CryptBoolean/Carlet/Chapter06/FlatSwitching.lean +++ b/CryptBoolean/Carlet/Chapter06/FlatSwitching.lean @@ -74,7 +74,8 @@ noncomputable def affineFlatWalshSum (b a : FABL.F₂Cube n) : ℤ := ∑ x : E, walshTerm f a (x.1 + b) -private noncomputable def affineFlatSubtypeEquiv +/-- Translation identifies a subspace with each of its affine cosets. -/ +noncomputable def affineFlatSubtypeEquiv (E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)) (b : FABL.F₂Cube n) : E ≃ {x : FABL.F₂Cube n // x ∈ FABL.binaryAffineSubspace E b} where @@ -696,7 +697,8 @@ theorem derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_ba (isBent_flatSwitch_iff_derivative_balanced_on_affineFlat f hf E b).symm.trans (isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced f hf E b) -private theorem bitSignInt_mul_self_flatSwitching (z : FABL.𝔽₂) : +/-- A binary sign squares to one. -/ +theorem bitSignInt_mul_self (z : FABL.𝔽₂) : bitSignInt z * bitSignInt z = 1 := by fin_cases z <;> rfl @@ -739,7 +741,7 @@ theorem two_pow_half_dvd_walshTransform_affineFlatRestriction (bitSignInt (FABL.f₂DotProduct a b) * bitSignInt (FABL.f₂DotProduct a b)) * walshTransform (coordinateAffineSubspaceRestriction f E b e) c := by - rw [bitSignInt_mul_self_flatSwitching, one_mul] + rw [bitSignInt_mul_self, one_mul] _ = bitSignInt (FABL.f₂DotProduct a b) * (bitSignInt (FABL.f₂DotProduct a b) * walshTransform (coordinateAffineSubspaceRestriction f E b e) c) := by diff --git a/CryptBoolean/Carlet/Chapter06/HadamardDifferenceSet.lean b/CryptBoolean/Carlet/Chapter06/HadamardDifferenceSet.lean new file mode 100644 index 0000000..2cbf3e9 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/HadamardDifferenceSet.lean @@ -0,0 +1,220 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.Bentness +public import Mathlib.LinearAlgebra.Matrix.HadamardMatrix + +/-! +# Hadamard matrices and difference sets from bent functions + +Carlet Section 6: the translation sign matrix and the support difference set +characterize bent Boolean functions. +-/ + +open scoped BigOperators BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {n : ℕ} + +/-- The translation sign matrix `H[x,y] = (-1)^(f(x+y))`. -/ +def bentSignMatrix (f : BooleanFunction n) : + Matrix (FABL.F₂Cube n) (FABL.F₂Cube n) ℝ := + fun x y ↦ realSignView f (x + y) + +/-- A Gram-matrix entry of the translation sign matrix is the corresponding +autocorrelation coefficient. -/ +theorem bentSignMatrix_mul_conjTranspose_apply + (f : BooleanFunction n) (x z : FABL.F₂Cube n) : + (bentSignMatrix f * Matrix.conjTranspose (bentSignMatrix f)) x z = + autocorrelation f (x + z) := by + classical + rw [Matrix.mul_apply, autocorrelation] + simp only [Matrix.conjTranspose_apply, bentSignMatrix, star_trivial] + simp_rw [realSignView_booleanDerivative] + change + (∑ y, realSignView f (x + y) * realSignView f (z + y)) = + ∑ y, realSignView f y * realSignView f (y + (x + z)) + calc + (∑ y, realSignView f (x + y) * realSignView f (z + y)) = + ∑ y, realSignView f (x + (y + x)) * + realSignView f (z + (y + x)) := + (Equiv.sum_comp (Equiv.addRight x) + (fun y : FABL.F₂Cube n ↦ + realSignView f (x + y) * realSignView f (z + y))).symm + _ = ∑ y, realSignView f y * realSignView f (y + (x + z)) := by + apply Finset.sum_congr rfl + intro y _hy + have hcancel : x + (y + x) = y := by + calc + x + (y + x) = (x + x) + y := by ac_rfl + _ = y := by rw [ZModModule.add_self, zero_add] + rw [hcancel] + congr 1 + ac_rfl + +private theorem bentSignMatrix_entry_mem_unitary + (f : BooleanFunction n) (x y : FABL.F₂Cube n) : + bentSignMatrix f x y ∈ unitary ℝ := by + apply Unitary.mem_iff_eq_one_or_eq_neg_one.mpr + unfold bentSignMatrix realSignView FABL.realSignEncodedFunction + FABL.signEncodedFunction + rcases FABL.signValue_eq_neg_one_or_one (FABL.signEncode (f (x + y))) with h | h + · exact Or.inr h + · exact Or.inl h + +/-- Bentness is equivalent to the Hadamard property of the translation sign +matrix. -/ +theorem isBent_iff_bentSignMatrix_isHadamard (f : BooleanFunction n) : + IsBent f ↔ (bentSignMatrix f).IsHadamard := by + constructor + · intro hf + apply Matrix.IsHadamard.of_mul_conjTranspose + (bentSignMatrix_entry_mem_unitary f) + · ext x z + rw [bentSignMatrix_mul_conjTranspose_apply] + by_cases hxz : x = z + · subst z + rw [ZModModule.add_self, autocorrelation_zero] + simp + · have hdirection : x + z ≠ 0 := by + intro hzero + apply hxz + exact (add_eq_zero_iff_eq_neg.mp hzero).trans + (ZModModule.neg_eq_self z) + have hbalanced := + (isBent_iff_forall_nonzero_derivative_isBalanced f).mp hf + (x + z) hdirection + have hzero := + (isBalanced_booleanDerivative_iff_autocorrelation_eq_zero + f (x + z)).mp hbalanced + rw [hzero] + simp [hxz] + · exact IsRegular.of_ne_zero (by positivity) + · intro hhadamard + apply (isBent_iff_forall_nonzero_derivative_isBalanced f).mpr + intro a ha + apply (isBalanced_booleanDerivative_iff_autocorrelation_eq_zero f a).mpr + have hentry := congrFun (congrFun hhadamard.mul_conjTranspose 0) a + rw [bentSignMatrix_mul_conjTranspose_apply] at hentry + have hzeroNe : (0 : FABL.F₂Cube n) ≠ a := fun h ↦ ha h.symm + simpa [hzeroNe] using hentry + +/-- The multiplicity of a nonzero group difference inside a finite subset of +the binary cube. -/ +def differenceMultiplicity + (D : Finset (FABL.F₂Cube n)) (a : FABL.F₂Cube n) : ℕ := + (D.filter fun x ↦ x + a ∈ D).card + +/-- The Hadamard difference-set parameters appropriate to a subset of the +binary cube. -/ +def IsHadamardDifferenceSet (D : Finset (FABL.F₂Cube n)) : Prop := + 2 ^ (n - 2) ≤ D.card ∧ + ∀ a : FABL.F₂Cube n, a ≠ 0 → + differenceMultiplicity D a = D.card - 2 ^ (n - 2) + +/-- On a Boolean support, difference multiplicity is the Hamming weight of +the translated function restricted to the original support. -/ +theorem differenceMultiplicity_support_eq_hammingNorm_restriction + (f : BooleanFunction n) (a : FABL.F₂Cube n) : + differenceMultiplicity (support f) a = + hammingNorm (fun x : {x : FABL.F₂Cube n // f x ≠ 0} ↦ f (x.1 + a)) := by + classical + unfold differenceMultiplicity hammingNorm + apply Finset.card_bij + (fun x hx ↦ ⟨x, by + have hxSupport := (Finset.mem_filter.mp hx).1 + rw [mem_support] at hxSupport + simp [hxSupport]⟩) + · intro x hx + rw [Finset.mem_filter] + have hxShift := (mem_support f (x + a)).mp + (Finset.mem_filter.mp hx).2 + exact ⟨Finset.mem_univ _, by simp [hxShift]⟩ + · intro x hx y hy hxy + exact congrArg Subtype.val hxy + · intro y hy + have hyShift : f (y.1 + a) = 1 := + Fin.eq_one_of_ne_zero _ (Finset.mem_filter.mp hy).2 + have hyOne : f y.1 = 1 := Fin.eq_one_of_ne_zero _ y.2 + refine ⟨y.1, ?_, ?_⟩ + · rw [Finset.mem_filter] + exact ⟨(mem_support f y.1).mpr hyOne, + (mem_support f (y.1 + a)).mpr hyShift⟩ + · exact Subtype.ext rfl + +/-- Derivative weight plus twice the support difference multiplicity equals +twice the support size. -/ +theorem hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity + (f : BooleanFunction n) (a : FABL.F₂Cube n) : + hammingWeight (FABL.booleanDerivative f a) + + 2 * differenceMultiplicity (support f) a = + 2 * hammingWeight f := by + have hidentity := hammingNorm_add_restrictSupport_identity + f (fun x ↦ f (x + a)) + rw [← differenceMultiplicity_support_eq_hammingNorm_restriction, + ] at hidentity + have htranslate := hammingWeight_translate f a + change hammingNorm (fun x ↦ f (x + a)) = hammingNorm f at htranslate + rw [htranslate] at hidentity + change hammingNorm (FABL.booleanDerivative f a) + + 2 * differenceMultiplicity (support f) a = 2 * hammingNorm f + change hammingNorm (f + fun x ↦ f (x + a)) + + 2 * differenceMultiplicity (support f) a = 2 * hammingNorm f + omega + +private theorem exists_nonzero_f₂Cube (hn : 0 < n) : + ∃ a : FABL.F₂Cube n, a ≠ 0 := by + let i : Fin n := ⟨0, hn⟩ + let a : FABL.F₂Cube n := Pi.single i 1 + refine ⟨a, ?_⟩ + intro hzero + have hvalue := congrFun hzero i + simp [a, i] at hvalue + +/-- In positive even dimension, bentness is equivalent to the support being +a Hadamard difference set in the additive binary cube. -/ +theorem isBent_iff_support_isHadamardDifferenceSet + (f : BooleanFunction n) (_hnEven : Even n) (hn : 2 ≤ n) : + IsBent f ↔ IsHadamardDifferenceSet (support f) := by + have hpower : 2 ^ n = 4 * 2 ^ (n - 2) := by + rw [show n = (n - 2) + 2 by omega, pow_add] + norm_num + omega + constructor + · intro hf + have hbalanced := + (isBent_iff_forall_nonzero_derivative_isBalanced f).mp hf + have hmultiplicity (a : FABL.F₂Cube n) (ha : a ≠ 0) : + differenceMultiplicity (support f) a + 2 ^ (n - 2) = + hammingWeight f := by + have hderivative := hbalanced a ha + rw [IsBalanced] at hderivative + have hidentity := + hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity f a + omega + obtain ⟨a, ha⟩ := exists_nonzero_f₂Cube (by omega : 0 < n) + have hle : 2 ^ (n - 2) ≤ hammingWeight f := by + have := hmultiplicity a ha + omega + rw [IsHadamardDifferenceSet, ← hammingWeight_eq_card_support] + refine ⟨hle, fun a ha ↦ ?_⟩ + have := hmultiplicity a ha + omega + · rw [IsHadamardDifferenceSet, ← hammingWeight_eq_card_support] + rintro ⟨hle, hmultiplicity⟩ + apply (isBent_iff_forall_nonzero_derivative_isBalanced f).mpr + intro a ha + rw [IsBalanced] + have hidentity := + hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity f a + have hmultiplicity' := hmultiplicity a ha + omega + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean b/CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean index b552202..cc8c7b6 100644 --- a/CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean +++ b/CryptBoolean/Carlet/Chapter06/HyperplaneRestriction.lean @@ -31,7 +31,7 @@ def singletonF₂Cube (b : FABL.𝔽₂) : FABL.F₂Cube 1 := singletonF₂Cube b i = b := rfl -private def singletonF₂CubeLinearEquiv : +def singletonF₂CubeLinearEquiv : FABL.𝔽₂ ≃ₗ[FABL.𝔽₂] FABL.F₂Cube 1 where toFun := singletonF₂Cube invFun x := x 0 @@ -46,7 +46,7 @@ private def singletonF₂CubeLinearEquiv : fin_cases i rfl -private theorem sum_singletonF₂Cube +theorem sum_singletonF₂Cube {R : Type*} [AddCommMonoid R] (g : FABL.F₂Cube 1 → R) : (∑ y, g y) = g (singletonF₂Cube 0) + g (singletonF₂Cube 1) := by calc diff --git a/CryptBoolean/Carlet/Chapter06/IndirectSum.lean b/CryptBoolean/Carlet/Chapter06/IndirectSum.lean index 821044b..d82ef5e 100644 --- a/CryptBoolean/Carlet/Chapter06/IndirectSum.lean +++ b/CryptBoolean/Carlet/Chapter06/IndirectSum.lean @@ -41,33 +41,6 @@ private theorem xor_cancel_left (a b c : FABL.𝔽₂) : a + c + (a + b) = b + c := by fin_cases a <;> fin_cases b <;> fin_cases c <;> decide -private theorem bentDual_add_constant - (f : BooleanFunction n) (hf : IsBent f) (c : FABL.𝔽₂) - (a : FABL.F₂Cube n) : - bentDual (f + FABL.affineFunction c 0) a = bentDual f a + c := by - have hg : IsBent (f + FABL.affineFunction c 0) := - (isBent_add_affineFunction_iff f c 0).2 hf - have hdualG := - walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual - (f + FABL.affineFunction c 0) hg a - have hshift := walshTransform_add_affineFunction f c 0 a - have hdualF := - walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual f hf a - apply bitSignInt_injective - apply mul_left_cancel₀ (by positivity : (2 ^ (n / 2) : ℤ) ≠ 0) - calc - (2 ^ (n / 2) : ℤ) * - bitSignInt (bentDual (f + FABL.affineFunction c 0) a) = - walshTransform (f + FABL.affineFunction c 0) a := hdualG.symm - _ = bitSignInt c * walshTransform f (a + 0) := hshift - _ = bitSignInt c * - ((2 ^ (n / 2) : ℤ) * bitSignInt (bentDual f a)) := by - rw [add_zero, hdualF] - _ = (2 ^ (n / 2) : ℤ) * - (bitSignInt (bentDual f a) * bitSignInt c) := by ring - _ = (2 ^ (n / 2) : ℤ) * bitSignInt (bentDual f a + c) := by - rw [bitSignInt_add] - private theorem firstBlockSlice_indirectSum (f₁ f₂ : BooleanFunction n) (g₁ g₂ : BooleanFunction m) (y : FABL.F₂Cube m) : diff --git a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean index eba6e28..643fe4f 100644 --- a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean +++ b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarland.lean @@ -21,7 +21,26 @@ open scoped BigOperators BooleanCube namespace CryptBoolean -variable {n : ℕ} +variable {m n : ℕ} + +/-- The Boolean-valued original Maiorana--McFarland function associated to a +permutation and an arbitrary Boolean offset. -/ +def booleanMaioranaMcFarlandPermutation + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) : + BooleanFunction (m + m) := + fun z ↦ + let blocks := FABL.f₂CubeBlockEquiv m z + FABL.f₂DotProduct blocks.1 (π blocks.2) + g blocks.2 + +/-- Evaluation of the Boolean Maiorana--McFarland function on its two +coordinate blocks. -/ +@[simp] theorem booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (x y : FABL.F₂Cube m) : + booleanMaioranaMcFarlandPermutation π g + (FABL.joinF₂CubeBlocks x y) = + FABL.f₂DotProduct x (π y) + g y := by + simp [booleanMaioranaMcFarlandPermutation] /-- The original permutation construction belongs to the Maiorana--McFarland class introduced in Chapter 5. -/ @@ -125,4 +144,13 @@ theorem bentDual_maioranaMcFarlandPermutation simpa [add_comm, mul_comm] using hdual.symm exact bitSignInt_injective hsign +/-- Every Boolean-valued original Maiorana--McFarland function is bent. -/ +theorem isBent_booleanMaioranaMcFarlandPermutation + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) : + IsBent (booleanMaioranaMcFarlandPermutation π g) := by + apply isBent_of_maioranaMcFarlandPermutation + (booleanMaioranaMcFarlandPermutation π g) g π + intro x y + exact booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks π g x y + end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean new file mode 100644 index 0000000..1d7ec38 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBalance.lean @@ -0,0 +1,145 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandGeneral + +/-! +# Balance of the Maiorana--McFarland frequency map + +The fiber character sums in Relation (49), together with raw Plancherel, +force the frequency map in every bent representation to be uniformly +distributed. +-/ + +open scoped BigOperators BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {r s : ℕ} + +/-- A map between binary cubes is balanced when all output fibers have the +cardinality forced by the two cube dimensions. -/ +def IsBalancedCubeMap + (φ : FABL.F₂Cube s → FABL.F₂Cube r) : Prop := + ∀ a : FABL.F₂Cube r, + ((Finset.univ : Finset (FABL.F₂Cube s)).filter fun y ↦ φ y = a).card = + 2 ^ (s - r) + +private noncomputable def maioranaMcFarlandFiberSign + (φ : FABL.F₂Cube s → FABL.F₂Cube r) + (g : BooleanFunction s) (a : FABL.F₂Cube r) : + FABL.F₂Cube s → ℝ := + fun y ↦ if φ y = a then realSignView g y else 0 + +private theorem rawFourierTransform_maioranaMcFarlandFiberSign + (φ : FABL.F₂Cube s → FABL.F₂Cube r) + (g : BooleanFunction s) (a : FABL.F₂Cube r) + (b : FABL.F₂Cube s) : + rawFourierTransform (maioranaMcFarlandFiberSign φ g a) b = + (maioranaMcFarlandFiberCharacterSum φ g a b : ℝ) := by + classical + rw [rawFourierTransform, maioranaMcFarlandFiberCharacterSum] + push_cast + rw [Finset.sum_filter] + apply Finset.sum_congr rfl + intro y _hy + by_cases hφ : φ y = a + · simp only [maioranaMcFarlandFiberSign, hφ, if_pos] + rw [bitSignInt_add] + norm_num only [Int.cast_mul] + rw [bitSignInt_cast, bitSignInt_cast] + simp [realSignView, FABL.realSignEncodedFunction, + FABL.signEncodedFunction, FABL.vectorWalshCharacter_apply, + FABL.signValue_signEncode_eq_binarySign] + · simp [hφ, maioranaMcFarlandFiberSign] + +private theorem sum_sq_maioranaMcFarlandFiberSign + (φ : FABL.F₂Cube s → FABL.F₂Cube r) + (g : BooleanFunction s) (a : FABL.F₂Cube r) : + (∑ y, maioranaMcFarlandFiberSign φ g a y ^ 2) = + (((Finset.univ : Finset (FABL.F₂Cube s)).filter + fun y ↦ φ y = a).card : ℝ) := by + classical + calc + (∑ y, maioranaMcFarlandFiberSign φ g a y ^ 2) = + ∑ y, if φ y = a then (1 : ℝ) else 0 := by + apply Finset.sum_congr rfl + intro y _hy + by_cases hφ : φ y = a + · simp [maioranaMcFarlandFiberSign, hφ, realSignView_mul_self, + pow_two] + · simp [maioranaMcFarlandFiberSign, hφ] + _ = (((Finset.univ : Finset (FABL.F₂Cube s)).filter + fun y ↦ φ y = a).card : ℝ) := by + simp + +/-- If a general Maiorana--McFarland representation is bent, then its +frequency map is uniformly distributed over the output cube. -/ +theorem isBalancedCubeMap_of_isBent_maioranaMcFarlandGeneral + (f : BooleanFunction (r + s)) + (φ : FABL.F₂Cube s → FABL.F₂Cube r) + (g : BooleanFunction s) + (hf : ∀ x y, + f (Fin.append x y) = FABL.f₂DotProduct x (φ y) + g y) + (heven : Even (r + s)) (hbent : IsBent f) : + IsBalancedCubeMap φ := by + classical + have hcriterion := + (isBent_iff_maioranaMcFarlandFiberCharacterSum_natAbs + f φ g hf heven).1 hbent + have hrs : r ≤ s := by omega + intro a + let ψ := maioranaMcFarlandFiberSign φ g a + let e := (r + s) / 2 - r + have habs (b : FABL.F₂Cube s) : + |rawFourierTransform ψ b| = (2 : ℝ) ^ e := by + change + |rawFourierTransform (maioranaMcFarlandFiberSign φ g a) b| = _ + rw [rawFourierTransform_maioranaMcFarlandFiberSign] + have hmag := hcriterion.2 a b + have hcast := congrArg (fun k : ℕ ↦ (k : ℝ)) hmag + simpa only [Nat.cast_natAbs, Int.cast_abs, Nat.cast_pow, + Nat.cast_ofNat, e] using hcast + have hplancherel := sum_rawFourierTransform_mul ψ ψ + have hleft : + (∑ b : FABL.F₂Cube s, + rawFourierTransform ψ b * rawFourierTransform ψ b) = + (2 : ℝ) ^ s * ((2 : ℝ) ^ e) ^ 2 := by + calc + (∑ b : FABL.F₂Cube s, + rawFourierTransform ψ b * rawFourierTransform ψ b) = + ∑ _b : FABL.F₂Cube s, ((2 : ℝ) ^ e) ^ 2 := by + apply Finset.sum_congr rfl + intro b _hb + have hsquare := congrArg (fun z : ℝ ↦ z ^ 2) (habs b) + rw [sq_abs] at hsquare + simpa [pow_two] using hsquare + _ = (2 : ℝ) ^ s * ((2 : ℝ) ^ e) ^ 2 := by + rw [Finset.sum_const, Finset.card_univ, card_f₂Cube, nsmul_eq_mul] + norm_num + have hcardReal : + ((((Finset.univ : Finset (FABL.F₂Cube s)).filter + fun y ↦ φ y = a).card : ℕ) : ℝ) = + ((2 : ℝ) ^ e) ^ 2 := by + rw [hleft] at hplancherel + dsimp [ψ] at hplancherel + simp_rw [← pow_two] at hplancherel + rw [sum_sq_maioranaMcFarlandFiberSign] at hplancherel + apply mul_left_cancel₀ (by positivity : (2 : ℝ) ^ s ≠ 0) + exact hplancherel.symm + have hexponent : 2 * e = s - r := by + rcases heven with ⟨k, hk⟩ + dsimp [e] + omega + apply Nat.cast_injective (R := ℝ) + rw [hcardReal] + norm_num only [Nat.cast_pow, Nat.cast_ofNat] + rw [← pow_mul, show e * 2 = s - r by omega] + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean new file mode 100644 index 0000000..db1893a --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandBentSubspace.lean @@ -0,0 +1,165 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter02.FiniteField +public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandGeneral + +/-! +# Linear spaces of bent functions + +Finite-field multiplication supplies the half-dimensional linear spaces of +bent functions noted after the Maiorana--McFarland construction. +-/ + +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +/-- Binary coordinates on a positive-dimensional binary Galois field. -/ +noncomputable def binaryGaloisFieldCoordinateEquiv + (m : ℕ) (hm : 0 < m) : + FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m := + LinearEquiv.ofFinrankEq _ _ (by + rw [Module.finrank_fintype_fun_eq_card, Fintype.card_fin, + GaloisField.finrank 2 hm.ne']) + +/-- Multiplication by a field element, transported to binary cube +coordinates. -/ +noncomputable def fieldMultiplicationCubeMap {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (a : BinaryGaloisField m) : + FABL.F₂Cube m → FABL.F₂Cube m := + fun y ↦ theta.symm (a * theta y) + +/-- The Maiorana--McFarland function indexed linearly by a field element. -/ +noncomputable def fieldMaioranaMcFarlandFunction {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (a : BinaryGaloisField m) : BooleanFunction (m + m) := + fun z ↦ + let p := FABL.f₂CubeBlockEquiv m z + FABL.f₂DotProduct p.1 (fieldMultiplicationCubeMap theta a p.2) + +@[simp] theorem fieldMaioranaMcFarlandFunction_joinF₂CubeBlocks {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (a : BinaryGaloisField m) (x y : FABL.F₂Cube m) : + fieldMaioranaMcFarlandFunction theta a + (FABL.joinF₂CubeBlocks x y) = + FABL.f₂DotProduct x (fieldMultiplicationCubeMap theta a y) := by + simp [fieldMaioranaMcFarlandFunction] + +/-- The field-indexed Maiorana--McFarland family depends linearly on its +field parameter. -/ +noncomputable def fieldMaioranaMcFarlandLinearMap {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + BinaryGaloisField m →ₗ[FABL.𝔽₂] BooleanFunction (m + m) where + toFun := fieldMaioranaMcFarlandFunction theta + map_add' a b := by + funext z + let p := FABL.f₂CubeBlockEquiv m z + simp only [fieldMaioranaMcFarlandFunction, fieldMultiplicationCubeMap, + Pi.add_apply, add_mul, map_add, FABL.f₂DotProduct, dotProduct_add] + map_smul' c a := by + funext z + simp only [fieldMaioranaMcFarlandFunction, fieldMultiplicationCubeMap, + Pi.smul_apply, RingHom.id_apply] + rw [smul_mul_assoc, map_smul, FABL.f₂DotProduct, dotProduct_smul] + rfl + +/-- Multiplication by a nonzero field parameter is a permutation of the +binary coordinate cube. -/ +theorem fieldMultiplicationCubeMap_bijective {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (a : BinaryGaloisField m) (ha : a ≠ 0) : + Function.Bijective (fieldMultiplicationCubeMap theta a) := by + constructor + · intro y z hyz + apply theta.injective + apply mul_left_cancel₀ ha + simpa [fieldMultiplicationCubeMap] using congrArg theta hyz + · intro z + refine ⟨theta.symm (a⁻¹ * theta z), ?_⟩ + simp [fieldMultiplicationCubeMap, ha] + +/-- Every nonzero member of the field-indexed family is bent. -/ +theorem isBent_fieldMaioranaMcFarlandFunction {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (a : BinaryGaloisField m) (ha : a ≠ 0) : + IsBent (fieldMaioranaMcFarlandFunction theta a) := by + apply (isBent_iff_bijective_maioranaMcFarland + (fieldMaioranaMcFarlandFunction theta a) + (fieldMultiplicationCubeMap theta a) 0 (by + intro x y + have hblocks : FABL.f₂CubeBlockEquiv m (Fin.append x y) = (x, y) := by + apply Prod.ext + · funext i + exact Fin.append_left x y i + · funext i + exact Fin.append_right x y i + simp [fieldMaioranaMcFarlandFunction, hblocks])).2 + exact fieldMultiplicationCubeMap_bijective theta a ha + +/-- Distinct field parameters give distinct members of the linear family. -/ +theorem fieldMaioranaMcFarlandLinearMap_injective {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + Function.Injective (fieldMaioranaMcFarlandLinearMap theta) := by + intro a b hab + apply theta.symm.injective + funext i + let x : FABL.F₂Cube m := Pi.single i 1 + let y : FABL.F₂Cube m := theta.symm 1 + have hvalue := congrFun hab (FABL.joinF₂CubeBlocks x y) + simpa [fieldMaioranaMcFarlandLinearMap, fieldMultiplicationCubeMap, + x, y, FABL.f₂DotProduct, single_dotProduct] using hvalue + +/-- The half-dimensional linear space obtained as the range of the +field-indexed family. -/ +noncomputable def maioranaMcFarlandBentSubspace {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + Submodule FABL.𝔽₂ (BooleanFunction (m + m)) := + LinearMap.range (fieldMaioranaMcFarlandLinearMap theta) + +/-- The constructed bent-function space has dimension `m`. -/ +theorem finrank_maioranaMcFarlandBentSubspace {m : ℕ} (hm : 0 < m) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + Module.finrank FABL.𝔽₂ (maioranaMcFarlandBentSubspace theta) = m := by + change Module.finrank FABL.𝔽₂ + (LinearMap.range (fieldMaioranaMcFarlandLinearMap theta)) = m + rw [LinearMap.finrank_range_of_inj + (fieldMaioranaMcFarlandLinearMap_injective theta), + GaloisField.finrank 2 hm.ne'] + +/-- Every nonzero function in the constructed subspace is bent. -/ +theorem isBent_of_mem_maioranaMcFarlandBentSubspace {m : ℕ} + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (f : BooleanFunction (m + m)) + (hf : f ∈ maioranaMcFarlandBentSubspace theta) (hf0 : f ≠ 0) : + IsBent f := by + change f ∈ LinearMap.range (fieldMaioranaMcFarlandLinearMap theta) at hf + obtain ⟨a, rfl⟩ := hf + apply isBent_fieldMaioranaMcFarlandFunction + intro ha + subst a + apply hf0 + funext z + simp [fieldMaioranaMcFarlandLinearMap, + fieldMaioranaMcFarlandFunction, fieldMultiplicationCubeMap, + FABL.f₂DotProduct] + +/-- In every positive even dimension `2m`, there is an `m`-dimensional +linear space of Boolean functions whose nonzero members are bent. -/ +theorem exists_halfDimensionalBentSubspace (m : ℕ) (hm : 0 < m) : + ∃ B : Submodule FABL.𝔽₂ (BooleanFunction (m + m)), + Module.finrank FABL.𝔽₂ B = m ∧ + ∀ f : BooleanFunction (m + m), f ∈ B → f ≠ 0 → IsBent f := by + let theta := binaryGaloisFieldCoordinateEquiv m hm + exact ⟨maioranaMcFarlandBentSubspace theta, + finrank_maioranaMcFarlandBentSubspace hm theta, + isBent_of_mem_maioranaMcFarlandBentSubspace theta⟩ + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean index d003eb9..4c3b639 100644 --- a/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean +++ b/CryptBoolean/Carlet/Chapter06/MaioranaMcFarlandCounting.lean @@ -33,25 +33,6 @@ Maiorana--McFarland construction. -/ abbrev MaioranaMcFarlandParameters (m : ℕ) := Equiv.Perm (FABL.F₂Cube m) × BooleanFunction m -/-- The Boolean-valued original Maiorana--McFarland function associated to a -permutation and an arbitrary Boolean offset. -/ -def booleanMaioranaMcFarlandPermutation - (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) : - BooleanFunction (m + m) := - fun z ↦ - let blocks := FABL.f₂CubeBlockEquiv m z - FABL.f₂DotProduct blocks.1 (π blocks.2) + g blocks.2 - -/-- Evaluation of the Boolean Maiorana--McFarland function on its two -coordinate blocks. -/ -@[simp] theorem booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks - (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) - (x y : FABL.F₂Cube m) : - booleanMaioranaMcFarlandPermutation π g - (FABL.joinF₂CubeBlocks x y) = - FABL.f₂DotProduct x (π y) + g y := by - simp [booleanMaioranaMcFarlandPermutation] - /-- The Boolean function determined by a Maiorana--McFarland parameter pair. -/ def booleanMaioranaMcFarlandOfParameters @@ -111,15 +92,6 @@ theorem card_originalMaioranaMcFarlandClass (m : ℕ) : · rw [Finset.card_univ, card_maioranaMcFarlandParameters] · exact booleanMaioranaMcFarlandOfParameters_injective -/-- Every Boolean-valued original Maiorana--McFarland function is bent. -/ -theorem isBent_booleanMaioranaMcFarlandPermutation - (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) : - IsBent (booleanMaioranaMcFarlandPermutation π g) := by - apply isBent_of_maioranaMcFarlandPermutation - (booleanMaioranaMcFarlandPermutation π g) g π - intro x y - exact booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks π g x y - /-- The finite family of all `n`-variable bent Boolean functions. -/ noncomputable def bentFunctionFamily (n : ℕ) : Finset (BooleanFunction n) := by diff --git a/CryptBoolean/Carlet/Chapter06/NestedBent.lean b/CryptBoolean/Carlet/Chapter06/NestedBent.lean index cd9c672..88c5e6e 100644 --- a/CryptBoolean/Carlet/Chapter06/NestedBent.lean +++ b/CryptBoolean/Carlet/Chapter06/NestedBent.lean @@ -21,28 +21,35 @@ namespace CryptBoolean variable {n m : ℕ} +/-- Appending binary-cube blocks commutes with addition. -/ +@[simp] theorem finAppend_add + (u₁ u₂ : FABL.F₂Cube n) (v₁ v₂ : FABL.F₂Cube m) : + Fin.append (u₁ + u₂) (v₁ + v₂) = + Fin.append u₁ v₁ + Fin.append u₂ v₂ := by + funext i + refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i <;> simp + /-- The restriction of a block Boolean function at a fixed second-block input. -/ def firstBlockSlice (f : BooleanFunction (n + m)) (y : FABL.F₂Cube m) : BooleanFunction n := fun x ↦ f (Fin.append x y) -/-- At a first-block frequency, collect the dual values of all bent first-block slices. -/ -noncomputable def dualSliceFunction - (f : BooleanFunction (n + m)) (s : FABL.F₂Cube n) : BooleanFunction m := - fun y ↦ bentDual (firstBlockSlice f y) s +/-- The restriction of a block Boolean function at a fixed first-block input. -/ +def secondBlockSlice + (f : BooleanFunction (n + m)) (x : FABL.F₂Cube n) : BooleanFunction m := + fun y ↦ f (Fin.append x y) -/-- The raw Walsh transform of nested bent slices factors through their dual slice. -/ -theorem walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction +/-- At fixed first-block frequency, the ambient Walsh transform is the raw +Fourier transform of the Walsh coefficients of the first-block slices. -/ +theorem walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh (f : BooleanFunction (n + m)) - (hslices : ∀ y, IsBent (firstBlockSlice f y)) (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) : - walshTransform f (Fin.append s t) = - (2 ^ (n / 2) : ℤ) * walshTransform (dualSliceFunction f s) t := by + (walshTransform f (Fin.append s t) : ℝ) = + rawFourierTransform + (fun y ↦ (walshTransform (firstBlockSlice f y) s : ℝ)) t := by classical - apply Int.cast_injective (α := ℝ) - push_cast rw [walshTransform_cast_eq_sum_realSignView_mul_character, - walshTransform_cast_eq_sum_realSignView_mul_character] + rawFourierTransform] calc (∑ z : FABL.F₂Cube (n + m), realSignView f z * FABL.vectorWalshCharacter (Fin.append s t) z) = @@ -90,7 +97,31 @@ theorem walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction apply Finset.sum_congr rfl intro y _hy rw [walshTransform_cast_eq_sum_realSignView_mul_character] - _ = ∑ y : FABL.F₂Cube m, + +/-- At a first-block frequency, collect the dual values of all bent first-block slices. -/ +noncomputable def dualSliceFunction + (f : BooleanFunction (n + m)) (s : FABL.F₂Cube n) : BooleanFunction m := + fun y ↦ bentDual (firstBlockSlice f y) s + +/-- The raw Walsh transform of nested bent slices factors through their dual slice. -/ +theorem walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction + (f : BooleanFunction (n + m)) + (hslices : ∀ y, IsBent (firstBlockSlice f y)) + (s : FABL.F₂Cube n) (t : FABL.F₂Cube m) : + walshTransform f (Fin.append s t) = + (2 ^ (n / 2) : ℤ) * walshTransform (dualSliceFunction f s) t := by + classical + apply Int.cast_injective (α := ℝ) + push_cast + rw [walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh, + rawFourierTransform, + walshTransform_cast_eq_sum_realSignView_mul_character + (dualSliceFunction f s) t] + calc + (∑ y : FABL.F₂Cube m, + (walshTransform (firstBlockSlice f y) s : ℝ) * + FABL.vectorWalshCharacter t y) = + ∑ y : FABL.F₂Cube m, ((2 : ℝ) ^ (n / 2) * (bitSignInt (dualSliceFunction f s y) : ℝ)) * FABL.vectorWalshCharacter t y := by diff --git a/CryptBoolean/Carlet/Chapter06/NormalExtension.lean b/CryptBoolean/Carlet/Chapter06/NormalExtension.lean index cf58612..e5da5f4 100644 --- a/CryptBoolean/Carlet/Chapter06/NormalExtension.lean +++ b/CryptBoolean/Carlet/Chapter06/NormalExtension.lean @@ -1834,13 +1834,6 @@ private def prop29CubeThreeLinearEquiv (a b c : ℕ) : ((LinearEquiv.refl FABL.𝔽₂ (FABL.F₂Cube a)).prodCongr (cubeSplitLinearEquiv b c)) -@[simp] private theorem finAppend_add - (u₁ u₂ : FABL.F₂Cube a) (v₁ v₂ : FABL.F₂Cube b) : - Fin.append (u₁ + u₂) (v₁ + v₂) = - Fin.append u₁ v₁ + Fin.append u₂ v₂ := by - funext i - refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i <;> simp - @[simp] private theorem finAppend_smul (c : FABL.𝔽₂) (u : FABL.F₂Cube a) (v : FABL.F₂Cube b) : Fin.append (c • u) (c • v) = c • Fin.append u v := by diff --git a/CryptBoolean/Carlet/Chapter06/PSapCounting.lean b/CryptBoolean/Carlet/Chapter06/PSapCounting.lean new file mode 100644 index 0000000..bd848f9 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/PSapCounting.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter04.SupportDualDistance +public import CryptBoolean.Carlet.Chapter05.Affine +public import CryptBoolean.Carlet.Chapter06.HyperBentPartialSpread +import Mathlib.Data.Fintype.Powerset + +/-! +# Counting the `PS_ap` family + +The partial-spread quotient construction is injectively parametrized by the +balanced Boolean functions on the middle field. +-/ + +open Finset +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +noncomputable local instance psapCountingFieldFintype {r : ℕ} : + Fintype (BinaryGaloisField r) := + Fintype.ofFinite (BinaryGaloisField r) + +/-- The balanced Boolean parameters of the `PS_ap` construction. -/ +abbrev PSapParameters (m : ℕ) := + {g : BooleanFunction m // IsBalanced g} + +noncomputable local instance psapParametersFintype (m : ℕ) : + Fintype (PSapParameters m) := + Fintype.ofFinite (PSapParameters m) + +private noncomputable def booleanFunctionSupportEquiv (m : ℕ) : + BooleanFunction m ≃ Finset (FABL.F₂Cube m) where + toFun := support + invFun := fun S x ↦ if x ∈ S then 1 else 0 + left_inv := by + intro f + funext x + by_cases hx : f x = 0 + · simp [mem_support, hx] + · have hxOne : f x = 1 := Fin.eq_one_of_ne_zero _ hx + simp [mem_support, hxOne] + right_inv := by + intro S + ext x + simp [mem_support] + +private noncomputable def balancedBooleanFunctionSupportEquiv + (m : ℕ) (hm : 0 < m) : + PSapParameters m ≃ + {S : Finset (FABL.F₂Cube m) // S.card = 2 ^ (m - 1)} := + (booleanFunctionSupportEquiv m).subtypeEquiv fun f ↦ by + exact isBalanced_iff_support_card_eq_two_pow_pred f hm + +/-- There are exactly `choose (2^m) (2^(m-1))` balanced Boolean parameters. -/ +theorem card_psapParameters (m : ℕ) (hm : 0 < m) : + Fintype.card (PSapParameters m) = + Nat.choose (2 ^ m) (2 ^ (m - 1)) := by + calc + Fintype.card (PSapParameters m) = + Fintype.card + {S : Finset (FABL.F₂Cube m) // S.card = 2 ^ (m - 1)} := + Fintype.card_congr (balancedBooleanFunctionSupportEquiv m hm) + _ = Nat.choose (Fintype.card (FABL.F₂Cube m)) (2 ^ (m - 1)) := + Fintype.card_finset_len (2 ^ (m - 1)) + _ = Nat.choose (2 ^ m) (2 ^ (m - 1)) := by + rw [card_f₂Cube] + +/-- The field-valued `PS_ap` function selected by a balanced Boolean +parameter and fixed quadratic-extension coordinates. -/ +noncomputable def psapOfParameters {m : ℕ} (hm : 0 < m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (g : PSapParameters m) : FieldBooleanFunction (2 * m) := + psapFunction hm iota omega homega (g.1 ∘ theta.symm) + +/-- Evaluation of a parametrized `PS_ap` function in quadratic-extension +coordinates. -/ +@[simp] theorem psapOfParameters_coordinate {m : ℕ} (hm : 0 < m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (g : PSapParameters m) (y' y : BinaryGaloisField m) : + psapOfParameters hm iota omega homega theta g + (iota y' + omega * iota y) = + g.1 (theta.symm (y' / y)) := by + rw [psapOfParameters, psapFunction_coordinate] + rfl + +/-- Distinct balanced parameters give distinct `PS_ap` functions. -/ +theorem psapOfParameters_injective {m : ℕ} (hm : 0 < m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + Function.Injective (psapOfParameters hm iota omega homega theta) := by + intro g h heq + apply Subtype.ext + funext x + have hvalue := congrFun heq + (iota (theta x) + omega * iota (1 : BinaryGaloisField m)) + rw [psapOfParameters_coordinate, psapOfParameters_coordinate] at hvalue + simpa using hvalue + +/-- The finite `PS_ap` family in fixed quadratic-extension coordinates. -/ +noncomputable def psapClass {m : ℕ} (hm : 0 < m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + Finset (FieldBooleanFunction (2 * m)) := by + classical + exact Finset.univ.image + (psapOfParameters hm iota omega homega theta) + +/-- Carlet's exact count for the `PS_ap` family. -/ +theorem card_psapClass {m : ℕ} (hm : 0 < m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) : + (psapClass hm iota omega homega theta).card = + Nat.choose (2 ^ m) (2 ^ (m - 1)) := by + classical + rw [psapClass, Finset.card_image_of_injective, + Finset.card_univ, card_psapParameters m hm] + exact psapOfParameters_injective hm iota omega homega theta + +private theorem isBalanced_add_constant_one + {m : ℕ} (f : BooleanFunction m) (hf : IsBalanced f) : + IsBalanced (f + FABL.affineFunction 1 0) := by + apply (isBalanced_iff_walshTransform_zero_eq_zero _).2 + rw [walshTransform_add_affineFunction] + simp only [add_zero] + rw [(isBalanced_iff_walshTransform_zero_eq_zero f).1 hf] + simp + +/-- Every balanced `PS_ap` parameter yields a bent function after any linear +choice of ambient binary coordinates. -/ +theorem isBent_psapOfParameters_comp_linearEquiv {m : ℕ} (hm : 2 ≤ m) + (iota : BinaryGaloisField m →ₐ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (omega : BinaryGaloisField (2 * m)) (homega : omega ∉ Set.range iota) + (theta : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] BinaryGaloisField m) + (Theta : FABL.F₂Cube (2 * m) ≃ₗ[FABL.𝔽₂] + BinaryGaloisField (2 * m)) + (g : PSapParameters m) : + IsBent (psapOfParameters (by omega) iota omega homega theta g ∘ Theta) := by + let gf : FieldBooleanFunction m := g.1 ∘ theta.symm + have hgfBalanced : IsBalanced (gf ∘ theta) := by + simpa [gf, Function.comp_def] using g.2 + by_cases hgfZero : gf 0 = 0 + · have hhyper := isHyperBent_psapFunction hm iota omega homega theta + gf hgfBalanced hgfZero + exact (isFieldBent_iff_isBent_comp_linearEquiv Theta _).1 + hhyper.isFieldBent + · have hgfOne : gf 0 = 1 := Fin.eq_one_of_ne_zero _ hgfZero + let gc : FieldBooleanFunction m := fun x ↦ gf x + 1 + have hgcZero : gc 0 = 0 := by + simp [gc, hgfOne] + have hgcCoordinate : + gc ∘ theta = + (gf ∘ theta) + FABL.affineFunction 1 0 := by + funext x + simp [gc, FABL.affineFunction, FABL.f₂DotProduct] + have hgcBalanced : IsBalanced (gc ∘ theta) := by + rw [hgcCoordinate] + exact isBalanced_add_constant_one (gf ∘ theta) hgfBalanced + have hhyper := isHyperBent_psapFunction hm iota omega homega theta + gc hgcBalanced hgcZero + have hgcBent : + IsBent (psapFunction (by omega) iota omega homega gc ∘ Theta) := + (isFieldBent_iff_isBent_comp_linearEquiv Theta _).1 + hhyper.isFieldBent + have hcomplement : + psapFunction (by omega) iota omega homega gf ∘ Theta = + (psapFunction (by omega) iota omega homega gc ∘ Theta) + + FABL.affineFunction 1 0 := by + funext x + simp only [Function.comp_apply, Pi.add_apply, FABL.affineFunction, + FABL.f₂DotProduct, zero_dotProduct, add_zero] + unfold psapFunction + dsimp [gc] + rw [add_assoc, show (1 : FABL.𝔽₂) + 1 = 0 by decide, + add_zero] + change IsBent (psapFunction (by omega) iota omega homega gf ∘ Theta) + rw [hcomplement] + exact (isBent_add_affineFunction_iff + (psapFunction (by omega) iota omega homega gc ∘ Theta) 1 0).2 + hgcBent + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean b/CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean new file mode 100644 index 0000000..4c87497 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/SecondaryClasses.lean @@ -0,0 +1,873 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.FlatSwitching +public import CryptBoolean.Carlet.Chapter06.MaioranaMcFarland +public import CryptBoolean.Carlet.Chapter06.NestedBent +public import FABL.Chapter06.F₂Polynomials.Interpolation + +/-! +# Secondary classes of bent functions + +Carlet's classes `D₀`, `D`, and `C` derived from the permutation +Maiorana--McFarland construction and affine-flat switching. +-/ + +open Finset +open scoped BigOperators BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {k m : ℕ} + +noncomputable local instance secondaryClassesSubmoduleFintype + (S : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : Fintype S := + Fintype.ofFinite S + +private def firstBlockZeroLinearMap (m : ℕ) : + FABL.F₂Cube m →ₗ[FABL.𝔽₂] FABL.F₂Cube (m + m) where + toFun y := Fin.append 0 y + map_add' x y := by + funext i + refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i + · simp + · simp only [Pi.add_apply, Fin.append_right] + map_smul' c x := by + funext i + refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i + · simp + · simp only [Pi.smul_apply, Fin.append_right, RingHom.id_apply] + +private theorem firstBlockZeroLinearMap_injective : + Function.Injective (firstBlockZeroLinearMap m) := by + intro x y hxy + funext i + have h := congrFun hxy (Fin.addNat i m) + simpa [firstBlockZeroLinearMap, ← Fin.natAdd_eq_addNat] using h + +private def firstBlockZeroSubspace (m : ℕ) : + Submodule FABL.𝔽₂ (FABL.F₂Cube (m + m)) := + LinearMap.range (firstBlockZeroLinearMap m) + +private noncomputable def firstBlockZeroLinearEquiv (m : ℕ) : + FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] firstBlockZeroSubspace m := + LinearEquiv.ofInjective (firstBlockZeroLinearMap m) + firstBlockZeroLinearMap_injective + +@[simp] private theorem firstBlockZeroLinearEquiv_apply_coe + (y : FABL.F₂Cube m) : + (firstBlockZeroLinearEquiv m y).1 = Fin.append 0 y := + rfl + +private theorem mem_firstBlockZeroSubspace_append_iff + (x y : FABL.F₂Cube m) : + Fin.append x y ∈ firstBlockZeroSubspace m ↔ x = 0 := by + constructor + · rintro ⟨z, hz⟩ + funext i + have h := congrFun hz (Fin.castAdd m i) + simpa [firstBlockZeroLinearMap] using h.symm + · rintro rfl + exact ⟨y, rfl⟩ + +@[simp] private theorem cubeSplitLinearEquiv_append + (x y : FABL.F₂Cube m) : + cubeSplitLinearEquiv m m (Fin.append x y) = (x, y) := by + apply Prod.ext + · funext i + exact Fin.append_left x y i + · funext i + exact Fin.append_right x y i + +@[simp] private theorem joinF₂CubeBlocks_eq_append + (x y : FABL.F₂Cube m) : + FABL.joinF₂CubeBlocks x y = Fin.append x y := + rfl + +@[simp] private theorem booleanMaioranaMcFarlandPermutation_append + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (x y : FABL.F₂Cube m) : + booleanMaioranaMcFarlandPermutation π g (Fin.append x y) = + FABL.f₂DotProduct x (π y) + g y := by + rw [← joinF₂CubeBlocks_eq_append, + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks] + +/-- Carlet's class `D₀`, obtained by switching the zero first-block flat +of the permutation Maiorana--McFarland construction. -/ +def classDZero + (π : Equiv.Perm (FABL.F₂Cube m)) : BooleanFunction (m + m) := + fun z ↦ + let p := cubeSplitLinearEquiv m m z + FABL.f₂DotProduct p.1 (π p.2) + FABL.f₂PointIndicator 0 p.1 + +@[simp] theorem classDZero_append + (π : Equiv.Perm (FABL.F₂Cube m)) + (x y : FABL.F₂Cube m) : + classDZero π (Fin.append x y) = + FABL.f₂DotProduct x (π y) + FABL.f₂PointIndicator 0 x := by + rw [classDZero, cubeSplitLinearEquiv_append] + +private theorem affineFlatIndicator_firstBlockZero_append + (x y : FABL.F₂Cube m) : + affineFlatIndicator (firstBlockZeroSubspace m) 0 (Fin.append x y) = + FABL.f₂PointIndicator 0 x := by + classical + rw [FABL.f₂PointIndicator_eq_ite] + by_cases hx : x = 0 + · rw [if_pos hx, affineFlatIndicator_apply_eq_one_iff] + simpa [FABL.mem_binaryAffineSubspace_iff_add_mem] using + (mem_firstBlockZeroSubspace_append_iff x y).2 hx + · rw [if_neg hx] + simp only [affineFlatIndicator] + rw [if_neg] + simpa [FABL.mem_binaryAffineSubspace_iff_add_mem] using + (mem_firstBlockZeroSubspace_append_iff x y).not.mpr hx + +private theorem classDZero_eq_flatSwitch + (π : Equiv.Perm (FABL.F₂Cube m)) : + classDZero π = + flatSwitch (booleanMaioranaMcFarlandPermutation π 0) + (firstBlockZeroSubspace m) 0 := by + funext z + let p := cubeSplitLinearEquiv m m z + have hz : Fin.append p.1 p.2 = z := + (Fin.appendEquiv m m).apply_symm_apply z + rw [← hz, classDZero_append, flatSwitch, Pi.add_apply, + booleanMaioranaMcFarlandPermutation_append, + affineFlatIndicator_firstBlockZero_append, Pi.zero_apply, add_zero] + +private theorem affineFlatWalshSum_maioranaMcFarlandZero + (π : Equiv.Perm (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) : + affineFlatWalshSum (booleanMaioranaMcFarlandPermutation π 0) + (firstBlockZeroSubspace m) 0 (Fin.append a b) = + if b = 0 then (2 ^ m : ℤ) else 0 := by + let e := firstBlockZeroLinearEquiv m + have hfrequency : ∀ y : FABL.F₂Cube m, + FABL.f₂DotProduct (Fin.append a b) (e y).1 = + FABL.f₂DotProduct b y := by + intro y + rw [show (e y).1 = Fin.append 0 y by rfl, + FABL.f₂DotProduct_append] + simp [FABL.f₂DotProduct, dotProduct_zero] + rw [affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction + (booleanMaioranaMcFarlandPermutation π 0) (firstBlockZeroSubspace m) 0 + (Fin.append a b) e b hfrequency] + have hrestriction : + coordinateAffineSubspaceRestriction (booleanMaioranaMcFarlandPermutation π 0) + (firstBlockZeroSubspace m) 0 e = + FABL.affineFunction 0 0 := by + funext y + simp [coordinateAffineSubspaceRestriction_apply, e, + booleanMaioranaMcFarlandPermutation_append, + FABL.affineFunction, FABL.f₂DotProduct] + rw [hrestriction, walshTransform_affineFunction] + simp [FABL.f₂DotProduct, dotProduct_zero, bitSignInt] + +/-- The exact Walsh spectrum of Carlet's class `D₀`. -/ +theorem walshTransform_classDZero + (π : Equiv.Perm (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) : + walshTransform (classDZero π) (Fin.append a b) = + bitSignInt + (FABL.f₂DotProduct b (π.symm a) + + FABL.f₂PointIndicator 0 b) * + (2 ^ m : ℤ) := by + have hdifference := walshTransform_sub_flatSwitch + (booleanMaioranaMcFarlandPermutation π 0) (firstBlockZeroSubspace m) 0 + (Fin.append a b) + rw [← classDZero_eq_flatSwitch π, + affineFlatWalshSum_maioranaMcFarlandZero] at hdifference + have hbase := walshTransform_maioranaMcFarlandPermutation + (booleanMaioranaMcFarlandPermutation π 0) 0 π + (by + intro x y + exact booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks π 0 x y) a b + simp only [Pi.zero_apply, zero_add] at hbase + change walshTransform (booleanMaioranaMcFarlandPermutation π 0) + (Fin.append a b) = _ at hbase + by_cases hb : b = 0 + · subst b + rw [hbase] at hdifference + simp [FABL.f₂PointIndicator_eq_ite, FABL.f₂DotProduct, + bitSignInt] at hdifference ⊢ + linarith + · rw [if_neg hb] at hdifference + rw [hbase] at hdifference + rw [FABL.f₂PointIndicator_eq_ite, if_neg hb, add_zero] + linarith + +/-- Every class-`D₀` function is bent. -/ +theorem isBent_classDZero + (π : Equiv.Perm (FABL.F₂Cube m)) : + IsBent (classDZero π) := by + apply (isBent_iff_forall_natAbs_walshTransform_eq_two_pow_half _).2 + intro u + let p := cubeSplitLinearEquiv m m u + have hu : Fin.append p.1 p.2 = u := + (Fin.appendEquiv m m).apply_symm_apply u + rw [← hu, walshTransform_classDZero, Int.natAbs_mul] + have hhalf : (m + m) / 2 = m := by omega + rw [hhalf] + simp [bitSignInt] + +/-- The dual of a class-`D₀` function has the inverse-permutation formula +recorded by Carlet. -/ +theorem bentDual_classDZero_append + (π : Equiv.Perm (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) : + bentDual (classDZero π) (Fin.append a b) = + FABL.f₂DotProduct b (π.symm a) + FABL.f₂PointIndicator 0 b := by + have hdual := walshTransform_eq_two_pow_half_mul_bitSignInt_bentDual + (classDZero π) (isBent_classDZero π) (Fin.append a b) + have hhalf : (m + m) / 2 = m := by omega + rw [hhalf, walshTransform_classDZero] at hdual + apply bitSignInt_injective + exact mul_right_cancel₀ (by positivity : (2 ^ m : ℤ) ≠ 0) + (by simpa [mul_comm] using hdual.symm) + +private def submoduleProdLinearEquiv + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + (E₁ × E₂) ≃ₗ[FABL.𝔽₂] E₁.prod E₂ where + toFun p := ⟨(p.1.1, p.2.1), p.1.2, p.2.2⟩ + invFun p := (⟨p.1.1, p.2.1⟩, ⟨p.1.2, p.2.2⟩) + left_inv _ := rfl + right_inv _ := rfl + map_add' _ _ := rfl + map_smul' _ _ := rfl + +private def blockProductSubspace + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + Submodule FABL.𝔽₂ (FABL.F₂Cube (m + m)) := + (E₁.prod E₂).map (cubeSplitLinearEquiv m m).symm.toLinearMap + +private theorem mem_blockProductSubspace_iff + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (z : FABL.F₂Cube (m + m)) : + z ∈ blockProductSubspace E₁ E₂ ↔ + (cubeSplitLinearEquiv m m z).1 ∈ E₁ ∧ + (cubeSplitLinearEquiv m m z).2 ∈ E₂ := by + constructor + · rintro ⟨p, hp, hpz⟩ + have hsplit := congrArg (cubeSplitLinearEquiv m m) hpz + have hpEq : p = cubeSplitLinearEquiv m m z := by + simpa using hsplit + rw [← hpEq] + exact hp + · intro hz + refine ⟨cubeSplitLinearEquiv m m z, hz, ?_⟩ + exact (cubeSplitLinearEquiv m m).symm_apply_apply z + +private theorem mem_blockProductSubspace_append_iff + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (x y : FABL.F₂Cube m) : + Fin.append x y ∈ blockProductSubspace E₁ E₂ ↔ + x ∈ E₁ ∧ y ∈ E₂ := by + rw [mem_blockProductSubspace_iff, cubeSplitLinearEquiv_append] + +private theorem finrank_blockProductSubspace + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + Module.finrank FABL.𝔽₂ (blockProductSubspace E₁ E₂) = + Module.finrank FABL.𝔽₂ E₁ + Module.finrank FABL.𝔽₂ E₂ := by + rw [blockProductSubspace, LinearEquiv.finrank_map_eq, + ← (submoduleProdLinearEquiv E₁ E₂).finrank_eq, + Module.finrank_prod] + +private def permutationSubmoduleEquiv + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (hπ : ∀ y, y ∈ E₂ ↔ π y ∈ FABL.perpendicularSubspace E₁) : + E₂ ≃ FABL.perpendicularSubspace E₁ where + toFun y := ⟨π y.1, (hπ y.1).1 y.2⟩ + invFun z := ⟨π.symm z.1, (hπ (π.symm z.1)).2 (by + rw [π.apply_symm_apply] + exact z.2)⟩ + left_inv y := by + apply Subtype.ext + simp + right_inv z := by + apply Subtype.ext + simp + +private theorem finrank_add_finrank_eq_of_permutation_image_perpendicular + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (hπ : ∀ y, y ∈ E₂ ↔ π y ∈ FABL.perpendicularSubspace E₁) : + Module.finrank FABL.𝔽₂ E₁ + Module.finrank FABL.𝔽₂ E₂ = m := by + have hcard : Nat.card E₂ = Nat.card (FABL.perpendicularSubspace E₁) := + Nat.card_congr (permutationSubmoduleEquiv π E₁ E₂ hπ) + rw [FABL.card_submodule_eq_two_pow_finrank, + FABL.card_submodule_eq_two_pow_finrank, + FABL.finrank_perpendicularSubspace] at hcard + have hrank : Module.finrank FABL.𝔽₂ E₂ = + m - Module.finrank FABL.𝔽₂ E₁ := + Nat.pow_right_injective (by norm_num : 2 ≤ 2) hcard + have hle : Module.finrank FABL.𝔽₂ E₁ ≤ m := by + simpa using E₁.finrank_le + omega + +private theorem affineFlatIndicator_blockProduct_append + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (x y : FABL.F₂Cube m) : + affineFlatIndicator (blockProductSubspace E₁ E₂) 0 + (Fin.append x y) = + affineFlatIndicator E₁ 0 x * affineFlatIndicator E₂ 0 y := by + classical + by_cases hx : x ∈ E₁ <;> by_cases hy : y ∈ E₂ <;> + simp [affineFlatIndicator, FABL.mem_binaryAffineSubspace_iff_add_mem, + mem_blockProductSubspace_append_iff, hx, hy] + +/-- Carlet's class `D`, obtained by switching a permutation +Maiorana--McFarland function on a product of subspaces. -/ +noncomputable def classD + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + BooleanFunction (m + m) := + fun z ↦ + let p := cubeSplitLinearEquiv m m z + FABL.f₂DotProduct p.1 (π p.2) + + affineFlatIndicator E₁ 0 p.1 * affineFlatIndicator E₂ 0 p.2 + +@[simp] theorem classD_append + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (x y : FABL.F₂Cube m) : + classD π E₁ E₂ (Fin.append x y) = + FABL.f₂DotProduct x (π y) + + affineFlatIndicator E₁ 0 x * affineFlatIndicator E₂ 0 y := by + rw [classD, cubeSplitLinearEquiv_append] + +private theorem classD_eq_flatSwitch + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + classD π E₁ E₂ = + flatSwitch (booleanMaioranaMcFarlandPermutation π 0) + (blockProductSubspace E₁ E₂) 0 := by + funext z + let p := cubeSplitLinearEquiv m m z + have hz : Fin.append p.1 p.2 = z := + (Fin.appendEquiv m m).apply_symm_apply z + rw [← hz, classD_append, flatSwitch, Pi.add_apply, + booleanMaioranaMcFarlandPermutation_append, + affineFlatIndicator_blockProduct_append, Pi.zero_apply, add_zero] + +/-- Carlet's class `D` is bent when the permutation sends the second +switching subspace onto the perpendicular of the first. -/ +theorem isBent_classD + (π : Equiv.Perm (FABL.F₂Cube m)) + (E₁ E₂ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (hπ : ∀ y, y ∈ E₂ ↔ π y ∈ FABL.perpendicularSubspace E₁) : + IsBent (classD π E₁ E₂) := by + let E := blockProductSubspace E₁ E₂ + have hErank : Module.finrank FABL.𝔽₂ E = m := by + change Module.finrank FABL.𝔽₂ (blockProductSubspace E₁ E₂) = m + rw [finrank_blockProductSubspace] + exact finrank_add_finrank_eq_of_permutation_image_perpendicular π E₁ E₂ hπ + let e : FABL.F₂Cube m ≃ₗ[FABL.𝔽₂] E := + LinearEquiv.ofFinrankEq _ _ (by + rw [Module.finrank_fintype_fun_eq_card] + simpa using hErank.symm) + have hbase : IsBent (booleanMaioranaMcFarlandPermutation π 0) := + isBent_booleanMaioranaMcFarlandPermutation π 0 + have hrestriction : + coordinateAffineSubspaceRestriction + (booleanMaioranaMcFarlandPermutation π 0) E 0 e = 0 := by + funext z + rw [coordinateAffineSubspaceRestriction_apply, add_zero] + let p := cubeSplitLinearEquiv m m (e z).1 + have hp : p.1 ∈ E₁ ∧ p.2 ∈ E₂ := by + exact (mem_blockProductSubspace_iff E₁ E₂ (e z).1).1 (e z).2 + have hperp : π p.2 ∈ FABL.perpendicularSubspace E₁ := + (hπ p.2).1 hp.2 + have hzero := (FABL.mem_perpendicularSubspace_iff E₁ (π p.2)).1 + hperp p.1 hp.1 + change FABL.f₂DotProduct p.1 (π p.2) + 0 = 0 + rw [add_zero] + rw [show FABL.f₂DotProduct p.1 (π p.2) = + FABL.f₂DotProduct (π p.2) p.1 by exact dotProduct_comm _ _] + exact hzero + have hdegree : FABL.functionAlgebraicDegree + (coordinateAffineSubspaceRestriction + (booleanMaioranaMcFarlandPermutation π 0) E 0 e) ≤ 1 := by + rw [hrestriction, FABL.functionAlgebraicDegree_zero] + omega + have hswitch := + isBent_flatSwitch_of_half_dimension_of_restriction_degree_le_one + (booleanMaioranaMcFarlandPermutation π 0) hbase E 0 e (by omega) hdegree + rw [classD_eq_flatSwitch] + simpa [E] using hswitch + +private def leftBlockPerpendicularLinearMap + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + FABL.perpendicularSubspace L →ₗ[FABL.𝔽₂] + FABL.perpendicularSubspace (blockProductSubspace L ⊤) where + toFun u := ⟨Fin.append u.1 0, by + rw [FABL.mem_perpendicularSubspace_iff] + intro z hz + let p := cubeSplitLinearEquiv m m z + have hp : p.1 ∈ L := + (mem_blockProductSubspace_iff L ⊤ z).1 hz |>.1 + have hz' : Fin.append p.1 p.2 = z := + (Fin.appendEquiv m m).apply_symm_apply z + rw [← hz', FABL.f₂DotProduct_append] + have hzero := (FABL.mem_perpendicularSubspace_iff L u.1).1 + u.2 p.1 hp + rw [hzero] + simp [FABL.f₂DotProduct, zero_dotProduct]⟩ + map_add' u v := by + apply Subtype.ext + funext i + refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i + · simp only [Pi.add_apply, Fin.append_left, Submodule.coe_add] + · simp only [Pi.add_apply, Fin.append_right, Submodule.coe_add] + simp + map_smul' c u := by + apply Subtype.ext + funext i + refine Fin.addCases (fun j ↦ ?_) (fun j ↦ ?_) i + · simp only [Pi.smul_apply, Fin.append_left, SetLike.val_smul, + RingHom.id_apply] + · simp only [Pi.smul_apply, Fin.append_right, SetLike.val_smul, + RingHom.id_apply] + simp + +private theorem leftBlockPerpendicularLinearMap_injective + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + Function.Injective (leftBlockPerpendicularLinearMap L) := by + intro u v huv + apply Subtype.ext + funext i + have h := congrArg + (fun z : FABL.perpendicularSubspace (blockProductSubspace L ⊤) ↦ + z.1 (Fin.castAdd m i)) huv + simpa [leftBlockPerpendicularLinearMap] using h + +private theorem leftBlockPerpendicularLinearMap_surjective + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + Function.Surjective (leftBlockPerpendicularLinearMap L) := by + intro γ + let p := cubeSplitLinearEquiv m m γ.1 + have hsecond : p.2 = 0 := by + funext i + have hzmem : Fin.append 0 (Pi.single i 1) ∈ + blockProductSubspace L ⊤ := by + rw [mem_blockProductSubspace_append_iff] + simp + have hdot := + (FABL.mem_perpendicularSubspace_iff (blockProductSubspace L ⊤) γ.1).1 + γ.2 (Fin.append 0 (Pi.single i 1)) hzmem + have hγ : Fin.append p.1 p.2 = γ.1 := + (Fin.appendEquiv m m).apply_symm_apply γ.1 + rw [← hγ, FABL.f₂DotProduct_append] at hdot + simpa [FABL.f₂DotProduct, dotProduct_zero, dotProduct_single] using hdot + have hfirst : p.1 ∈ FABL.perpendicularSubspace L := by + rw [FABL.mem_perpendicularSubspace_iff] + intro x hx + have hzmem : Fin.append x 0 ∈ blockProductSubspace L ⊤ := by + rw [mem_blockProductSubspace_append_iff] + simp [hx] + have hdot := + (FABL.mem_perpendicularSubspace_iff (blockProductSubspace L ⊤) γ.1).1 + γ.2 (Fin.append x 0) hzmem + have hγ : Fin.append p.1 p.2 = γ.1 := + (Fin.appendEquiv m m).apply_symm_apply γ.1 + rw [← hγ, FABL.f₂DotProduct_append] at hdot + simpa [FABL.f₂DotProduct, dotProduct_zero] using hdot + refine ⟨⟨p.1, hfirst⟩, ?_⟩ + apply Subtype.ext + apply (cubeSplitLinearEquiv m m).injective + have hγ : Fin.append p.1 p.2 = γ.1 := + (Fin.appendEquiv m m).apply_symm_apply γ.1 + rw [show (leftBlockPerpendicularLinearMap L ⟨p.1, hfirst⟩).1 = + Fin.append p.1 0 by rfl, cubeSplitLinearEquiv_append, + ← hγ, cubeSplitLinearEquiv_append, hsecond] + +private noncomputable def leftBlockPerpendicularLinearEquiv + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + FABL.perpendicularSubspace L ≃ₗ[FABL.𝔽₂] + FABL.perpendicularSubspace (blockProductSubspace L ⊤) := + LinearEquiv.ofBijective (leftBlockPerpendicularLinearMap L) + ⟨leftBlockPerpendicularLinearMap_injective L, + leftBlockPerpendicularLinearMap_surjective L⟩ + +@[simp] private theorem leftBlockPerpendicularLinearEquiv_apply_coe + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (u : FABL.perpendicularSubspace L) : + (leftBlockPerpendicularLinearEquiv L u).1 = Fin.append u.1 0 := + rfl + +@[simp] private theorem leftBlockPerpendicularLinearEquiv_symm_apply_coe + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (q : FABL.perpendicularSubspace (blockProductSubspace L ⊤)) : + ((leftBlockPerpendicularLinearEquiv L).symm q).1 = + (cubeSplitLinearEquiv m m q.1).1 := by + have h := congrArg + (fun z : FABL.perpendicularSubspace (blockProductSubspace L ⊤) ↦ z.1) + ((leftBlockPerpendicularLinearEquiv L).apply_symm_apply q) + rw [leftBlockPerpendicularLinearEquiv_apply_coe] at h + have hfirst := congrArg (fun z ↦ (cubeSplitLinearEquiv m m z).1) h + rw [cubeSplitLinearEquiv_append] at hfirst + exact hfirst + +private theorem affineSubspaceRestrictionImbalance_eq_walshTransform_zero_cast + (f : BooleanFunction m) + (E : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a : FABL.F₂Cube m) + (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] E) : + affineSubspaceRestrictionImbalance f E a = + (walshTransform (coordinateAffineSubspaceRestriction f E a e) 0 : ℝ) := by + classical + rw [affineSubspaceRestrictionImbalance, + walshTransform_cast_eq_sum_realSignView_mul_character] + calc + (∑ x : E, FABL.affineSubspaceRestriction (realSignView f) E a x) = + ∑ y : FABL.F₂Cube k, + FABL.affineSubspaceRestriction (realSignView f) E a (e y) := by + exact (Equiv.sum_comp e.toEquiv + (fun x : E ↦ FABL.affineSubspaceRestriction (realSignView f) E a x)).symm + _ = ∑ y : FABL.F₂Cube k, + realSignView (coordinateAffineSubspaceRestriction f E a e) y * + FABL.vectorWalshCharacter 0 y := by + apply Finset.sum_congr rfl + intro y _hy + simp [coordinateAffineSubspaceRestriction, realSignView, + FABL.realSignEncodedFunction, FABL.signEncodedFunction] + +private theorem isConstantOrBalancedOnAffineFlat_of_coordinate_eq_affineFunction + (f : BooleanFunction m) + (E : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a : FABL.F₂Cube m) + (e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] E) + (d : FABL.𝔽₂) (u : FABL.F₂Cube k) + (hrestriction : coordinateAffineSubspaceRestriction f E a e = + FABL.affineFunction d u) : + IsConstantOrBalancedOnAffineFlat f E a := by + rw [IsConstantOrBalancedOnAffineFlat] + have himbalance := + affineSubspaceRestrictionImbalance_eq_walshTransform_zero_cast f E a e + have hcard : Nat.card E = 2 ^ k := by + calc + Nat.card E = Nat.card (FABL.F₂Cube k) := + Nat.card_congr e.symm.toEquiv + _ = 2 ^ k := by + rw [Nat.card_eq_fintype_card, card_f₂Cube] + have hsign : |(bitSignInt d : ℝ)| = 1 := by + have hmul : (bitSignInt d : ℝ) * (bitSignInt d : ℝ) = 1 := by + exact_mod_cast bitSignInt_mul_self d + have habsmul : |(bitSignInt d : ℝ)| * |(bitSignInt d : ℝ)| = 1 := by + rw [← abs_mul, hmul, abs_one] + nlinarith [abs_nonneg (bitSignInt d : ℝ)] + by_cases hu : u = 0 + · right + rw [himbalance, hrestriction, hu, walshTransform_affineFunction, + if_pos rfl, hcard] + push_cast + rw [abs_mul, hsign] + norm_num + · left + have hzero : (0 : FABL.F₂Cube k) ≠ u := fun h ↦ hu h.symm + rw [IsBalancedOnAffineFlat, himbalance, hrestriction, + walshTransform_affineFunction, if_neg hzero] + norm_num + +private theorem isConstantOrBalancedOnAffineFlat_affineFunction + (d : FABL.𝔽₂) (u : FABL.F₂Cube m) + (H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (b : FABL.F₂Cube m) : + IsConstantOrBalancedOnAffineFlat (FABL.affineFunction d u) H b := by + let e : FABL.F₂Cube (Module.finrank FABL.𝔽₂ H) ≃ₗ[FABL.𝔽₂] H := + LinearEquiv.ofFinrankEq _ _ (by + rw [Module.finrank_fintype_fun_eq_card] + simp) + let c := coordinateRestrictedAffineFrequency H e u + apply isConstantOrBalancedOnAffineFlat_of_coordinate_eq_affineFunction + (FABL.affineFunction d u) H b e (FABL.affineFunction d u b) c + funext y + rw [coordinateAffineSubspaceRestriction_apply] + simpa only [add_comm] using + affineFunction_coordinateAffineSubspaceRestriction H e b u d y + +private def perpendicularCosetPreimageEquiv + (π : Equiv.Perm (FABL.F₂Cube m)) + (L H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) + (hflat : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a ↔ + y ∈ FABL.binaryAffineSubspace H b) : + FABL.perpendicularSubspace L ≃ + {y : FABL.F₂Cube m // y ∈ FABL.binaryAffineSubspace H b} where + toFun v := ⟨π.symm (v.1 + a), (hflat _).1 (by + rw [π.apply_symm_apply, FABL.mem_binaryAffineSubspace_iff_add_mem] + rw [add_assoc, ZModModule.add_self, add_zero] + exact v.2)⟩ + invFun y := ⟨π y.1 + a, by + exact (FABL.mem_binaryAffineSubspace_iff_add_mem _ _ _).1 + ((hflat y.1).2 y.2)⟩ + left_inv v := by + apply Subtype.ext + change π (π.symm (v.1 + a)) + a = v.1 + rw [π.apply_symm_apply, add_assoc, ZModModule.add_self, add_zero] + right_inv y := by + apply Subtype.ext + change π.symm (π y.1 + a + a) = y.1 + rw [add_assoc, ZModModule.add_self, add_zero, π.symm_apply_apply] + +@[simp] private theorem perpendicularCosetPreimageEquiv_apply_coe + (π : Equiv.Perm (FABL.F₂Cube m)) + (L H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) + (hflat : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a ↔ + y ∈ FABL.binaryAffineSubspace H b) + (v : FABL.perpendicularSubspace L) : + (perpendicularCosetPreimageEquiv π L H a b hflat v).1 = + π.symm (v.1 + a) := + rfl + + +private noncomputable def classCCosetEquiv + (π : Equiv.Perm (FABL.F₂Cube m)) + (L H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) + (hflat : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a ↔ + y ∈ FABL.binaryAffineSubspace H b) : + FABL.perpendicularSubspace (blockProductSubspace L ⊤) ≃ H := + (leftBlockPerpendicularLinearEquiv L).symm.toEquiv |>.trans + ((perpendicularCosetPreimageEquiv π L H a b hflat).trans + (affineFlatSubtypeEquiv H b).symm) + +private theorem classCCosetEquiv_apply_add + (π : Equiv.Perm (FABL.F₂Cube m)) + (L H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a b : FABL.F₂Cube m) + (hflat : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a ↔ + y ∈ FABL.binaryAffineSubspace H b) + (q : FABL.perpendicularSubspace (blockProductSubspace L ⊤)) : + (classCCosetEquiv π L H a b hflat q).1 + b = + π.symm (((cubeSplitLinearEquiv m m q.1).1) + a) := by + change + (π.symm + (((leftBlockPerpendicularLinearEquiv L).symm q).1 + a) + b) + b = _ + rw [add_assoc, ZModModule.add_self, add_zero, + leftBlockPerpendicularLinearEquiv_symm_apply_coe] + +private theorem bentDual_booleanMaioranaMcFarlandPermutation_append + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (a b : FABL.F₂Cube m) : + bentDual (booleanMaioranaMcFarlandPermutation π g) (Fin.append a b) = + FABL.f₂DotProduct b (π.symm a) + g (π.symm a) := by + rw [← joinF₂CubeBlocks_eq_append] + exact bentDual_maioranaMcFarlandPermutation + (booleanMaioranaMcFarlandPermutation π g) g π + (booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks π g) a b + +private theorem affineSubspaceRestrictionImbalance_classC_dual + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (L H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (a₁ a₂ b : FABL.F₂Cube m) (d : FABL.𝔽₂) (u : FABL.F₂Cube m) + (hflat : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a₁ ↔ + y ∈ FABL.binaryAffineSubspace H b) + (hg : ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a₁ → + g y = FABL.affineFunction d u y) : + affineSubspaceRestrictionImbalance + (bentDual (booleanMaioranaMcFarlandPermutation π g) + + FABL.affineFunction 0 0) + (FABL.perpendicularSubspace (blockProductSubspace L ⊤)) + (Fin.append a₁ a₂) = + affineSubspaceRestrictionImbalance + (FABL.affineFunction d (u + a₂)) H b := by + classical + let Eperp := FABL.perpendicularSubspace (blockProductSubspace L ⊤) + let Q : Eperp ≃ H := classCCosetEquiv π L H a₁ b hflat + rw [affineSubspaceRestrictionImbalance, + affineSubspaceRestrictionImbalance] + calc + (∑ q : Eperp, + FABL.affineSubspaceRestriction + (realSignView + (bentDual (booleanMaioranaMcFarlandPermutation π g) + + FABL.affineFunction 0 0)) Eperp (Fin.append a₁ a₂) q) = + ∑ q : Eperp, + FABL.affineSubspaceRestriction + (realSignView (FABL.affineFunction d (u + a₂))) H b (Q q) := by + apply Finset.sum_congr rfl + intro q _hq + let v := (leftBlockPerpendicularLinearEquiv L).symm q + let y := π.symm (v.1 + a₁) + have hqcoe : q.1 = Fin.append v.1 0 := by + have h := congrArg + (fun z : Eperp ↦ z.1) + ((leftBlockPerpendicularLinearEquiv L).apply_symm_apply q) + exact h.symm + have hinput : q.1 + Fin.append a₁ a₂ = + Fin.append (v.1 + a₁) a₂ := by + calc + q.1 + Fin.append a₁ a₂ = + Fin.append v.1 0 + Fin.append a₁ a₂ := by rw [hqcoe] + _ = Fin.append (v.1 + a₁) (0 + a₂) := + (finAppend_add v.1 a₁ 0 a₂).symm + _ = Fin.append (v.1 + a₁) a₂ := by rw [zero_add] + have hymem : π y ∈ + FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a₁ := by + change π (π.symm (v.1 + a₁)) ∈ + FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a₁ + rw [π.apply_symm_apply, FABL.mem_binaryAffineSubspace_iff_add_mem] + rw [add_assoc, ZModModule.add_self, add_zero] + exact v.2 + have hvalue : + ((bentDual (booleanMaioranaMcFarlandPermutation π g) : + BooleanFunction (m + m)) + + FABL.affineFunction 0 (0 : FABL.F₂Cube (m + m))) + (q.1 + Fin.append a₁ a₂) = + FABL.affineFunction d (u + a₂) ((Q q).1 + b) := by + rw [hinput, Pi.add_apply, + bentDual_booleanMaioranaMcFarlandPermutation_append, + hg y hymem, classCCosetEquiv_apply_add] + have hv : (cubeSplitLinearEquiv m m q.1).1 = v.1 := by + exact (leftBlockPerpendicularLinearEquiv_symm_apply_coe L q).symm + rw [hv] + change + FABL.f₂DotProduct a₂ y + FABL.affineFunction d u y + + FABL.affineFunction 0 0 (Fin.append (v.1 + a₁) a₂) = + FABL.affineFunction d (u + a₂) y + simp only [FABL.affineFunction, FABL.f₂DotProduct, + add_dotProduct, zero_dotProduct, add_zero] + abel + exact congrArg + (fun c : FABL.𝔽₂ ↦ FABL.signValue (FABL.signEncode c)) hvalue + _ = ∑ x : H, + FABL.affineSubspaceRestriction + (realSignView (FABL.affineFunction d (u + a₂))) H b x := by + exact Equiv.sum_comp Q + (fun x : H ↦ FABL.affineSubspaceRestriction + (realSignView (FABL.affineFunction d (u + a₂))) H b x) + +/-- Every inverse image under `π` of a coset of `Lᵖ` is an affine flat. -/ +def HasAffinePerpendicularCosetPreimages + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : Prop := + ∀ a, ∃ (H : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (b : FABL.F₂Cube m), ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a ↔ + y ∈ FABL.binaryAffineSubspace H b + +/-- The offset function restricts affinely to every inverse image under +`π` of a coset of `Lᵖ`. -/ +def IsAffineOnPerpendicularCosetPreimages + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (g : BooleanFunction m) : Prop := + ∀ a, ∃ (d : FABL.𝔽₂) (u : FABL.F₂Cube m), ∀ y, + π y ∈ FABL.binaryAffineSubspace (FABL.perpendicularSubspace L) a → + g y = FABL.affineFunction d u y + +/-- The zero offset is affine on every perpendicular-coset preimage. -/ +theorem isAffineOnPerpendicularCosetPreimages_zero + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) : + IsAffineOnPerpendicularCosetPreimages π L 0 := by + intro a + refine ⟨0, 0, fun y _hy ↦ ?_⟩ + simp [FABL.affineFunction, FABL.f₂DotProduct, zero_dotProduct] + +/-- Carlet's class `C`, obtained by switching a permutation +Maiorana--McFarland function on `L × V_m`. -/ +noncomputable def classC + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (g : BooleanFunction m) : BooleanFunction (m + m) := + fun z ↦ + let p := cubeSplitLinearEquiv m m z + FABL.f₂DotProduct p.1 (π p.2) + g p.2 + + affineFlatIndicator L 0 p.1 + +@[simp] theorem classC_append + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (g : BooleanFunction m) + (x y : FABL.F₂Cube m) : + classC π L g (Fin.append x y) = + FABL.f₂DotProduct x (π y) + g y + affineFlatIndicator L 0 x := by + rw [classC, cubeSplitLinearEquiv_append] + +private theorem affineFlatIndicator_top_zero + (y : FABL.F₂Cube m) : + affineFlatIndicator (⊤ : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) 0 y = 1 := by + classical + simp [affineFlatIndicator, FABL.mem_binaryAffineSubspace_iff_add_mem] + +private theorem classC_eq_flatSwitch + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (g : BooleanFunction m) : + classC π L g = + flatSwitch (booleanMaioranaMcFarlandPermutation π g) + (blockProductSubspace L ⊤) 0 := by + funext z + let p := cubeSplitLinearEquiv m m z + have hz : Fin.append p.1 p.2 = z := + (Fin.appendEquiv m m).apply_symm_apply z + rw [← hz, classC_append, flatSwitch, Pi.add_apply, + booleanMaioranaMcFarlandPermutation_append, + affineFlatIndicator_blockProduct_append, + affineFlatIndicator_top_zero, mul_one] + +/-- Carlet's class `C` is bent when perpendicular-coset preimages are +affine flats and the offset restricts affinely to each of them. -/ +theorem isBent_classC + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (g : BooleanFunction m) + (hpreimages : HasAffinePerpendicularCosetPreimages π L) + (hoffset : IsAffineOnPerpendicularCosetPreimages π L g) : + IsBent (classC π L g) := by + rw [classC_eq_flatSwitch] + let E := blockProductSubspace L ⊤ + have hbase := isBent_booleanMaioranaMcFarlandPermutation π g + apply (isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced + (booleanMaioranaMcFarlandPermutation π g) hbase E 0).2 + intro a + let p := cubeSplitLinearEquiv m m a + have ha : Fin.append p.1 p.2 = a := + (Fin.appendEquiv m m).apply_symm_apply a + rw [← ha] + obtain ⟨H, b, hflat⟩ := hpreimages p.1 + obtain ⟨d, u, hg⟩ := hoffset p.1 + have himbalance := affineSubspaceRestrictionImbalance_classC_dual + π g L H p.1 p.2 b d u hflat hg + have haffine := isConstantOrBalancedOnAffineFlat_affineFunction + d (u + p.2) H b + have hcard : + Nat.card (FABL.perpendicularSubspace (blockProductSubspace L ⊤)) = + Nat.card H := + Nat.card_congr (classCCosetEquiv π L H p.1 b hflat) + rw [IsConstantOrBalancedOnAffineFlat] at haffine ⊢ + rcases haffine with hbalanced | hconstant + · left + rw [IsBalancedOnAffineFlat] at hbalanced ⊢ + rw [himbalance] + exact hbalanced + · right + rw [himbalance, hcard] + exact hconstant + +/-- The basic class-`C` construction with zero offset. -/ +theorem isBent_classC_zero + (π : Equiv.Perm (FABL.F₂Cube m)) + (L : Submodule FABL.𝔽₂ (FABL.F₂Cube m)) + (hpreimages : HasAffinePerpendicularCosetPreimages π L) : + IsBent (classC π L 0) := + isBent_classC π L 0 hpreimages + (isAffineOnPerpendicularCosetPreimages_zero π L) + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean b/CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean new file mode 100644 index 0000000..425050d --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/SecondarySpecializations.lean @@ -0,0 +1,246 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.DualAffine +public import CryptBoolean.Carlet.Chapter06.SecondaryClasses + +/-! +# Further secondary constructions of bent functions + +Carlet's Maiorana--McFarland bent-family extension and the four-block +construction obtained by switching between the original and class-`D₀` +families. +-/ + +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {m k p q : ℕ} + +/-- The extension of Maiorana--McFarland type indexed by a family of Boolean +functions on an additional coordinate block. -/ +def maioranaMcFarlandBentFamilyExtension + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (h : FABL.F₂Cube m → BooleanFunction k) : + BooleanFunction ((m + m) + k) := + fun u ↦ + let blocks := (Fin.appendEquiv (m + m) k).symm u + let xy := FABL.f₂CubeBlockEquiv m blocks.1 + h xy.2 blocks.2 + booleanMaioranaMcFarlandPermutation π g blocks.1 + +/-- Evaluation of the Maiorana--McFarland bent-family extension on its three +coordinate blocks. -/ +@[simp] theorem maioranaMcFarlandBentFamilyExtension_append + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (h : FABL.F₂Cube m → BooleanFunction k) + (x y : FABL.F₂Cube m) (z : FABL.F₂Cube k) : + maioranaMcFarlandBentFamilyExtension π g h + (Fin.append (FABL.joinF₂CubeBlocks x y) z) = + h y z + FABL.f₂DotProduct x (π y) + g y := by + simp [maioranaMcFarlandBentFamilyExtension, + booleanMaioranaMcFarlandPermutation] + abel + +private theorem firstBlockSlice_maioranaMcFarlandBentFamilyExtension + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (h : FABL.F₂Cube m → BooleanFunction k) (z : FABL.F₂Cube k) : + firstBlockSlice (maioranaMcFarlandBentFamilyExtension π g h) z = + booleanMaioranaMcFarlandPermutation π (fun y ↦ g y + h y z) := by + funext u + let xy := FABL.f₂CubeBlockEquiv m u + have hu : FABL.joinF₂CubeBlocks xy.1 xy.2 = u := + (FABL.f₂CubeBlockEquiv m).symm_apply_apply u + rw [← hu] + simp [firstBlockSlice, + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks] + abel + +/-- If every member of the indexed family is bent, the corresponding +Maiorana--McFarland extension is bent. -/ +theorem isBent_maioranaMcFarlandBentFamilyExtension + (π : Equiv.Perm (FABL.F₂Cube m)) (g : BooleanFunction m) + (h : FABL.F₂Cube m → BooleanFunction k) + (hk : Even k) (hh : ∀ y, IsBent (h y)) : + IsBent (maioranaMcFarlandBentFamilyExtension π g h) := by + let F := maioranaMcFarlandBentFamilyExtension π g h + have hslices : ∀ z, IsBent (firstBlockSlice F z) := by + intro z + dsimp [F] + rw [firstBlockSlice_maioranaMcFarlandBentFamilyExtension] + exact isBent_booleanMaioranaMcFarlandPermutation π + (fun y ↦ g y + h y z) + apply (isBent_iff_forall_isBent_dualSliceFunction + F ⟨m, by omega⟩ hk hslices).2 + intro s + let ab := FABL.f₂CubeBlockEquiv m s + let a := ab.1 + let b := ab.2 + have hs : FABL.joinF₂CubeBlocks a b = s := + (FABL.f₂CubeBlockEquiv m).symm_apply_apply s + let c := FABL.f₂DotProduct b (π.symm a) + g (π.symm a) + have hdual : + dualSliceFunction F s = + h (π.symm a) + FABL.affineFunction c 0 := by + funext z + rw [dualSliceFunction] + dsimp [F] + rw [firstBlockSlice_maioranaMcFarlandBentFamilyExtension, ← hs] + have hformula := bentDual_maioranaMcFarlandPermutation + (booleanMaioranaMcFarlandPermutation π (fun y ↦ g y + h y z)) + (fun y ↦ g y + h y z) π + (fun x y ↦ + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks + π (fun y ↦ g y + h y z) x y) + a b + rw [hformula] + simp [c, FABL.affineFunction, FABL.f₂DotProduct] + abel + rw [hdual] + exact (isBent_add_affineFunction_iff (h (π.symm a)) c 0).2 + (hh (π.symm a)) + +/-- The four-block construction combining two permutation +Maiorana--McFarland terms with a class-`D₀` switch. -/ +def classDZeroFourBlock + (π : Equiv.Perm (FABL.F₂Cube p)) + (ρ : Equiv.Perm (FABL.F₂Cube q)) (h : BooleanFunction q) : + BooleanFunction ((p + p) + (q + q)) := + fun u ↦ + let blocks := (Fin.appendEquiv (p + p) (q + q)).symm u + let xy := FABL.f₂CubeBlockEquiv p blocks.1 + let zt := FABL.f₂CubeBlockEquiv q blocks.2 + FABL.f₂DotProduct xy.1 (π xy.2) + + FABL.f₂DotProduct zt.1 (ρ zt.2) + + FABL.f₂PointIndicator 0 xy.1 * h zt.2 + +/-- Evaluation of the four-block class-`D₀` construction. -/ +@[simp] theorem classDZeroFourBlock_append + (π : Equiv.Perm (FABL.F₂Cube p)) + (ρ : Equiv.Perm (FABL.F₂Cube q)) (h : BooleanFunction q) + (x y : FABL.F₂Cube p) (z t : FABL.F₂Cube q) : + classDZeroFourBlock π ρ h + (Fin.append (FABL.joinF₂CubeBlocks x y) + (FABL.joinF₂CubeBlocks z t)) = + FABL.f₂DotProduct x (π y) + FABL.f₂DotProduct z (ρ t) + + FABL.f₂PointIndicator 0 x * h t := by + simp [classDZeroFourBlock] + +private theorem firstBlockSlice_classDZeroFourBlock + (π : Equiv.Perm (FABL.F₂Cube p)) + (ρ : Equiv.Perm (FABL.F₂Cube q)) (h : BooleanFunction q) + (z t : FABL.F₂Cube q) : + firstBlockSlice (classDZeroFourBlock π ρ h) + (FABL.joinF₂CubeBlocks z t) = + if h t = 0 then + booleanMaioranaMcFarlandPermutation π 0 + + FABL.affineFunction (FABL.f₂DotProduct z (ρ t)) 0 + else + classDZero π + + FABL.affineFunction (FABL.f₂DotProduct z (ρ t)) 0 := by + funext u + let xy := FABL.f₂CubeBlockEquiv p u + have hu : FABL.joinF₂CubeBlocks xy.1 xy.2 = u := + (FABL.f₂CubeBlockEquiv p).symm_apply_apply u + rw [← hu] + by_cases ht : h t = 0 + · rw [if_pos ht] + simp [firstBlockSlice, ht, + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks, + FABL.affineFunction, FABL.f₂DotProduct] + · have htOne : h t = 1 := Fin.eq_one_of_ne_zero _ ht + rw [if_neg ht] + simp only [Pi.add_apply] + have hDZero : + classDZero π (FABL.joinF₂CubeBlocks xy.1 xy.2) = + FABL.f₂DotProduct xy.1 (π xy.2) + + FABL.f₂PointIndicator 0 xy.1 := by + change classDZero π (Fin.append xy.1 xy.2) = _ + exact classDZero_append π xy.1 xy.2 + rw [firstBlockSlice, classDZeroFourBlock_append, hDZero] + rw [htOne, mul_one] + simp [FABL.affineFunction, FABL.f₂DotProduct] + abel + +/-- Carlet's four-block construction is bent for arbitrary Boolean `h` and +arbitrary permutations on the two coordinate pairs. -/ +theorem isBent_classDZeroFourBlock + (π : Equiv.Perm (FABL.F₂Cube p)) + (ρ : Equiv.Perm (FABL.F₂Cube q)) (h : BooleanFunction q) : + IsBent (classDZeroFourBlock π ρ h) := by + let F := classDZeroFourBlock π ρ h + have hslices : ∀ u, IsBent (firstBlockSlice F u) := by + intro u + let zt := FABL.f₂CubeBlockEquiv q u + let z := zt.1 + let t := zt.2 + have hu : FABL.joinF₂CubeBlocks z t = u := + (FABL.f₂CubeBlockEquiv q).symm_apply_apply u + rw [← hu] + dsimp [F] + rw [firstBlockSlice_classDZeroFourBlock] + by_cases ht : h t = 0 + · rw [if_pos ht] + exact (isBent_add_affineFunction_iff + (booleanMaioranaMcFarlandPermutation π 0) + (FABL.f₂DotProduct z (ρ t)) 0).2 + (isBent_booleanMaioranaMcFarlandPermutation π 0) + · rw [if_neg ht] + exact (isBent_add_affineFunction_iff + (classDZero π) (FABL.f₂DotProduct z (ρ t)) 0).2 + (isBent_classDZero π) + apply (isBent_iff_forall_isBent_dualSliceFunction + F ⟨p, by omega⟩ ⟨q, by omega⟩ hslices).2 + intro s + let ab := FABL.f₂CubeBlockEquiv p s + let a := ab.1 + let b := ab.2 + have hs : FABL.joinF₂CubeBlocks a b = s := + (FABL.f₂CubeBlockEquiv p).symm_apply_apply s + let offset : BooleanFunction q := fun t ↦ + FABL.f₂DotProduct b (π.symm a) + + FABL.f₂PointIndicator 0 b * h t + have hdual : + dualSliceFunction F s = + booleanMaioranaMcFarlandPermutation ρ offset := by + funext u + let zt := FABL.f₂CubeBlockEquiv q u + let z := zt.1 + let t := zt.2 + have hu : FABL.joinF₂CubeBlocks z t = u := + (FABL.f₂CubeBlockEquiv q).symm_apply_apply u + rw [← hu, dualSliceFunction, ← hs] + dsimp [F] + rw [firstBlockSlice_classDZeroFourBlock] + by_cases ht : h t = 0 + · rw [if_pos ht, + bentDual_add_constant + (booleanMaioranaMcFarlandPermutation π 0) + (isBent_booleanMaioranaMcFarlandPermutation π 0)] + have hformula := bentDual_maioranaMcFarlandPermutation + (booleanMaioranaMcFarlandPermutation π 0) 0 π + (fun x y ↦ + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks π 0 x y) + a b + rw [hformula] + simp [offset, ht, + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks] + abel + · have htOne : h t = 1 := Fin.eq_one_of_ne_zero _ ht + rw [if_neg ht, + bentDual_add_constant (classDZero π) (isBent_classDZero π)] + rw [show FABL.joinF₂CubeBlocks a b = Fin.append a b from rfl, + bentDual_classDZero_append] + simp [offset, htOne, + booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks] + abel + rw [hdual] + exact isBent_booleanMaioranaMcFarlandPermutation ρ offset + +end CryptBoolean diff --git a/CryptBoolean/Carlet/Chapter06/SupportCode.lean b/CryptBoolean/Carlet/Chapter06/SupportCode.lean index f3a9522..12c48b2 100644 --- a/CryptBoolean/Carlet/Chapter06/SupportCode.lean +++ b/CryptBoolean/Carlet/Chapter06/SupportCode.lean @@ -131,7 +131,9 @@ def SupportCodeHasExactlyTwoNonzeroWeights (f : BooleanFunction n) : Prop := (∃ c : supportCode f, c ≠ 0 ∧ hammingNorm c.1 = first) ∧ (∃ c : supportCode f, c ≠ 0 ∧ hammingNorm c.1 = second) -private theorem finrank_supportCode_eq_n_iff_injective +/-- The support code has full ambient dimension exactly when its defining +linear map is injective. -/ +theorem finrank_supportCode_eq_n_iff_injective (f : BooleanFunction n) : Module.finrank FABL.𝔽₂ (supportCode f) = n ↔ Function.Injective (supportCodeMap f) := by diff --git a/CryptBoolean/Carlet/Chapter06/SupportCodeAlternatives.lean b/CryptBoolean/Carlet/Chapter06/SupportCodeAlternatives.lean new file mode 100644 index 0000000..77d6167 --- /dev/null +++ b/CryptBoolean/Carlet/Chapter06/SupportCodeAlternatives.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2026 Asher Yan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Asher Yan with Codex +-/ +module + +public import CryptBoolean.Carlet.Chapter06.SupportCode + +/-! +# Alternate support-code claims + +Carlet reports two further support-code characterizations after Proposition 16. +Finite four-variable examples show that both converses require hypotheses absent +from the printed statements. +-/ + +open scoped BooleanCube + +@[expose] public section + +namespace CryptBoolean + +variable {n : ℕ} + +/-- The nonzero words of the support code have exactly the two distinct +weights `r` and `s`. -/ +def SupportCodeHasExactlyTwoNonzeroWeightValues + (f : BooleanFunction n) (r s : ℕ) : Prop := + r ≠ s ∧ 0 < r ∧ 0 < s ∧ + (∀ v : FABL.F₂Cube n, supportCodewordWeight f v ≠ 0 → + supportCodewordWeight f v = r ∨ supportCodewordWeight f v = s) ∧ + (∃ v : FABL.F₂Cube n, supportCodewordWeight f v = r) ∧ + ∃ v : FABL.F₂Cube n, supportCodewordWeight f v = s + +/-- The first reported alternative: full dimension and two nonzero weights +whose sum is the code length. -/ +def HasSupportCodeWeightSumAlternative (f : BooleanFunction n) : Prop := + Module.finrank FABL.𝔽₂ (supportCode f) = n ∧ + ∃ r s : ℕ, + SupportCodeHasExactlyTwoNonzeroWeightValues f r s ∧ + r + s = hammingWeight f + +/-- The second reported alternative: even length and two nonzero weights, one +of which is `2^(n-2)`. -/ +def HasSupportCodeEvenLengthQuarterWeightAlternative + (f : BooleanFunction n) : Prop := + Even (hammingWeight f) ∧ + ∃ r s : ℕ, + SupportCodeHasExactlyTwoNonzeroWeightValues f r s ∧ + (r = 2 ^ (n - 2) ∨ s = 2 ^ (n - 2)) + +/-- The complement of one nonzero point in the four-dimensional cube. -/ +def supportCodeWeightSumCounterexample : BooleanFunction 4 := + fun x ↦ if x = ![1, 0, 0, 0] then 0 else 1 + +/-- A nonconstant linear function in the four-dimensional cube. -/ +def supportCodeQuarterWeightCounterexample : BooleanFunction 4 := + fun x ↦ x 2 + x 3 + +private theorem hammingWeight_supportCodeWeightSumCounterexample : + hammingWeight supportCodeWeightSumCounterexample = 15 := by + decide +revert + +private theorem supportCodeMap_supportCodeWeightSumCounterexample_injective : + Function.Injective (supportCodeMap supportCodeWeightSumCounterexample) := by + decide +revert + +private theorem supportCodeWeightSumCounterexample_two_weights : + SupportCodeHasExactlyTwoNonzeroWeightValues + supportCodeWeightSumCounterexample 7 8 := by + rw [SupportCodeHasExactlyTwoNonzeroWeightValues] + decide +revert + +private theorem hammingWeight_supportCodeQuarterWeightCounterexample : + hammingWeight supportCodeQuarterWeightCounterexample = 8 := by + decide +revert + +private theorem supportCodeQuarterWeightCounterexample_two_weights : + SupportCodeHasExactlyTwoNonzeroWeightValues + supportCodeQuarterWeightCounterexample 4 8 := by + rw [SupportCodeHasExactlyTwoNonzeroWeightValues] + decide +revert + +private theorem not_isBent_supportCodeWeightSumCounterexample : + ¬ IsBent supportCodeWeightSumCounterexample := by + intro hf + have hwalsh := natAbs_walshTransform_eq_two_pow_half_of_isBent + supportCodeWeightSumCounterexample hf 0 + rw [walshTransform_zero_eq_two_pow_sub_two_weight, + hammingWeight_supportCodeWeightSumCounterexample] at hwalsh + norm_num at hwalsh + +private theorem not_isBent_supportCodeQuarterWeightCounterexample : + ¬ IsBent supportCodeQuarterWeightCounterexample := by + intro hf + have hwalsh := natAbs_walshTransform_eq_two_pow_half_of_isBent + supportCodeQuarterWeightCounterexample hf 0 + rw [walshTransform_zero_eq_two_pow_sub_two_weight, + hammingWeight_supportCodeQuarterWeightCounterexample] at hwalsh + norm_num at hwalsh + +/-- Full dimension and two distinct nonzero weights summing to the support +size do not characterize bentness without an additional hypothesis. -/ +theorem supportCodeWeightSumAlternative_not_characterize_bent : + HasSupportCodeWeightSumAlternative supportCodeWeightSumCounterexample ∧ + ¬ IsBent supportCodeWeightSumCounterexample := by + refine ⟨⟨?_, 7, 8, supportCodeWeightSumCounterexample_two_weights, ?_⟩, + not_isBent_supportCodeWeightSumCounterexample⟩ + · exact (finrank_supportCode_eq_n_iff_injective _).2 + supportCodeMap_supportCodeWeightSumCounterexample_injective + · rw [hammingWeight_supportCodeWeightSumCounterexample] + +/-- Even length and two distinct nonzero weights including `2^(n-2)` do not +characterize bentness without an additional hypothesis. -/ +theorem supportCodeEvenLengthQuarterWeightAlternative_not_characterize_bent : + HasSupportCodeEvenLengthQuarterWeightAlternative + supportCodeQuarterWeightCounterexample ∧ + ¬ IsBent supportCodeQuarterWeightCounterexample := by + refine ⟨⟨?_, 4, 8, supportCodeQuarterWeightCounterexample_two_weights, ?_⟩, + not_isBent_supportCodeQuarterWeightCounterexample⟩ + · rw [hammingWeight_supportCodeQuarterWeightCounterexample] + exact even_iff_two_dvd.mpr (by norm_num) + · left + norm_num + +end CryptBoolean diff --git a/README.md b/README.md index fe773c1..a4a77ac 100644 --- a/README.md +++ b/README.md @@ -52,14 +52,14 @@ canonical scalar Boolean functions have type `FABL.F₂Cube n → FABL.𝔽₂`. ## Using CryptBoolean -Release `v0.5.0` uses Lean and Mathlib `v4.32.0` and pins FABL `v0.5.6`. Add the package to a +Release `v0.5.1` uses Lean and Mathlib `v4.32.0` and pins FABL `v0.5.6`. Add the package to a downstream `lakefile.toml`: ```toml [[require]] name = "CryptBooleanFunction" git = "https://github.com/Polarnova/CryptBoolean.git" -rev = "v0.5.0" +rev = "v0.5.1" ``` On Linux x86-64 and macOS arm64, obtain the verified release archive with: diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Bentness.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Bentness.lean index 570774e..c9cd35c 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Bentness.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Bentness.lean @@ -6,7 +6,10 @@ Authors: Asher Yan with Codex import Verso import VersoManual import VersoBlueprint +import CryptBoolean.Carlet.Chapter06.HadamardDifferenceSet +import CryptBoolean.Carlet.Chapter06.CayleyGraph import CryptBoolean.Carlet.Chapter06.SupportCode +import CryptBoolean.Carlet.Chapter06.SupportCodeAlternatives import CryptBoolean.Carlet.Chapter06.WalshCongruence open Verso.Genre @@ -44,6 +47,37 @@ $$` Equivalently, $`f` satisfies the propagation criterion of degree $`n`. ::: +:::theorem "carlet-6-hadamard-difference-set-characterizations" (parent := "carlet-chapter-6") (lean := "CryptBoolean.f₂BitWeight, CryptBoolean.hammingNorm_eq_sum_f₂BitWeight, CryptBoolean.hammingNorm_add_restrictSupport_identity, CryptBoolean.bentSignMatrix, CryptBoolean.bentSignMatrix_mul_conjTranspose_apply, CryptBoolean.isBent_iff_bentSignMatrix_isHadamard, CryptBoolean.differenceMultiplicity, CryptBoolean.IsHadamardDifferenceSet, CryptBoolean.differenceMultiplicity_support_eq_hammingNorm_restriction, CryptBoolean.hammingWeight_booleanDerivative_add_two_mul_differenceMultiplicity, CryptBoolean.isBent_iff_support_isHadamardDifferenceSet") (uses := "carlet-6-def-7-bent, carlet-6-theorem-8-perfect-nonlinearity, carlet-2-def-support-weight") (tags := "carlet, chapter-6, page-78, fidelity-exact") +*Hadamard-matrix and difference-set characterizations (Carlet, p. 78).* +Let $`n\ge2` be even and let $`f:V_n\to\mathbb F_2`. The matrix +$$` +H_f(x,y)=(-1)^{f(x+y)} +` +is Hadamard if and only if $`f` is bent. If $`S_f` is the support of +$`f` and +$$` +N_{S_f}(a)=\bigl|\{x\in S_f:x+a\in S_f\}\bigr|, +` +then $`f` is bent if and only if +$$` +|S_f|\ge 2^{n-2} +\quad\text{and}\quad +N_{S_f}(a)=|S_f|-2^{n-2} +\quad(a\ne0). +` +Thus $`S_f` is a Hadamard difference set in the additive group $`V_n`. +::: + +:::theorem "carlet-6-bent-cayley-strongly-regular" (parent := "carlet-chapter-6") (lean := "CryptBoolean.booleanCayleyGraph, CryptBoolean.booleanCayleyGraph_adj, CryptBoolean.card_commonNeighbors_booleanCayleyGraph, CryptBoolean.degree_booleanCayleyGraph, CryptBoolean.isSRGWith_booleanCayleyGraph_of_isBent") (uses := "carlet-6-hadamard-difference-set-characterizations") (tags := "carlet, chapter-6, cayley-graph, page-78, fidelity-exact-explicit-parameters") +*Strong regularity of the Boolean Cayley graph (Carlet, p. 78).* Let +$`n\ge2` be even, let $`f:V_n\to\mathbb F_2` be bent with $`f(0)=0`, and +join distinct $`x,y\in V_n` exactly when $`f(x+y)=1`. If $`S_f` is the +support of $`f`, the resulting graph is strongly regular with parameters +$$` +\left(2^n,\ |S_f|,\ |S_f|-2^{n-2},\ |S_f|-2^{n-2}\right). +` +::: + :::proposition "carlet-6-prop-16-support-code" (parent := "carlet-chapter-6") (lean := "CryptBoolean.supportCodeMap, CryptBoolean.supportCode, CryptBoolean.supportCodewordWeight, CryptBoolean.supportCodewordWeight_zero, CryptBoolean.supportCodewordWeight_eq_card_filter, CryptBoolean.codeCharacterSum_support_eq_card_sub_two_weight, CryptBoolean.four_mul_supportCodewordWeight_eq, CryptBoolean.SupportCodeHasExactlyTwoNonzeroWeights, CryptBoolean.isBent_iff_supportCode_finrank_and_two_nonzero_weights") (uses := "carlet-6-def-7-bent, carlet-4-resiliency-support-dual-distance, carlet-2-balanced-zero-walsh, carlet-2-parseval") (tags := "carlet, chapter-6, proposition-16, pages-78-79, fidelity-corrected-dimension-range") *Proposition 16 (Carlet, pp. 78--79; corrected dimension range).* Let $`n\ge4` be even, let $`S_f=\{u_1,\ldots,u_w\}` be the support of @@ -62,3 +96,17 @@ with both weights occurring. For $`n=2`, every bent function has odd support size, so the second displayed quantity can coincide with zero; the printed positive-even formulation is therefore false in that dimension. + +:::theorem "carlet-6-support-code-alternate-characterizations" (parent := "carlet-chapter-6") (lean := "CryptBoolean.finrank_supportCode_eq_n_iff_injective, CryptBoolean.SupportCodeHasExactlyTwoNonzeroWeightValues, CryptBoolean.HasSupportCodeWeightSumAlternative, CryptBoolean.HasSupportCodeEvenLengthQuarterWeightAlternative, CryptBoolean.supportCodeWeightSumCounterexample, CryptBoolean.supportCodeQuarterWeightCounterexample, CryptBoolean.supportCodeWeightSumAlternative_not_characterize_bent, CryptBoolean.supportCodeEvenLengthQuarterWeightAlternative_not_characterize_bent") (uses := "carlet-6-prop-16-support-code") (tags := "carlet, chapter-6, page-79, fidelity-counterexamples-to-printed-characterizations") +*Alternate support-code characterizations (Carlet, p. 79; correction).* +The two reported converses require additional hypotheses. Indeed, define +$`f_1:V_4\to\mathbb F_2` to vanish at $`(1,0,0,0)` and to equal one +elsewhere. Then $`\dim C_{f_1}=4`, the two nonzero weights of $`C_{f_1}` +are $`7` and $`8`, and +$$` +7+8=w_H(f_1)=15, +` +but $`f_1` is not bent. Also let $`f_2(x)=x_2+x_3` on $`V_4`. Then +$`w_H(f_2)=8` is even, the two nonzero weights of $`C_{f_2}` are $`4` +and $`8`, and $`4=2^{4-2}`, but $`f_2` is not bent. +::: diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Constructions.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Constructions.lean index 8067da8..66c2db3 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Constructions.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Constructions.lean @@ -6,6 +6,8 @@ Authors: Asher Yan with Codex import Verso import VersoManual import VersoBlueprint +import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandBalance +import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandBentSubspace import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandGeneral import CryptBoolean.Carlet.Chapter06.PartialSpreads @@ -15,7 +17,7 @@ open Informal #doc (Manual) "Primary constructions of bent functions" => -:::theorem "carlet-6-maiorana-mcfarland" (parent := "carlet-chapter-6") (lean := "CryptBoolean.isMaioranaMcFarland_of_eq_permutation, CryptBoolean.walshTransform_maioranaMcFarlandPermutation, CryptBoolean.isBent_of_maioranaMcFarlandPermutation, CryptBoolean.bentDual_maioranaMcFarlandPermutation, CryptBoolean.isBent_iff_bijective_maioranaMcFarland") (uses := "carlet-6-def-7-bent, carlet-5-def-maiorana-mcfarland, carlet-5-affine-walsh-spectrum") (tags := "carlet, chapter-6, maiorana-mcfarland, relation-48, pages-83-84, fidelity-exact") +:::theorem "carlet-6-maiorana-mcfarland" (parent := "carlet-chapter-6") (lean := "CryptBoolean.booleanMaioranaMcFarlandPermutation, CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks, CryptBoolean.isMaioranaMcFarland_of_eq_permutation, CryptBoolean.walshTransform_maioranaMcFarlandPermutation, CryptBoolean.isBent_of_maioranaMcFarlandPermutation, CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation, CryptBoolean.bentDual_maioranaMcFarlandPermutation, CryptBoolean.isBent_iff_bijective_maioranaMcFarland") (uses := "carlet-6-def-7-bent, carlet-5-def-maiorana-mcfarland, carlet-5-affine-walsh-spectrum") (tags := "carlet, chapter-6, maiorana-mcfarland, relation-48, pages-83-84, fidelity-exact") *Maiorana--McFarland construction (Carlet, Relation (48), pp. 83--84).* For $`x,y\in V_m`, let $$` @@ -44,6 +46,29 @@ $`s-r` and, when $`r0`, there is an $`m`-dimensional $`\mathbb F_2`-linear +subspace $`B` of the Boolean functions on $`V_{2m}` such that +$$` +f\in B\setminus\{0\}\quad\Longrightarrow\quad f\text{ is bent}. +` +::: + :::theorem "carlet-6-partial-spread-construction" (parent := "carlet-chapter-6") (lean := "CryptBoolean.IsHalfDimensionalPartialSpread, CryptBoolean.HasPartialSpreadBentCardinality, CryptBoolean.partialSpreadFunction, CryptBoolean.partialSpreadCoefficients, CryptBoolean.bitValueInt_partialSpreadFunction_of_ne_zero, CryptBoolean.partialSpreadFunction_zero, CryptBoolean.hasExactGPSRepresentation_partialSpreadFunction, CryptBoolean.isBent_partialSpreadFunction") (uses := "carlet-6-theorem-12-geometric-characterization") (tags := "carlet, chapter-6, partial-spread, pages-85-86, fidelity-exact-positive-half-dimension") *Dillon's partial-spread construction (Carlet, pp. 85--86).* Let $`n` be even with $`n/2\ge2`, and let $`\mathcal P` be a family of diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Counting.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Counting.lean index 0a066d5..6a89b96 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Counting.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Counting.lean @@ -7,6 +7,7 @@ import Verso import VersoManual import VersoBlueprint import CryptBoolean.Carlet.Chapter06.MaioranaMcFarlandCounting +import CryptBoolean.Carlet.Chapter06.PSapCounting open Verso.Genre open Verso.Genre.Manual @@ -14,7 +15,7 @@ open Informal #doc (Manual) "On the number of bent functions" => -:::theorem "carlet-6-maiorana-mcfarland-count" (parent := "carlet-chapter-6") (lean := "CryptBoolean.MaioranaMcFarlandParameters, CryptBoolean.booleanMaioranaMcFarlandPermutation, CryptBoolean.booleanMaioranaMcFarlandPermutation_joinF₂CubeBlocks, CryptBoolean.booleanMaioranaMcFarlandOfParameters, CryptBoolean.booleanMaioranaMcFarlandOfParameters_injective, CryptBoolean.card_maioranaMcFarlandParameters, CryptBoolean.originalMaioranaMcFarlandClass, CryptBoolean.card_originalMaioranaMcFarlandClass, CryptBoolean.isBent_booleanMaioranaMcFarlandPermutation, CryptBoolean.originalMaioranaMcFarlandClass_subset_bentFunctionFamily") (uses := "carlet-6-maiorana-mcfarland") (tags := "carlet, chapter-6, counting, page-97, fidelity-exact") +:::theorem "carlet-6-maiorana-mcfarland-count" (parent := "carlet-chapter-6") (lean := "CryptBoolean.MaioranaMcFarlandParameters, CryptBoolean.booleanMaioranaMcFarlandOfParameters, CryptBoolean.booleanMaioranaMcFarlandOfParameters_injective, CryptBoolean.card_maioranaMcFarlandParameters, CryptBoolean.originalMaioranaMcFarlandClass, CryptBoolean.card_originalMaioranaMcFarlandClass, CryptBoolean.originalMaioranaMcFarlandClass_subset_bentFunctionFamily") (uses := "carlet-6-maiorana-mcfarland") (tags := "carlet, chapter-6, counting, page-97, fidelity-exact") *Number of Maiorana--McFarland functions (Carlet, p. 97).* In dimension $`n=2m`, the original Maiorana--McFarland class contains exactly $$` @@ -23,6 +24,20 @@ $$` distinct bent functions. ::: +:::theorem "carlet-6-psap-count" (parent := "carlet-chapter-6") (lean := "CryptBoolean.PSapParameters, CryptBoolean.card_psapParameters, CryptBoolean.psapOfParameters, CryptBoolean.psapOfParameters_coordinate, CryptBoolean.psapOfParameters_injective, CryptBoolean.psapClass, CryptBoolean.card_psapClass, CryptBoolean.isBent_psapOfParameters_comp_linearEquiv") (uses := "carlet-6-prop-25-psap-hyper-bent, carlet-4-resiliency-support-dual-distance") (tags := "carlet, chapter-6, counting, partial-spread, page-97, fidelity-exact-positive-half-dimension") +*Number of $`PS_{ap}` functions (Carlet, p. 97).* Let $`m\ge2`. With field +division defined at zero, the functions on +$`\mathbb F_{2^m}\times\mathbb F_{2^m}` of the form +$$` +f_g(x,y)=g(x/y), +` +where $`g:\mathbb F_{2^m}\to\mathbb F_2` is balanced, are distinct bent +functions. Their number is +$$` +\binom{2^m}{2^{m-1}}. +` +::: + :::theorem "carlet-6-naive-bent-count-bound" (parent := "carlet-chapter-6") (lean := "CryptBoolean.bentFunctionFamily, CryptBoolean.mem_bentFunctionFamily_iff, CryptBoolean.card_bentFunctionFamily_le_naiveBound") (uses := "carlet-6-prop-18-rothaus-degree-bound, carlet-3-reed-muller-dimension") (tags := "carlet, chapter-6, counting, naive-bound, page-97, fidelity-exact") *Naive upper bound for the number of bent functions (Carlet, p. 97).* If $`n\ge4` is even, then the number $`B_n` of bent functions on $`V_n` diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/DecompositionsCounting.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/DecompositionsCounting.lean index 6ba8f9e..77b456f 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/DecompositionsCounting.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/DecompositionsCounting.lean @@ -6,7 +6,7 @@ Authors: Asher Yan with Codex import Verso import VersoManual import VersoBlueprint -import CryptBoolean.Carlet.Chapter06.HyperplaneRestriction +import CryptBoolean.Carlet.Chapter06.AdditionalDecompositions open Verso.Genre open Verso.Genre.Manual @@ -14,7 +14,7 @@ open Informal #doc (Manual) "Decompositions of bent functions" => -:::theorem "carlet-6-theorem-11-hyperplane-restrictions" (parent := "carlet-chapter-6") (lean := "CryptBoolean.singletonF₂Cube, CryptBoolean.singletonF₂Cube_apply, CryptBoolean.walshTransform_append_singletonF₂Cube, CryptBoolean.linearHyperplaneRestriction, CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.isBent_iff_hasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.hyperplaneExtension, CryptBoolean.hyperplaneExtension_append_singletonF₂Cube, CryptBoolean.linearHyperplaneRestriction_hyperplaneExtension_refl, CryptBoolean.isBent_hyperplaneExtension_of_complementaryWalshSpectra, CryptBoolean.isBent_iff_forall_hasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.isBent_iff_exists_hasComplementaryHyperplaneRestrictionSpectra") (uses := "carlet-2-prop-9-restriction-square, carlet-6-def-7-bent") (tags := "carlet, chapter-6, theorem-11, pages-95-96, fidelity-exact") +:::theorem "carlet-6-theorem-11-hyperplane-restrictions" (parent := "carlet-chapter-6") (lean := "CryptBoolean.singletonF₂Cube, CryptBoolean.singletonF₂Cube_apply, CryptBoolean.singletonF₂CubeLinearEquiv, CryptBoolean.sum_singletonF₂Cube, CryptBoolean.walshTransform_append_singletonF₂Cube, CryptBoolean.linearHyperplaneRestriction, CryptBoolean.HasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.isBent_iff_hasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.hyperplaneExtension, CryptBoolean.hyperplaneExtension_append_singletonF₂Cube, CryptBoolean.linearHyperplaneRestriction_hyperplaneExtension_refl, CryptBoolean.isBent_hyperplaneExtension_of_complementaryWalshSpectra, CryptBoolean.isBent_iff_forall_hasComplementaryHyperplaneRestrictionSpectra, CryptBoolean.isBent_iff_exists_hasComplementaryHyperplaneRestrictionSpectra") (uses := "carlet-2-prop-9-restriction-square, carlet-6-def-7-bent") (tags := "carlet, chapter-6, theorem-11, pages-95-96, fidelity-exact") *Theorem 11 (Carlet, pp. 95--96).* Let $`n\ge4` be even and let $`f:V_n\to\mathbb F_2`. For a linear hyperplane $`E`, identify $`E` and its complementary coset with $`V_{n-1}` and denote the two restrictions by @@ -35,3 +35,22 @@ $$` 2^{n-2}-2^{(n-2)/2}. ` ::: + +:::theorem "carlet-6-balanced-hyperplane-derivative-restrictions" (parent := "carlet-chapter-6") (lean := "CryptBoolean.isBent_linearHyperplaneRestriction_of_balanced_derivatives") (uses := "carlet-6-theorem-11-hyperplane-restrictions, carlet-6-theorem-8-perfect-nonlinearity") (tags := "carlet, chapter-6, decomposition, page-97, fidelity-exact-coordinate-identification") +*Balanced derivatives along a hyperplane (Carlet, p. 97).* Let +$`f:V_{2k+1}\to\mathbb F_2`, and let $`E` be a linear hyperplane. If +$`D_u f` is balanced for every nonzero $`u\in E`, then the restrictions of +$`f` to $`E` and to its complementary coset are bent. +::: + +:::theorem "carlet-6-codimension-two-restrictions" (parent := "carlet-chapter-6") (lean := "CryptBoolean.four_mul_walshTransform_firstBlockSlice_eq, CryptBoolean.walshMagnitudeSet, CryptBoolean.walshMagnitudeSet_firstBlockSlice_eq, CryptBoolean.isBent_firstBlockSlices_iff_bentDual_secondDerivative_eq_one") (uses := "carlet-6-theorem-10-slice-construction, carlet-6-dual, carlet-6-quadratic-bent-characterization, carlet-6-prop-24-second-order-characterization") (tags := "carlet, chapter-6, decomposition, page-97, fidelity-exact-coordinate-identification") +*Restrictions to four codimension-two cosets (Carlet, p. 97).* Let $`f` be +bent on $`V_N`, with $`N` even, and let $`E\le V_N` have codimension two. +The four restrictions of $`f` to the cosets of $`E`, viewed in any fixed +linear coordinate identification with $`V_{N-2}`, have the same set of +Walsh magnitudes. If $`E^\perp=\langle a,b\rangle`, then all four +restrictions are bent if and only if +$$` +D_aD_b\widetilde f=1. +` +::: diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Duality.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Duality.lean index 175a829..4f57786 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Duality.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/Duality.lean @@ -46,7 +46,7 @@ d_H(\widetilde f,\widetilde g)=d_H(f,g), so duality preserves pairwise Hamming distance on bent functions. ::: -:::theorem "carlet-6-rel-45-dual-derivatives" (parent := "carlet-chapter-6") (lean := "CryptBoolean.isBent_domainTranslate, CryptBoolean.isBent_domainTranslate_add_linear, CryptBoolean.bentDual_domainTranslate_add_linear, CryptBoolean.walshTransform_zero_bentDual_derivative_add_linear") (uses := "carlet-6-dual, carlet-6-rel-44-dual-isometry, carlet-2-prop-6-fourier-shifts, carlet-2-def-2-derivative") (tags := "carlet, chapter-6, duality, relation-45, pages-79-80, fidelity-exact") +:::theorem "carlet-6-rel-45-dual-derivatives" (parent := "carlet-chapter-6") (lean := "CryptBoolean.isBent_domainTranslate, CryptBoolean.isBent_domainTranslate_add_linear, CryptBoolean.bentDual_domainTranslate_add_linear, CryptBoolean.bentDual_add_constant, CryptBoolean.walshTransform_zero_bentDual_derivative_add_linear") (uses := "carlet-6-dual, carlet-6-rel-44-dual-isometry, carlet-2-prop-6-fourier-shifts, carlet-2-def-2-derivative") (tags := "carlet, chapter-6, duality, relation-45, pages-79-80, fidelity-exact") *Relation (45) (Carlet, pp. 79--80).* Let $`f:V_n\to\mathbb F_2` be bent and let $`a,b\in V_n`. The function $$` diff --git a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/SecondaryConstructions.lean b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/SecondaryConstructions.lean index 057ad06..be23cd3 100644 --- a/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/SecondaryConstructions.lean +++ b/blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter06/SecondaryConstructions.lean @@ -11,6 +11,8 @@ import CryptBoolean.Carlet.Chapter06.FlatSwitching import CryptBoolean.Carlet.Chapter06.IndirectSum import CryptBoolean.Carlet.Chapter06.PermutationReindex import CryptBoolean.Carlet.Chapter06.Rothaus +import CryptBoolean.Carlet.Chapter06.SecondaryClasses +import CryptBoolean.Carlet.Chapter06.SecondarySpecializations open Verso.Genre open Verso.Genre.Manual @@ -39,7 +41,7 @@ gh+gk+hk+(g+h)x_1+(g+k)x_2+x_1x_2 is bent. ::: -:::theorem "carlet-6-theorem-9-flat-switching" (parent := "carlet-chapter-6") (lean := "CryptBoolean.flatSwitch, CryptBoolean.IsBalancedOnAffineFlat, CryptBoolean.IsConstantOrBalancedOnAffineFlat, CryptBoolean.affineFlatWalshSum, CryptBoolean.walshTransform_sub_flatSwitch, CryptBoolean.affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction, CryptBoolean.affineSubspaceRestrictionImbalance_bentDual_add_linear, CryptBoolean.abs_affineSubspaceRestrictionImbalance_bentDual_add_linear, CryptBoolean.autocorrelation_flatSwitch, CryptBoolean.isBent_flatSwitch_iff_derivative_balanced_on_affineFlat, CryptBoolean.isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced, CryptBoolean.derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_balanced, CryptBoolean.two_pow_half_dvd_walshTransform_affineFlatRestriction, CryptBoolean.half_dimension_le_finrank_of_isBent_flatSwitch, CryptBoolean.functionAlgebraicDegree_affineFlatRestriction_le_of_isBent_flatSwitch, CryptBoolean.isBent_flatSwitch_of_half_dimension_of_restriction_degree_le_one") (uses := "carlet-6-theorem-8-perfect-nonlinearity, carlet-6-rel-46-dual-poisson, carlet-2-prop-11-walsh-divisibility, carlet-3-prop-12") (tags := "carlet, chapter-6, theorem-9, pages-90-91, fidelity-exact") +:::theorem "carlet-6-theorem-9-flat-switching" (parent := "carlet-chapter-6") (lean := "CryptBoolean.flatSwitch, CryptBoolean.IsBalancedOnAffineFlat, CryptBoolean.IsConstantOrBalancedOnAffineFlat, CryptBoolean.affineFlatWalshSum, CryptBoolean.affineFlatSubtypeEquiv, CryptBoolean.walshTransform_sub_flatSwitch, CryptBoolean.affineFlatWalshSum_eq_bitSignInt_mul_walshTransform_restriction, CryptBoolean.affineSubspaceRestrictionImbalance_bentDual_add_linear, CryptBoolean.abs_affineSubspaceRestrictionImbalance_bentDual_add_linear, CryptBoolean.autocorrelation_flatSwitch, CryptBoolean.isBent_flatSwitch_iff_derivative_balanced_on_affineFlat, CryptBoolean.isBent_flatSwitch_iff_bentDual_add_linear_constant_or_balanced, CryptBoolean.derivative_balanced_on_affineFlat_iff_bentDual_add_linear_constant_or_balanced, CryptBoolean.bitSignInt_mul_self, CryptBoolean.two_pow_half_dvd_walshTransform_affineFlatRestriction, CryptBoolean.half_dimension_le_finrank_of_isBent_flatSwitch, CryptBoolean.functionAlgebraicDegree_affineFlatRestriction_le_of_isBent_flatSwitch, CryptBoolean.isBent_flatSwitch_of_half_dimension_of_restriction_degree_le_one") (uses := "carlet-6-theorem-8-perfect-nonlinearity, carlet-6-rel-46-dual-poisson, carlet-2-prop-11-walsh-divisibility, carlet-3-prop-12") (tags := "carlet, chapter-6, theorem-9, pages-90-91, fidelity-exact") *Theorem 9 (Carlet, pp. 90--91).* Let $`f` be bent on $`V_n`, let $`b+E` be an affine flat, and put $`f^*=f+\mathbf1_{b+E}`. Then $`f^*` is bent if and only if either of the following equivalent conditions holds: @@ -54,7 +56,44 @@ $`\dim E-n/2+1`. Conversely, if $`\dim E=n/2` and that restriction is affine, then $`f^*` is bent. ::: -:::theorem "carlet-6-theorem-10-slice-construction" (parent := "carlet-chapter-6") (lean := "CryptBoolean.firstBlockSlice, CryptBoolean.dualSliceFunction, CryptBoolean.walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction, CryptBoolean.isBent_iff_forall_isBent_dualSliceFunction, CryptBoolean.bentDual_append_eq_bentDual_dualSliceFunction") (uses := "carlet-6-def-7-bent, carlet-6-dual") (tags := "carlet, chapter-6, theorem-10, pages-91-92, fidelity-exact") +:::theorem "carlet-6-class-d-zero" (parent := "carlet-chapter-6") (lean := "CryptBoolean.classDZero, CryptBoolean.classDZero_append, CryptBoolean.walshTransform_classDZero, CryptBoolean.isBent_classDZero, CryptBoolean.bentDual_classDZero_append") (uses := "carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching") (tags := "carlet, chapter-6, class-d-zero, pages-90-91, fidelity-exact") +*Class $`D_0` (Carlet, pp. 90--91).* Let $`\pi` be a permutation of +$`V_m`. The function +$$` +f(x,y)=x\mathbin\cdot\pi(y)+\delta_0(x) +` +is bent on $`V_m\times V_m`, and its dual is +$$` +\widetilde f(a,b)=b\mathbin\cdot\pi^{-1}(a)+\delta_0(b). +` +::: + +:::theorem "carlet-6-class-d" (parent := "carlet-chapter-6") (lean := "CryptBoolean.classD, CryptBoolean.classD_append, CryptBoolean.isBent_classD") (uses := "carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching") (tags := "carlet, chapter-6, class-d, pages-90-91, fidelity-exact") +*Class $`D` (Carlet, pp. 90--91).* Let $`E_1,E_2` be subspaces of +$`V_m` and let $`\pi` be a permutation such that +$`\pi(E_2)=E_1^\perp`. Then +$$` +f(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_{E_1}(x)\mathbf 1_{E_2}(y) +` +is bent on $`V_m\times V_m`. +::: + +:::theorem "carlet-6-class-c" (parent := "carlet-chapter-6") (lean := "CryptBoolean.HasAffinePerpendicularCosetPreimages, CryptBoolean.IsAffineOnPerpendicularCosetPreimages, CryptBoolean.isAffineOnPerpendicularCosetPreimages_zero, CryptBoolean.classC, CryptBoolean.classC_append, CryptBoolean.isBent_classC, CryptBoolean.isBent_classC_zero") (uses := "carlet-6-maiorana-mcfarland, carlet-6-theorem-9-flat-switching") (tags := "carlet, chapter-6, class-c, pages-90-91, fidelity-exact") +*Class $`C` (Carlet, pp. 90--91).* Let $`L` be a subspace of $`V_m` +and let $`\pi` be a permutation such that every set +$`\pi^{-1}(a+L^\perp)` is an affine flat. Then +$$` +f(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_L(x) +` +is bent. More generally, +$$` +f_g(x,y)=x\mathbin\cdot\pi(y)+\mathbf 1_L(x)+g(y) +` +is bent whenever the restriction of $`g` to every +$`\pi^{-1}(a+L^\perp)` is affine. +::: + +:::theorem "carlet-6-theorem-10-slice-construction" (parent := "carlet-chapter-6") (lean := "CryptBoolean.finAppend_add, CryptBoolean.firstBlockSlice, CryptBoolean.secondBlockSlice, CryptBoolean.walshTransform_append_cast_eq_rawFourierTransform_sliceWalsh, CryptBoolean.dualSliceFunction, CryptBoolean.walshTransform_eq_two_pow_half_mul_walshTransform_dualSliceFunction, CryptBoolean.isBent_iff_forall_isBent_dualSliceFunction, CryptBoolean.bentDual_append_eq_bentDual_dualSliceFunction") (uses := "carlet-6-def-7-bent, carlet-6-dual") (tags := "carlet, chapter-6, theorem-10, pages-91-92, fidelity-exact") *Theorem 10 (Carlet, pp. 91--92).* Let $`n,m` be even and let $`f:V_n\times V_m\to\mathbb F_2`. Suppose every slice $`f_y(x)=f(x,y)` is bent, and define $`\varphi_s(y)=\widetilde{f_y}(s)`. @@ -74,6 +113,27 @@ is bent. Its dual is obtained by applying the same formula to the four duals. ::: +:::theorem "carlet-6-maiorana-mcfarland-bent-family-extension" (parent := "carlet-chapter-6") (lean := "CryptBoolean.maioranaMcFarlandBentFamilyExtension, CryptBoolean.maioranaMcFarlandBentFamilyExtension_append, CryptBoolean.isBent_maioranaMcFarlandBentFamilyExtension") (uses := "carlet-6-theorem-10-slice-construction, carlet-6-maiorana-mcfarland") (tags := "carlet, chapter-6, secondary-construction, page-93, fidelity-exact") +*Maiorana--McFarland bent-family extension (Carlet, p. 93).* Let $`\pi` be a +permutation of $`V_r`, let $`g:V_r\to\mathbb F_2`, and let +$`(h_y)_{y\in V_r}` be a family of bent functions on $`V_m`, where $`m` is +even. Then +$$` +F(x,y,z)=h_y(z)+x\mathbin\cdot\pi(y)+g(y) +` +is bent on $`V_r\times V_r\times V_m`. +::: + +:::theorem "carlet-6-class-d-zero-four-block" (parent := "carlet-chapter-6") (lean := "CryptBoolean.classDZeroFourBlock, CryptBoolean.classDZeroFourBlock_append, CryptBoolean.isBent_classDZeroFourBlock") (uses := "carlet-6-theorem-10-slice-construction, carlet-6-maiorana-mcfarland, carlet-6-class-d-zero") (tags := "carlet, chapter-6, secondary-construction, page-93, fidelity-strengthened-zero-dimensional") +*Four-block class-$`D_0` construction (Carlet, p. 93).* Let $`r,s` be +positive, let $`\pi` and $`\pi'` be permutations of $`V_r` and $`V_s`, +respectively, and let $`h:V_s\to\mathbb F_2` be arbitrary. Then +$$` +F(x,y,z,t)=x\mathbin\cdot\pi(y)+z\mathbin\cdot\pi'(t)+\delta_0(x)h(t) +` +is bent on $`V_r\times V_r\times V_s\times V_s`. +::: + :::proposition "carlet-6-prop-21-permutation-reindexing" (parent := "carlet-chapter-6") (lean := "CryptBoolean.hammingDistance_comp_perm, CryptBoolean.hammingDistance_comp_perm_symm_linearFunction, CryptBoolean.walshTransform_comp_perm_symm_eq_two_pow_sub_two_hammingDistance, CryptBoolean.isBent_comp_perm_symm_of_hammingDistance") (uses := "carlet-6-def-7-bent, carlet-2-def-hamming-distance") (tags := "carlet, chapter-6, proposition-21, pages-93-94, fidelity-exact") *Proposition 21 (Carlet, pp. 93--94).* Let $`\sigma` be a permutation of $`V_n`, with coordinate functions $`\sigma_1,\ldots,\sigma_n`. If diff --git a/blueprint-verso/scripts/check_statement_style.py b/blueprint-verso/scripts/check_statement_style.py index ad6f958..6c9c5c9 100644 --- a/blueprint-verso/scripts/check_statement_style.py +++ b/blueprint-verso/scripts/check_statement_style.py @@ -119,9 +119,9 @@ def main() -> None: errors.append(f"{location}: {block.identifier} must have {expected}, but not both") formalized = sum("(lean :=" in block.header for block in blocks) open_count = sum("source-open" in block.header for block in blocks) - if (len(blocks), formalized, open_count) != (209, 206, 3): + if (len(blocks), formalized, open_count) != (222, 219, 3): errors.append( - "expected 209 statements split into 206 formalized and 3 open; " + "expected 222 statements split into 219 formalized and 3 open; " f"found {len(blocks)}, {formalized}, and {open_count}" ) if errors: diff --git a/blueprint-verso/scripts/validate_manifest.py b/blueprint-verso/scripts/validate_manifest.py index 4b34a28..9d895f9 100755 --- a/blueprint-verso/scripts/validate_manifest.py +++ b/blueprint-verso/scripts/validate_manifest.py @@ -8,23 +8,23 @@ from pathlib import Path -EXPECTED_STATEMENTS = 209 -EXPECTED_FORMALIZED = 206 -EXPECTED_DECLARATIONS = 1338 -EXPECTED_EDGES = 467 +EXPECTED_STATEMENTS = 222 +EXPECTED_FORMALIZED = 219 +EXPECTED_DECLARATIONS = 1418 +EXPECTED_EDGES = 493 EXPECTED_CHAPTERS = { "chapter-2": 41, "chapter-3": 7, "chapter-4": 73, "chapter-5": 31, - "chapter-6": 57, + "chapter-6": 70, } EXPECTED_GROUPS = { "«carlet-chapter-2»": 41, "«carlet-chapter-3»": 7, "«carlet-chapter-4»": 73, "«carlet-chapter-5»": 31, - "«carlet-chapter-6»": 57, + "«carlet-chapter-6»": 70, } EXPECTED_OPEN = { "carlet-5-theorem-7-weil-bound", diff --git a/lakefile.lean b/lakefile.lean index f87419b..557b704 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,7 +5,7 @@ open Lake DSL require FABL from git "https://github.com/Polarnova/FABL.git" @ "v0.5.6" package CryptBooleanFunction where - version := v!"0.5.0" + version := v!"0.5.1" description := "Cryptographic Boolean Functions in Lean" keywords := #["mathematics", "boolean-functions", "cryptography", "formalization"] license := "Apache-2.0"