Tensorgami

Verification

Verified work

Selected Tensorgami notes with theorem names, Lean source, and automated checks.

Guide

What is checked

Lean is used selectively when the formal statement clarifies or certifies a proof mechanism.

New construction Analysis

A Weighting Argument for Pointwise Convergence to Convergence in Measure

Measurable-weight construction turning pointwise or almost-everywhere convergence to zero into uniform convergence on a conull set, and hence convergence in measure.

Contribution
New measurable-weight construction and Lean-checked sigma-finite formulation.
Mechanism
Egorov pieces, pointwise envelope, measurable cover-index weight, convergence in measure
Lean theorem
PointwiseWeighting.exists_conull_pos_measurable_weight_uniformOn_tendstoInMeasure_of_ae_tendsto
Real-line theorem
PointwiseWeighting.real_exists_conull_pos_measurable_weight_uniformOn_tendstoInMeasure
Note page PDF Lean source Lean check

Independent solution Number theory

IBM Ponder This July 2010

Trace and companion-matrix certificate for the challenge of forcing 10^9 to divide the rounded power of 1 + 2 cos 20 deg.

Contribution
Independent trace and companion-matrix solution with a finite modular certificate verified in Lean.
Mechanism
Pisot rounding, trace recurrence, companion-matrix period, finite modular certificate
Lean theorem
IBMPonderThisFinal.ibm_ponder_this_main
Note page PDF Lean source Lean check

New argument Algebra

Divisibility of Separated Polynomials

Criterion for when f(X)-g(Y) divides p(X)-q(Y), showing that p and q descend through a common outer polynomial.

Contribution
Common-outer-polynomial criterion proved through a residue-expansion and diagonal-reduction mechanism.
Mechanism
free-module residue expansion, diagonal collapse, descent
Lean theorem
SeparatedPolynomialDifferences.sep_dvd_iff_exists_common_outer
Note page PDF Lean source Lean check

New viewpoint Algebra

A Galois-Theoretic and Frobenius-Descent Viewpoint on a Polynomial Composition Law

Companion proof of a separated-polynomial composition criterion using generic fibers, Galois descent, Frobenius reduction, and a cubic square-root functional equation.

Contribution
Galois-descent and Frobenius-reduction viewpoint on the separated-composition criterion.
Mechanism
generic fibers, splitting fields, Frobenius descent
Lean theorem family
SeparatedComposition.separated_composition_criterion_iff
Note page PDF Lean source Lean check

New construction Number theory

Extracting the First Prime Greater than m

Finite arithmetic extraction formula returning the least prime above m for every natural number m >= 3.

Contribution
Explicit finite extraction formula for the least prime above m, verified in Lean.
Mechanism
gcd filtering, valuation selection, finite certificate
Lean theorem
ExtractingFirstPrime.extractedPrime_is_smallest_prime_gt
Note page PDF Lean source Lean check

Independent solution Analysis

A Note on Disjoint Decompositions of [0,1) into Closed Sets

Proof that the half-open interval cannot be written as a countable disjoint union of closed subsets of the real line.

Contribution
Independent proof of the non-decomposition result via endpoint obstruction and Baire category, with the final statement formalized in Lean.
Mechanism
compactification, boundary obstruction, Baire category
Lean theorem
no_pairwiseDisjoint_closed_iUnion_eq_Ico
Note page PDF Lean source Lean check