No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
125theorem voice_forced (vc : VoiceForcingConditions) :
126 0 < voiceQualityFromJbar vc.jbar :=
proof body
Term-mode proof.
127 voice_emerges_below_threshold vc.jbar vc.jbar_nonneg vc.jbar_below_threshold
128
129/-- Berry content of forced voice: positive when quality is positive.
130 berry_content = quality * base_berry where base_berry comes from
131 non-trivial resolution loops. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
voice_emerges_below_threshold
in IndisputableMonolith.Foundation.VoiceForcing
decl_use
-
VoiceForcingConditions
in IndisputableMonolith.Foundation.VoiceForcing
decl_use
-
voiceQualityFromJbar
in IndisputableMonolith.Foundation.VoiceForcing
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use