Toroidal Provenance Cut

Abstract

A selected nonzero twist makes period vanishing equivalent to base vanishing.

Theorem 1.1 (A nonzero twist separates base zeros from twist zeros).

$$\forall Index\in \mathrm{Type}\left(\right),Point\in \mathrm{Type}\left(\right),Scalar\in \mathrm{Type}\left(\right),indexDecision\in \mathrm{DecidableEq}\left(Index\right),scalarDecision\in \mathrm{DecidableEq}\left(Scalar\right),mulZero\in \mathrm{MulZeroClass}\left(Scalar\right),noZeroDivisors\in \mathrm{NoZeroDivisors}\left(Scalar\right),selected\in \mathrm{Finset}\left(Index\right),period\in Index\to \left(Point\to Scalar\right),twist\in Index\to \left(Point\to Scalar\right),base\in Point\to Scalar,s\in Point,i\in Index,\left(\mathrm{mem}\left(i,selected\right)\wedge \left(period\left(i\right)\left(s\right)=base\left(s\right)\times twist\left(i\right)\left(s\right)\wedge twist\left(i\right)\left(s\right)\ne 0\right)\right)\Rightarrow \left(\left(\mathrm{mem}\left(i,\mathrm{periodZero}\left(\mathrm{toroidalVanishingProfile}\left(selected,period,twist,s\right)\right)\right)\iff base\left(s\right)=0\right)\wedge \left(\neg \mathrm{mem}\left(i,\mathrm{twistZero}\left(\mathrm{toroidalVanishingProfile}\left(selected,period,twist,s\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Toroidal/ToroidalProvenanceCut.toroidal_provenance_cut (✓ std3). ∎

Source. Repository-derived.

Commentary.

The profile retains the selected finite index set and filters it twice at the chosen point: once by period vanishing and once by twist vanishing. The theorem earns that profile definition by giving its per-index membership cut under the displayed factorization.

This result is distinct from ToroidalCommonZeroLocus, ToroidalObserverSetCover, ToroidalTemperednessCriterion, and ToroidalJetDepth. Those neighbouring modules concern global, observer, or jet statements; they are context rather than dependencies of this Mathlib-generic cut.

The nonzero-twist certificate is the C-5 chart-selection precondition: a chart must be chosen where twist is nonzero before projective jet normalization. The same provenance distinction supplies the A-R5 residual cut between a base zero and a twist zero.

References

• Truth anchor: D5/S3/Analytic/Toroidal/ToroidalProvenanceCut.toroidal_provenance_cut