abbrev definition def or abbrev

`sigma`

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

formal statement (Lean)

 173abbrev sigma (k : ℕ) : ArithmeticFunction ℕ := ArithmeticFunction.sigma k

proof body

Definition body.

used by (40)

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

canonicalRecognitionCostSystem in IndisputableMonolith.Algebra.CostAlgebra decl_use
RecognitionCostSystem in IndisputableMonolith.Algebra.CostAlgebra decl_use
encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
decodeCoeff in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
decodeMag in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
voxelStep_foldPlusOne_encodeIndex in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D decl_use
within3Sigma in IndisputableMonolith.Constants.ExternalAnchors decl_use
withinSigma in IndisputableMonolith.Constants.ExternalAnchors decl_use
band_excludes_falsifier in IndisputableMonolith.Cosmology.DarkMatterCrossSectionBound decl_use
DarkMatterCrossSectionCert in IndisputableMonolith.Cosmology.DarkMatterCrossSectionBound decl_use
alpha_over_pi_bounds in IndisputableMonolith.Cosmology.HubbleTension decl_use
AbileneParadoxCert in IndisputableMonolith.Decision.AbileneParadox decl_use
group_sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
group_sigma_cons in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma_abilene in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma_truthful in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma_truthfulGo in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma_truthfulStay in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma_preserving_consensual in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
valueFunctional in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
AgentState in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
automorphism_preserves_sigma in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
coupling_conserves_total in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
CrossLatticeTransform in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
love_changes_individual_sigma in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
love_equilibrates in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
loveOperator in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
SingleLatticeTransform in IndisputableMonolith.Ethics.LoveUniquenessDerivation decl_use
externalization in IndisputableMonolith.Ethics.MoralDebt decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

sigma in IndisputableMonolith.Decision.AbileneParadox decl_use