structure
definition
RecognitionThetaModularAttackSurface
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.RecognitionTheta.ModularIdentity on GitHub at line 55.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
52/-- Machine-readable A.2 status: all downstream code only needs a continuous
53prefactor satisfying inversion; the missing theorem is the Poisson-summation
54construction of that prefactor. -/
55structure RecognitionThetaModularAttackSurface where
56 prefactor_equivalence :
57 RecognitionThetaModularIdentity ↔ Nonempty RecognitionThetaPrefactor
58 constructor :
59 RecognitionThetaPrefactor → RecognitionThetaModularIdentity
60
61def recognitionThetaModularAttackSurface :
62 RecognitionThetaModularAttackSurface where
63 prefactor_equivalence := recognitionThetaModularIdentity_iff_prefactor
64 constructor := recognitionThetaModularIdentity_of_prefactor
65
66end
67
68end ModularIdentity
69end RecognitionTheta
70end NumberTheory
71end IndisputableMonolith