S — Recognition explainer

formal statement (Lean)

 133noncomputable def S (g : Metric) (ψ : RefreshField) (C_lag α : ℝ) : ℝ :=

proof body

Definition body.

 134  S_EH g + PsiAction g ψ C_lag α
 135
 136/-- GR-limit reduction: when C_lag = 0 and α = 0, the ψ-sector vanishes. -/

used by (40)

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

Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
isSpaceTranslationInvariant in IndisputableMonolith.Action.Noether decl_use
isTimeTranslationInvariant 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
time_translation_invariance_implies_energy_conservation in IndisputableMonolith.Action.Noether decl_use
const_apply in IndisputableMonolith.Action.PathSpace decl_use
newton_first_law in IndisputableMonolith.Action.QuadraticLimit decl_use
octave_loop_neutrality in IndisputableMonolith.Applied.CoherenceTechnology decl_use
RSNSBridgeSpec in IndisputableMonolith.ClassicalBridge.Fluids.Bridge decl_use
Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
CircuitZCapacity in IndisputableMonolith.Complexity.CircuitLedger decl_use
Gate in IndisputableMonolith.Complexity.CircuitLedger decl_use
clause_unchanged_by_flip in IndisputableMonolith.Complexity.JCostLaplacian decl_use
laplacian_form_zero_imp in IndisputableMonolith.Complexity.JCostLaplacian decl_use
parityOf in IndisputableMonolith.Complexity.SAT.XOR decl_use
Covers in IndisputableMonolith.Complexity.VertexCover decl_use
Covers_nil_edges in IndisputableMonolith.Complexity.VertexCover decl_use
EdgeCovered in IndisputableMonolith.Complexity.VertexCover decl_use
EdgeCovered_comm in IndisputableMonolith.Complexity.VertexCover decl_use
HasCover in IndisputableMonolith.Complexity.VertexCover decl_use
InCover in IndisputableMonolith.Complexity.VertexCover decl_use
InCover_of_mem in IndisputableMonolith.Complexity.VertexCover decl_use
Instance in IndisputableMonolith.Complexity.VertexCover decl_use
alpha_seed_structural in IndisputableMonolith.Constants.AlphaDerivation decl_use
unitSphereSurface_D2 in IndisputableMonolith.Constants.SolidAngleExclusivity decl_use
Model in IndisputableMonolith.CPM.LawOfExistence decl_use
fromSubsetSum_isSolution in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
fromSubsetSum_totalJCost_zero in IndisputableMonolith.Cryptography.BalancedJSubsetSum decl_use
absLogVorticity in IndisputableMonolith.Flight.Medium decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Metric in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiAction in IndisputableMonolith.Relativity.ILG.Action decl_use
RefreshField in IndisputableMonolith.Relativity.ILG.Action decl_use
S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use