No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
13structure CARuntimeModel where
14 /-- Grid side length as a function of number of inputs n. -/
15 sideLength : ℕ → ℕ
16 /-- Assumption: side length is Θ(n^{1/3}). -/
17 sideLength_bound : ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧
18 ∀ n : ℕ, c₁ * (n : ℝ)^(1/3 : ℝ) ≤ (sideLength n : ℝ) ∧
19 (sideLength n : ℝ) ≤ c₂ * (n : ℝ)^(1/3 : ℝ)
20 /-- Locality: constraints are realized by gadgets of O(1) diameter (abstract). -/
21 locality : Prop
22
23/-- Logical propagation depth (number of implication layers). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
caTimeBound
in IndisputableMonolith.Complexity.SAT.Runtime
decl_use
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use