recognitionThetaModularIdentity_of_prefactor
plain-language theorem explainer
The definition supplies a direct constructor turning a continuous prefactor ρ satisfying the inversion relation θ(1/t) = ρ(t) θ(t) for t > 0 into the RecognitionThetaModularIdentity structure. Number theorists tracking sub-conjecture A.2 on the RS theta modular identity would cite it when bridging prefactor data to the identity. The proof is a one-line wrapper applying the equivalence recognitionThetaModularIdentity_iff_prefactor.mpr to the input structure.
Claim. Let θ be the recognition theta function. Given a continuous function ρ : ℝ → ℝ such that θ(1/t) = ρ(t) ⋅ θ(t) for all t > 0, the data (ρ, θ) determines the modular identity structure.
background
The module RecognitionTheta/ModularIdentity.lean tracks sub-conjecture A.2. The RS theta modular identity requires a Poisson-summation theorem for the phi-ladder / 8-tick theta kernel, but the project lacks the required lattice package; the module therefore pins the exact interface. RecognitionThetaPrefactor is the structure consisting of a continuous map ρ : ℝ → ℝ together with the inversion property ∀ t > 0, recognitionTheta(1/t) = ρ t ⋅ recognitionTheta t. The module doc states that this prefactor data is exactly the RecognitionThetaModularIdentity structure.
proof idea
One-line wrapper that applies recognitionThetaModularIdentity_iff_prefactor.mpr to the input RecognitionThetaPrefactor, packaging it as the required structure.
why it matters
This supplies the constructor field of recognitionThetaModularAttackSurface, which records the current attack surface for A.2. It fills the modular-identity bridge in the Recognition Science framework, linking to the phi-ladder and eight-tick octave. The open question remains the Poisson-summation construction of the prefactor itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.