def definition def or abbrev

`main`

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

formal statement (Lean)

  98def main : IO Unit := do

proof body

Definition body.

  99  IO.println (exportPayload.pretty 2)

used by (23)

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

argon_ea_zero in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
galerkinNS_hasDerivAt_duhamelRemainder_mode in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
nsDuhamel_of_forall_kernelIntegral_of_forcing in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
consistent_completeStateFrom in IndisputableMonolith.Complexity.SAT.Completeness decl_use
Jcost_is_calibrated in IndisputableMonolith.CostUniqueness decl_use
main in IndisputableMonolith.CPM.AuditMain decl_use
P_forced_to_RCL in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
dalembert_deriv_ode in IndisputableMonolith.Foundation.DAlembert.FourthGate decl_use
xi_derived in IndisputableMonolith.Gravity.DerivedFactors decl_use
rar_power_law_emergence in IndisputableMonolith.Gravity.RAREmergence decl_use
dirichletForm_edgeArea in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use
bounded_Jcost_bounded_max in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
PhiLadderCutoffCert in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
six_almost_prime_threehundredfiftytwo in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use
linking_selection_principle in IndisputableMonolith.Papers.DraftV1 decl_use
eight_tick_compactification in IndisputableMonolith.Papers.GCIC.DiscreteGauge decl_use
endpoint_classification in IndisputableMonolith.Physics.StellarEvolution decl_use
radius_sublinear in IndisputableMonolith.Physics.StellarEvolution decl_use
riemann_lowered_pair_exchange in IndisputableMonolith.Relativity.Geometry.RiemannSymmetries decl_use
log_sum_inequality in IndisputableMonolith.Thermodynamics.FreeEnergyMonotone decl_use
main in IndisputableMonolith.URCAdapters.Audit decl_use
main in IndisputableMonolith.URCAdapters.Audit decl_use

depends on (3)

Lean names referenced from this declaration's body.

main in IndisputableMonolith.CPM.AuditMain decl_use
exportPayload in IndisputableMonolith.Exports.Virtues decl_use
main in IndisputableMonolith.URCAdapters.Audit decl_use