leonardopedro

Solved 50

• The Lean 4 theorem `wallHam_symmetricOn` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `kinCcR_quadratic_form` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `kinCcR_symmetricOn` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `field_evaluates_to_value_diagonal` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edge_energy_bound` 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 `edge_sup_sq_le` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `fiberSumHam_essentiallySelfAdjoint_of_nonneg` in the `ChapterBddBelowFiberSumEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `starobinskyV_lt_shelf_bounded` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edge_re_mul_le` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edge_normSq_hasDerivAt` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edgeShelf_pos` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edgeMassConst_pos` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `edgeKinConst_pos` in the `ChapterScalaronEdge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `intertwined_pos` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `intertwined_mom` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `intertwined_cre` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `intertwined_ann` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ell2ShiftInvert_isSelfAdjoint` in the `ChapterHashimotoShiftInvert` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `secondDerivativeField_momentum` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `derivativeField_momentum` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `dense_range_add_relBounded` in the `ChapterKatoRellichRelative` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsWord_length_le_three` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsHamiltonian_ne_zero_example` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsDivergenceConstraint_resolution` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `lagrangian_velocity` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `velIdx_apply` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `wave_indefiniteQuadratic_essentiallySelfAdjoint` in the `ChapterHyperbolicQuadraticEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `minkowski_apply_eq_differential` in the `ChapterHyperbolicQuadraticEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sqrtTwo_mul_self` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsDiffH_domain_dense` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `embedCore_coe` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `crd_coreState` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `core_ext` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `isUniformInducing_toComplL` in the `ChapterFriedrichsExtension` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `incl_apply` in the `ChapterFriedrichsExtension` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `starobinskyV_essentiallySelfAdjoint` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `smoothPotential_essentiallySelfAdjoint` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `wave_add_smoothPotential_symmetric` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `waveCc_symmetric` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `starobinskyWall_stone_flow` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `starobinskyWall_esa` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `wallHam_essentiallySelfAdjoint` in the `ChapterScalaronWallEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ccEquiv_norm_sq` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `spectrum_compress_subset_numRange_compress` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `contDiff_scalaronFullPotential` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ccDomain_dense` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `spectrum_compress_subset_numRange` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `symmetricOn_inclusion` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `starobinskyV_not_hasTemperateGrowth` in the `ChapterScalaronCoreEsa` chapter of the timepiece formalizationProved

  Sep 2026

Posted 50

• The Lean 4 theorem `qgKappa_spatial_pos` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `torsionPoly_antisymm` in the `ChapterQuantumGravity3DGauge` 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 `realCoeff_torsionPoly` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qgKappaElliptic_nonneg` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qg3DDensity_singular` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qgKappa_conformal_neg` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `idxX_ne_idxDE` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qg3DDensity_densitized` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `idxX_ne_idxE` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `idxX_injective` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `idxE_injective` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `idxE_ne_idxDE` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qgOuterN_esa` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationOpen

  Sep 2026

• The Lean 4 theorem `idxDE_injective` in the `ChapterQuantumGravity3DGauge` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sum_reindex_particles` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `qgOuterCore_dense` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationOpen

  Sep 2026

• The Lean 4 theorem `pcoord_partOf_modeOf` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sum_single_block` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `modeOf_pcoord` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `dsOp_quadForm_nonneg` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationOpen

  Sep 2026

• The Lean 4 theorem `qgOuterN_symmetricOn` in the `ChapterQgOuterFockEsa` chapter of the timepiece formalizationOpen

  Sep 2026

• The Lean 4 theorem `partOf_pcoord` in the `ChapterQgOuterFockEsa` 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 `sirk_error_bound_antitone` in the `ChapterH6` 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

• Outer Fock space for the quantum gravity Faris-Lavine programmeDefinition

  Sep 2026

• Chapter ChapterQymTimeIndependentFlowDefinition

  Sep 2026

• 3D gauge ESA definitionsDefinition

  Sep 2026

• ChapterQuantumGravity3DGaugeDefinition

  Sep 2026

• ChapterWallEsaBddBelowDefinition

  Sep 2026

• The Lean 4 theorem `kinetic_posSemidef` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsHamiltonian_hermitian` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ns_outer_degree_le_two` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsNumberOp_posSemidef` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `isShiftInvert_invShiftOperator` in the `ChapterHashimotoShiftInvert` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `symmetric_hasZeroDeficiency` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsNumberOp_eq_secondQuant` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ns_esa_of_farisLavine_dense` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `restrictToTop_apply` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsBrst_nilpotent` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ns_esa_of_farisLavine` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsBrst_adjoint` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsFlow_zero` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsHamiltonian_isPolynomial` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `field_evaluates_to_value` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsFlow_group` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `farisLavine_without_symmetry_forces_trivial` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `nsAdvection_hermitian` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `hasZeroDeficiencyOn_top_of_symmetric` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026