T
plain-language theorem explainer
Breath1024 introduces T as the type of natural numbers to index fundamental periods. Researchers constructing discrete-time structures such as period-8 and period-1024 objects cite this abbreviation when assembling the eight-tick octave and related counting arguments. The declaration is a direct type abbreviation with no computational content or lemmas.
Claim. Let $T$ denote the type of natural numbers.
background
The Breath1024 module supplies the discrete time carrier for fundamental periods. Sibling declarations include period8, period1024, flipTick, sum8, neutral8, Osc, flipAt512, and phaseLagPiOver4, all built on this carrier. The module imports Mathlib and depends on the upstream triangular-number definition whose doc-comment states: 'The n-th triangular number: T(n) = n(n+1)/2.'
proof idea
The declaration is a one-line abbreviation that directly sets T to the natural-numbers type. No lemmas are applied and no tactics are used.
why it matters
This type anchors forty downstream results, including space-translation invariance implying momentum conservation, the quadratic leading coefficient of Jcost, Newton's first law, narrative geodesic certificates, and Arrhenius rate constants. It supplies the discrete index required by the eight-tick octave (T7) and the 1024-period constructions in the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.