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)
54theorem cost_nonneg (e : RecognitionEvent) : 0 ≤ e.cost :=
proof body
Term-mode proof.
55 Cost.Jcost_nonneg e.state_pos
56
57/-- The canonical identity event sits at the J-cost minimum (`x = 1`). -/
used by (40)
From the project-wide theorem graph. These declarations reference this one in their body.
-
cert
in IndisputableMonolith.Acoustics.MusicPitchJNDFromJCost
decl_use
-
PitchJNDCert
in IndisputableMonolith.Acoustics.MusicPitchJNDFromJCost
decl_use
-
speechIntelligibilityCert
in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost
decl_use
-
SpeechIntelligibilityCert
in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost
decl_use
-
culturalAestheticCert
in IndisputableMonolith.Aesthetics.CulturalAestheticFromJCost
decl_use
-
CulturalAestheticCert
in IndisputableMonolith.Aesthetics.CulturalAestheticFromJCost
decl_use
-
cert
in IndisputableMonolith.Agronomy.YieldGapFromJCost
decl_use
-
YieldGapCert
in IndisputableMonolith.Agronomy.YieldGapFromJCost
decl_use
-
cert
in IndisputableMonolith.Architecture.GoldenSectionInProportion
decl_use
-
GoldenSectionCert
in IndisputableMonolith.Architecture.GoldenSectionInProportion
decl_use
-
attractorStructureCert
in IndisputableMonolith.Climate.AttractorStructure
decl_use
-
AttractorStructureCert
in IndisputableMonolith.Climate.AttractorStructure
decl_use
-
climatePredictabilityCert
in IndisputableMonolith.Climate.PredictabilityFromJCost
decl_use
-
ClimatePredictabilityCert
in IndisputableMonolith.Climate.PredictabilityFromJCost
decl_use
-
ignitionCert
in IndisputableMonolith.Combustion.IgnitionThresholdFromJCost
decl_use
-
IgnitionCert
in IndisputableMonolith.Combustion.IgnitionThresholdFromJCost
decl_use
-
cert
in IndisputableMonolith.CriminalJustice.RecidivismFromJCost
decl_use
-
RecidivismCert
in IndisputableMonolith.CriminalJustice.RecidivismFromJCost
decl_use
-
BraggAngleCert
in IndisputableMonolith.Crystallography.BraggAngleFromPhiLadder
decl_use
-
cert
in IndisputableMonolith.Crystallography.BraggAngleFromPhiLadder
decl_use
-
lorenzCurveCert
in IndisputableMonolith.Economics.LorenzCurveFromSigmaBudget
decl_use
-
LorenzCurveCert
in IndisputableMonolith.Economics.LorenzCurveFromSigmaBudget
decl_use
-
ZeroParameterFramework
in IndisputableMonolith.Foundation.ExclusivityProof
decl_use
-
observer_forcing_certificate
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
smLagrangianCert
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
SMLagrangianCert
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
cert
in IndisputableMonolith.Foundation.RecognitionLattice3
decl_use
-
RecogLattice3Cert
in IndisputableMonolith.Foundation.RecognitionLattice3
decl_use
-
cert
in IndisputableMonolith.InternationalRelations.PowerTransitionFromJCost
decl_use
-
PowerTransitionCert
in IndisputableMonolith.InternationalRelations.PowerTransitionFromJCost
decl_use
… and 10 more
depends on (16)
Lean names referenced from this declaration's body.
-
Jcost_nonneg
in IndisputableMonolith.Cost
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Cost.JcostCore
decl_use
-
canonical
in IndisputableMonolith.Foundation.ArithmeticOf
decl_use
-
RecognitionEvent
in IndisputableMonolith.Foundation.LedgerForcing
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
RecognitionEvent
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
canonical
in IndisputableMonolith.Gap45.Beat
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.CoherenceCollapse
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.EnergyProcessingBridge
decl_use
-
RecognitionEvent
in IndisputableMonolith.Information.InformationIsLedger
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Jcost_nonneg
in IndisputableMonolith.NavierStokes.PhiLadderCutoff
decl_use
-
canonical
in IndisputableMonolith.NavierStokes.RM2U.NonParasitism
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use