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)
160inductive ConstraintReason where
161 | zConservation -- Z is conserved; cannot duplicate patterns
162 | jUniqueness -- J is uniquely forced; cannot override cost structure
163 | costOfNothing -- J(0⁺) → ∞; cannot create from nothing
164 | boundaryDissolution -- Dissolution always thermodynamically available
165 deriving DecidableEq, Repr
166
167/-- Each constrained power has a specific conservation-law reason. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
power
in IndisputableMonolith.Cosmology.PrimordialSpectrum
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use