lemma proved term proof

`self`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  60lemma self (φ : ℝ) : PhiClosed φ φ := by

proof body

Term-mode proof.

  61  change φ ∈ phiSubfield φ
  62  exact Subfield.subset_closure (by simp)
  63

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

phiInt_sq in IndisputableMonolith.Algebra.PhiRing decl_use
hack_exponent_pos in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation decl_use
log_bifurcation_eq_two_log_length in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation decl_use
riverNetworkCert in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation decl_use
satisfiesSystem in IndisputableMonolith.Complexity.SAT.XOR decl_use
tau0_pos in IndisputableMonolith.Constants decl_use
alphaLock_numerical_bounds in IndisputableMonolith.Constants.FineStructureConstant decl_use
w8_pos in IndisputableMonolith.Constants.GapWeight decl_use
J_exp_eq_cosh in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
dm_ratio_phi_connection in IndisputableMonolith.Cosmology.DarkMatter decl_use
ledgerShadowProperties in IndisputableMonolith.Cosmology.DarkMatter decl_use
dm_halo_from_ledger in IndisputableMonolith.Cosmology.GalaxyRotation decl_use
frequencyRatioCost_nonneg in IndisputableMonolith.Cost.FrequencyLadder decl_use
IsSelfSimilarRatio in IndisputableMonolith.Cost.FrequencyLadder decl_use
phi_cost_fixed_point in IndisputableMonolith.Cost.FrequencyLadder decl_use
phi_is_self_similar in IndisputableMonolith.Cost.FrequencyLadder decl_use
verifiedConstants in IndisputableMonolith.CPM.ConstantsAudit decl_use
HasConfigDim5 in IndisputableMonolith.CrossDomain.ConfigDimUniversality decl_use
biodiversityScalingCert in IndisputableMonolith.Ecology.BiodiversityScalingFromJCost decl_use
compression_has_cost in IndisputableMonolith.Flight.TeslaTurbine decl_use
tesla_turbine_master in IndisputableMonolith.Flight.TeslaTurbine decl_use
planck_mass_eq in IndisputableMonolith.Foundation.ConstantDerivations decl_use
FrameworkConstraints in IndisputableMonolith.Foundation.ExclusivityProof decl_use
Diverges in IndisputableMonolith.Foundation.GodelDissolution decl_use
general_self_ref_impossible in IndisputableMonolith.Foundation.GodelDissolution decl_use
GeneralSelfRefQuery in IndisputableMonolith.Foundation.GodelDissolution decl_use
GodelDissolutionTheorem in IndisputableMonolith.Foundation.GodelDissolution decl_use
RSOutside in IndisputableMonolith.Foundation.GodelDissolution decl_use
SelfRefQuery in IndisputableMonolith.Foundation.GodelDissolution decl_use
self_ref_query_impossible in IndisputableMonolith.Foundation.GodelDissolution decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

PhiClosed in IndisputableMonolith.RecogSpec.Core decl_use
phiSubfield in IndisputableMonolith.RecogSpec.Core decl_use