structure definition def or abbrev

`required`

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

formal statement (Lean)

  96structure required to even *state* these conditions. -/

used by (40)

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

actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
abs_heatFactor_le_one in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
main_resolution in IndisputableMonolith.Complexity.ComputationBridge decl_use
P_vs_NP_resolved in IndisputableMonolith.Complexity.ComputationBridge decl_use
bandwidthBudget_succ in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
npWorkload_succ in IndisputableMonolith.Complexity.PvsNPFromBIT decl_use
xorMissing in IndisputableMonolith.Complexity.SAT.Backprop decl_use
hbar_eq_phi_inv_fifth in IndisputableMonolith.Constants decl_use
tau0_pos in IndisputableMonolith.Constants decl_use
k_R_pos in IndisputableMonolith.Constants.BoltzmannConstant decl_use
thermal_energy_at_unit_T in IndisputableMonolith.Constants.BoltzmannConstant decl_use
eleven_is_passive_edges in IndisputableMonolith.Constants.SolidAngleExclusivity decl_use
Lambda_not_planck_scale in IndisputableMonolith.Cosmology.CosmologicalConstantDerivation decl_use
implications in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
washburn_uniqueness in IndisputableMonolith.Cost.FunctionalEquation decl_use
EntropicCooling in IndisputableMonolith.Energy.VacuumPump decl_use
CQAligned in IndisputableMonolith.Ethics.CostModel decl_use
anomaly_magnitude_small in IndisputableMonolith.Experimental.FlybyAnomaly decl_use
coherence_variation in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
ea011_certificate in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
no_fine_tuning in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
axion_coupling_small in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
ea006_certificate in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
further_data_needed in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
neutrino_disfavored in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
neutrino_moment_sm in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
EEGFalsification in IndisputableMonolith.Experiments.Protocols decl_use
RCLCombiner_isCoupling_iff in IndisputableMonolith.Foundation.BranchSelection decl_use
gates_consistent in IndisputableMonolith.Foundation.DAlembert.TriangulatedProof decl_use

… and 10 more