admissible — Recognition explainer

formal statement (Lean)

  35def admissible (_s : LedgerState) : Prop := True

proof body

Definition body.

  36
  37/-- A local dissipative recognition operator for information thermodynamics. -/

used by (40)

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

const_one_is_geodesic in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_implies_const_one 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
Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_const_one in IndisputableMonolith.Action.PathSpace 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
admissibleFlows in IndisputableMonolith.Algebra.RecognitionCategory decl_use
IsConservedFlow in IndisputableMonolith.Algebra.RecognitionCategory decl_use
LedgerAlgObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
BWD3Model in IndisputableMonolith.Complexity.SAT.BWD3SchurPinch decl_use
feasible_implies_boolean in IndisputableMonolith.Complexity.SAT.BWD3SchurPinch decl_use
LinearFeasible in IndisputableMonolith.Complexity.SAT.BWD3SchurPinch decl_use
satisfiable_iff_linearFeasible in IndisputableMonolith.Complexity.SAT.BWD3SchurPinch decl_use
unique_cost_on_pos_from_rcl in IndisputableMonolith.CostUniqueness decl_use
ECDLPInstance in IndisputableMonolith.Cryptography.ECDLPWatch decl_use
sigmaCost_ordering in IndisputableMonolith.Decision.NewcombParadox decl_use
composeGenerators_preserves in IndisputableMonolith.Ethics.Virtues.FiniteLatticeEnumeration decl_use
fifteenth_generator_required_iff_not_rich in IndisputableMonolith.Ethics.Virtues.SigmaPreservingProof decl_use
toNat_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
combiner_unit_diagonal in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
PublicCostLayer in IndisputableMonolith.Foundation.DimensionalConstraints.CostLayer decl_use
four_canonical_domains_admissible in IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass decl_use
eight_tick_dissipation_limit in IndisputableMonolith.Information.Thermodynamics decl_use
RecognitionOperator in IndisputableMonolith.Information.Thermodynamics decl_use
rungResidueClass in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
gapCost_mono in IndisputableMonolith.Mathematics.RamanujanBridge.PhiLadderStability decl_use

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
LedgerState in IndisputableMonolith.Foundation.VariationalDynamics decl_use
LedgerState in IndisputableMonolith.Information.InformationIsLedger decl_use
LedgerState in IndisputableMonolith.Information.Thermodynamics decl_use
LedgerState in IndisputableMonolith.LedgerPostingAdjacency decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
LedgerState in IndisputableMonolith.QFT.GaugeInvariance decl_use