recognitionThetaModularIdentity_of_prefactor
plain-language theorem explainer
The definition supplies a constructor converting a continuous prefactor obeying the inversion relation for the recognition theta function into the modular identity data structure. Number theorists working on Recognition Science sub-conjecture A.2 would cite it when assembling the attack surface. The proof is a one-line wrapper applying the reverse direction of the equivalence between prefactors and modular identities.
Claim. Let $p$ be a continuous function $ρ:ℝ→ℝ$ such that $∀t>0$, $Θ(1/t)=ρ(t)⋅Θ(t)$ where $Θ$ is the recognition theta function. Then $p$ determines the modular identity structure for $Θ$.
background
The module tracks sub-conjecture A.2 for the recognition theta modular identity. Recognition Science requires a Poisson-summation theorem for the phi-ladder and 8-tick theta kernel, but Mathlib lacks the needed special lattice package. The module therefore pins the interface: a continuous prefactor satisfying the inversion identity is exactly the RecognitionThetaModularIdentity structure. The RecognitionThetaPrefactor structure consists of a continuous real-valued function ρ together with the inversion property that recognitionTheta(1/t) equals ρ(t) times recognitionTheta(t) for all t>0.
proof idea
This is a one-line wrapper that applies the reverse direction of the equivalence theorem recognitionThetaModularIdentity_iff_prefactor, packing the supplied prefactor data into the target structure.
why it matters
This constructor completes the modular-identity bridge and feeds directly into the attack-surface definition for sub-conjecture A.2. It lets downstream code treat any qualifying continuous prefactor as the required modular identity without the full Poisson-summation construction. In the Recognition Science framework the result sits inside the phi-ladder and 8-tick octave setting for the theta kernel; the open question remains the explicit Poisson-summation construction of the prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.