is — Recognition explainer

formal statement (Lean)

 388structure is cleanest. The combinatorial extension is mechanical
 389and adds no RS-relevant content. The `n`-agent statement is the
 390right next file: `MechanismDesignFromSigmaGeneralN.lean`.
 391-/
 392
 393end MechanismDesignFromSigma
 394end GameTheory
 395end IndisputableMonolith

used by (40)

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

optimalT60 in IndisputableMonolith.Acoustics.RoomAcousticsSabineFromJCost decl_use
hearingLossPenalty in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
hearingLossPenalty_zero in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
energyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
christoffel in IndisputableMonolith.Action.EulerLagrange decl_use
const_one_is_geodesic in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_iff_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_implies_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
geodesicEquationHolds in IndisputableMonolith.Action.EulerLagrange decl_use
geodesic_iff_hessianEnergy_EL in IndisputableMonolith.Action.EulerLagrange decl_use
actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
energy_conservation in IndisputableMonolith.Action.Hamiltonian decl_use
hamiltonPDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
newtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
NewtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
spaceShift in IndisputableMonolith.Action.Noether decl_use
spaceTranslationFlow in IndisputableMonolith.Action.Noether decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
timeShift in IndisputableMonolith.Action.Noether decl_use
timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
actionJ_def in IndisputableMonolith.Action.PathSpace decl_use
const_apply in IndisputableMonolith.Action.PathSpace decl_use
fixedEndpoints_trans in IndisputableMonolith.Action.PathSpace decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
next in IndisputableMonolith.RRF.Hypotheses.EightTick decl_use