theorem other other

`sat_computation_time`

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

formal statement (Lean)

 233theorem sat_computation_time (n : ℕ) (hn : 0 < n) :
 234    ∃ (c : ℝ), c > 0 ∧
 235    (sat_eval_time n n : ℝ) ≤ c * n^(1/3 : ℝ) * Real.log n
 236-/
 237
 238/-- **Recognition time** for SAT output (documentation / TODO): Ω(n) due to balanced-parity encoding.
 239
 240Intended claim: By balanced-parity hiding, reading fewer than n bits is insufficient to determine
 241the SAT result. Any decoder reading a proper subset of the input bits will fail on at least
 242one pair of tapes that match on the observed bits but differ in the total parity (and thus
 243the result). -/
 244/-!

depends on (21)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
sat_eval_time in IndisputableMonolith.Complexity.CellularAutomata decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
balanced in IndisputableMonolith.Foundation.LedgerForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use