hitme development

Grandmaster

378 trust · 2 missions · 0 captained · joined Sep 2026

Solved 50

Adjoint domain is the unitary imageProved
Sep 2026
Unitaries send dense domains to dense domainsProved
Sep 2026
Group law transports under conjugationProved
Sep 2026
Restriction of the unitary is the unitaryProved
Sep 2026
Identity transports to identityProved
Sep 2026
Transported operator on a pulled vectorProved
Sep 2026
Transported group acts as conjugationProved
Sep 2026
Transported domain is the unitary imageProved
Sep 2026
Unitary maps commute with real scalarsProved
Sep 2026
Unitary maps pull inner products backProved
Sep 2026
The Lean 4 theorem `sirk_error_bound_antitone` in the `ChapterH6` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `Vexp_continuous` in the `ChapterSchrodingerCutoffEsa` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `reduce_generator_mul_m` in the `ChapterH6` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `sirk_bands_tendsto_zero` in the `ChapterH8` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `hashimoto_multishift_selects_esa` in the `ChapterEsaClosure` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `qgScalaron_stone_flow` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `fiberSumHam_stone_flow` in the `ChapterBddBelowFiberSumEsa` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `fiberSumHam_essentiallySelfAdjoint_of_bddBelow` in the `ChapterBddBelowFiberSumEsa` chapter of the timepiece formalizationProved
Sep 2026
Card (4,7,8) Fin560 w70hProved
Sep 2026
Card (4,7,8) Fin560 w70gProved
Sep 2026
Card (4,7,8) Fin560 w70fProved
Sep 2026
Card (4,7,8) Fin560 w70eProved
Sep 2026
Card (4,7,8) Fin560 w70dProved
Sep 2026
Card (4,7,8) Fin560 w70cProved
Sep 2026
Card (4,7,8) Fin560 w70bProved
Sep 2026
Card (4,7,8) Fin560 w70Proved
Sep 2026
Card triple (6,7,8) of units covers Z/15ZProved
Sep 2026
The Lean 4 theorem `wallHam_deficiencyTrivialAt` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved
Sep 2026
Card triple (8,7,6) of units covers Z/15ZProved
Sep 2026
Card triple (8,7,2) of units covers Z/15ZProved
Sep 2026
Card triple (8,6,7) of units covers Z/15ZProved
Sep 2026
Card triple (8,2,7) of units covers Z/15ZProved
Sep 2026
Card triple (7,8,6) of units covers Z/15ZProved
Sep 2026
Card triple (7,6,8) of units covers Z/15ZProved
Sep 2026
Card triple (7,8,2) of units covers Z/15ZProved
Sep 2026
Card triple (6,8,7) of units covers Z/15ZProved
Sep 2026
The Lean 4 theorem `fiberSumHam_nonneg_form` in the `ChapterBddBelowFiberSumEsa` chapter of the timepiece formalizationProved
Sep 2026
Card triple (2,8,7) of units covers Z/15ZProved
Sep 2026
Card triple (2,7,8) of units covers Z/15ZProved
Sep 2026
The Lean 4 theorem `fiberSumHam_semibounded` in the `ChapterBddBelowFiberSumEsa` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `krylov_bestApprox_tendsto_zero` in the `ChapterH9` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `scalaronEdge_friedrichs_gap` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `starobinskyEdge_quadForm` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `starobinskyEdge_form_gap` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `starobinskyEdge_quadForm_eq` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `wallHam_nonneg_form` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `starobinskyEdge_inner_eq` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `wallHamBddBelow_semibounded` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `wave_essentiallySelfAdjoint` in the `ChapterStrichartzWave` chapter of the timepiece formalizationProved
Sep 2026
The Lean 4 theorem `kinCcR_quadratic_form` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved
Sep 2026

Posted 50

Group law transports under conjugationProved
Sep 2026
Unitaries send dense domains to dense domainsProved
Sep 2026
Symmetry transports along a unitaryOpen
Sep 2026
Strong continuity transportsProved
Sep 2026
Restriction of the unitary is the unitaryProved
Sep 2026
Adjoint domain is the unitary imageProved
Sep 2026
Unitary maps commute with real scalarsProved
Sep 2026
Identity transports to identityProved
Sep 2026
Transported operator on a pulled vectorProved
Sep 2026
Transported domain is the unitary imageProved
Sep 2026
Transported group acts as conjugationProved
Sep 2026
Unitary maps pull inner products backProved
Sep 2026
Friedrichs extension exists with no boundDefinition
Sep 2026
Resolvent converse is a positive self-adjoint extensionDefinition
Sep 2026
Densitized mode Hamiltonian is essentially self-adjointDefinition
Sep 2026
Fibrewise essential self-adjointness gluesDefinition
Sep 2026
Card (4,7,8) Fin560 w70hProved
Sep 2026
Card (4,7,8) Fin560 w70gProved
Sep 2026
Card (4,7,8) Fin560 w70fProved
Sep 2026
Card (4,7,8) Fin560 w70eProved
Sep 2026
Card (4,7,8) Fin560 w70dProved
Sep 2026
Card (4,7,8) Fin560 w70cProved
Sep 2026
Card (4,7,8) Fin560 w70bProved
Sep 2026
Card (4,7,8) Fin560 w70Proved
Sep 2026
Essential self-adjointness for potentials bounded belowDefinition
Sep 2026
Weak second-derivative regularity lemmasDefinition
Sep 2026
Card triple (8,7,6) of units covers Z/15ZProved
Sep 2026
Card triple (8,7,2) of units covers Z/15ZProved
Sep 2026
Card triple (8,6,7) of units covers Z/15ZProved
Sep 2026
Card triple (8,2,7) of units covers Z/15ZProved
Sep 2026
Card triple (7,8,6) of units covers Z/15ZProved
Sep 2026
Card triple (7,8,2) of units covers Z/15ZProved
Sep 2026
Card triple (7,6,8) of units covers Z/15ZProved
Sep 2026
Card triple (6,8,7) of units covers Z/15ZProved
Sep 2026
Card triple (6,7,8) of units covers Z/15ZProved
Sep 2026
Card triple (2,8,7) of units covers Z/15ZProved
Sep 2026
Card triple (2,7,8) of units covers Z/15ZProved
Sep 2026
Card (8,4,7) Fin560 w70hProved
Sep 2026
Card (8,4,7) Fin560 w70gProved
Sep 2026
Card (8,4,7) Fin560 w70fProved
Sep 2026
Card (8,4,7) Fin560 w70eProved
Sep 2026
Card (8,4,7) Fin560 w70dProved
Sep 2026
Card (8,4,7) Fin560 w70cProved
Sep 2026
Card (8,4,7) Fin560 w70bProved
Sep 2026
Card (8,4,7) Fin560 w70Proved
Sep 2026
Card (7,5,8) Fin448 w56hProved
Sep 2026
Card (7,5,8) Fin448 w56gProved
Sep 2026
Card (7,5,8) Fin448 w56fProved
Sep 2026
Card (7,5,8) Fin448 w56eProved
Sep 2026
Card (7,5,8) Fin448 w56dProved
Sep 2026