recognitionThetaModularIdentity_iff_prefactor
plain-language theorem explainer
The equivalence shows that the Recognition Theta modular identity holds precisely when a continuous prefactor structure satisfying the inversion relation exists. Researchers tracking sub-conjecture A.2 would cite this to equate the existential Prop with packaged prefactor data. The term-mode proof splits the biconditional via constructor and uses rcases to move between the existential witness and the structure.
Claim. The proposition asserting existence of a continuous function $ρ : ℝ → ℝ$ such that recognitionTheta$(1/t) = ρ(t) ·$ recognitionTheta$(t)$ for all $t > 0$ is equivalent to the nonemptiness of the RecognitionThetaPrefactor structure.
background
The module tracks sub-conjecture A.2 for the Recognition Theta function on the phi-ladder. RecognitionThetaModularIdentity is the Prop packaging the claim that a continuous prefactor exists satisfying the inversion identity under $t ↦ 1/t$. RecognitionThetaPrefactor is the sibling structure that records the same data explicitly as a ρ field together with proofs of continuity and the inversion equation. The module doc states that this pins the exact interface needed because Mathlib lacks the special lattice package for the 8-tick theta kernel.
proof idea
Term-mode proof applies constructor to split the biconditional. Forward direction rcases the prefactor existential inside RecognitionThetaModularIdentity and builds the structure record. Reverse direction rcases the Nonempty witness and repacks the three fields into the existential inside the Prop.
why it matters
The result supplies the bridge used by recognitionThetaModularAttackSurface and recognitionThetaModularIdentity_of_prefactor. It fills the interface step for sub-conjecture A.2 inside the RecognitionTheta module. The equivalence lets downstream code treat the modular identity as either an abstract existence claim or concrete prefactor data while the project develops the required Poisson summation for the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.