theorem
proved
cone_bound_export
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ConeExport.Theorem on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
30
31/-- Verification-level cone bound: if per-step bounds hold, any `n`-step reach obeys
32 `rad y - rad x ≤ U.c * (time y - time x)` with no `n` in the statement. -/
33theorem cone_bound_export
34 (H : LightCone.StepBounds K U time rad)
35 {n x y} (h : Causality.ReachN K n x y) :
36 rad y - rad x ≤ U.c * (time y - time x) := by
37 simpa using (LightCone.StepBounds.cone_bound (K:=K) (U:=U) (time:=time) (rad:=rad) H h)
38
39end
40
41/-- Cone entropy bound: Entropy in a cone is bounded by area over 4 λ_rec².
42
43 This is currently an axiom (typeclass assumption). A full proof would require:
44 - Voxel counting: number of voxels ~ area / λ_rec²
45 - Entropy per voxel: ~ ln φ from ledger structure
46 - Holographic principle: caps total at area/(4λ_rec²)
47
48 See docs/Assumptions.md for the status of this assumption.
49-/
50theorem cone_entropy_bound {α : Type _} (cone : LightCone α) (area : ℝ)
51 [ConeEntropyFacts] :
52 entropy cone ≤ area / (4 * λ_rec^2) :=
53 ConeEntropyFacts.cone_entropy_bound cone area
54
55end ConeExport
56end IndisputableMonolith