Mechanism Map
A guide to the recurring proof patterns in Tensorgami.
Guide
The archive is broad by subject because the same proof mechanisms appear in many mathematical settings.
Tensorgami is a public mathematical workbench for making proof mechanisms explicit. Some entries record arguments, extraction formulas, finite certificates, or Lean-checked statements; others rebuild familiar or standard results in concrete, algorithmic, inspectable form.
Many notes look for coordinates in which the theorem becomes rigid: residue expansions, standard monomials, compact decompositions, canonical representatives, or other normal forms where the obstruction can be seen directly.
Abstract existence statements are often replaced by terminating procedures, extraction formulas, finite certificates, or explicit computations. The point is not only that an object exists, but how it can be recovered.
A recurring pattern is to isolate the exceptional configurations that prevent cancellation, expansion, divisibility, or approximation, then prove that these are the only obstructions. Once the bad cases are controlled, the theorem becomes rigid.
Qualitative arguments are often converted into finite, inspectable, or bounded versions: estimates, finite partitions, degree control, norming sets, computable constants, and explicit reductions.
Several entries study when compatibility on fibers, overlaps, quotients, diagonals, or correspondences forces a global object to descend from a simpler base, factor through a common map, or collapse to a more rigid form.
Lean is used selectively as a second layer of inspection. It is most useful when the formalized statement clarifies the proof architecture or certifies a delicate final claim; it is not the primary identity of the site.