abbrev definition def or abbrev

`Chain`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  44abbrev Chain := Recognition.Chain

proof body

Definition body.

  45
  46/-- Re-export: Ledger for double-entry. -/

used by (40)

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

GradedLedger in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
Chain in IndisputableMonolith.Chain decl_use
chainFlux in IndisputableMonolith.Chain decl_use
Conserves in IndisputableMonolith.Chain decl_use
last in IndisputableMonolith.Chain decl_use
RecognitionStructure in IndisputableMonolith.Chain decl_use
T3_continuity in IndisputableMonolith.Chain decl_use
balance_determines_lambda in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_rec_is_forced in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
planck_gate_normalized in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
eta in IndisputableMonolith.Cosmology.Nucleosynthesis decl_use
Generator in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
separable_forces_additive in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
rcl_unconditional in IndisputableMonolith.Foundation.DAlembert.Unconditional decl_use
FrameworkConstraints in IndisputableMonolith.Foundation.ExclusivityProof decl_use
concrete_implies_no_alternatives in IndisputableMonolith.Foundation.InevitabilityEquivalence decl_use
E_coh_pos in IndisputableMonolith.Foundation.PhiForcing decl_use
J_cost_motivates_additive_composition in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
minimal_closure_sufficient in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
jcost_stationarity_implies_regge in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
selfAware_max_richness in IndisputableMonolith.Foundation.VoiceForcing decl_use
voice_berry_positive in IndisputableMonolith.Foundation.VoiceForcing decl_use
fibonacci_connection_explained in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
partial_weight_reduction in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
jacobi_variation_structural in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
n_s_at_55_from_jcost in IndisputableMonolith.Gravity.JCostInflaton decl_use
rs_exists_iff_zero_cost in IndisputableMonolith.Information.SimulationHypothesisStructure decl_use
current_chain_distinct in IndisputableMonolith.Masses.StepValueEnumeration decl_use
rh_from_composition_closure in IndisputableMonolith.NumberTheory.CompositionDivergence decl_use
defect_implies_zero_free in IndisputableMonolith.NumberTheory.WeakZeroFreeRegion decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

Chain in IndisputableMonolith.Chain decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Chain in IndisputableMonolith.Recognition decl_use