def definition def or abbrev

`value`

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

formal statement (Lean)

  79noncomputable def value (s : Spin) : ℝ := s.twice / 2

proof body

Definition body.

  80
  81/-- Is this a half-integer spin (fermion)? -/

used by (40)

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

geodesic_minimizes_via_convexity in IndisputableMonolith.Action.FunctionalConvexity decl_use
coe_mk in IndisputableMonolith.Action.PathSpace decl_use
card_eq_seven in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
defectDist_nonneg in IndisputableMonolith.Algebra.CostAlgebra decl_use
shiftedComposeH_val in IndisputableMonolith.Algebra.CostAlgebra decl_use
ShiftedHValue in IndisputableMonolith.Algebra.CostAlgebra decl_use
LedgerEvent in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
GeometricStrain in IndisputableMonolith.Applied.CoherenceTechnology decl_use
rs_neutral_pattern in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
J_bit in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_derivation_complete in IndisputableMonolith.Astrophysics.MassToLight decl_use
ml_derived in IndisputableMonolith.Astrophysics.MassToLight decl_use
three_strategies_agree in IndisputableMonolith.Astrophysics.MassToLight decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
PhiTier in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
ml_stellar in IndisputableMonolith.Astrophysics.StellarAssembly decl_use
alphaInv_dimensionless in IndisputableMonolith.Bridge.GaugeVsParams decl_use
PhysicalCertificate in IndisputableMonolith.Certificates.Standard decl_use
RealCertificate in IndisputableMonolith.Certificates.Standard decl_use
ammoniaAnglePrediction in IndisputableMonolith.Chemistry.BondAngles decl_use
Enzyme in IndisputableMonolith.Chemistry.EnzymeCatalysis decl_use
ionizationProxy in IndisputableMonolith.Chemistry.IonizationEnergy decl_use
hack_exponent_pos in IndisputableMonolith.Climate.RiverNetworkFromSigmaConservation decl_use
moat_zero_sat in IndisputableMonolith.Complexity.CircuitLedger decl_use
flipBit_other in IndisputableMonolith.Complexity.JCostLaplacian decl_use
varDegree in IndisputableMonolith.Complexity.JCostLaplacian decl_use
BPState in IndisputableMonolith.Complexity.SAT.Backprop decl_use
compatible_setVar in IndisputableMonolith.Complexity.SAT.Backprop decl_use
known_lit_false'' in IndisputableMonolith.Complexity.SAT.Backprop decl_use
list_singleton_of_length_one' in IndisputableMonolith.Complexity.SAT.Backprop decl_use

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.

half in IndisputableMonolith.QFT.SpinStatistics decl_use
Spin in IndisputableMonolith.QFT.SpinStatistics decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
half in IndisputableMonolith.Support.RungFractions decl_use