coneEntropyStub
plain-language theorem explainer
coneEntropyStub supplies a placeholder instance for the holographic entropy bound on light cones, allowing the inequality entropy(cone) ≤ area/(4 λ_rec²) to be invoked in relativity proofs. Researchers extending the recognition framework's cone export theorems would cite it to clear sorries while preserving a clear trust boundary. The implementation reduces the obligation to a parameter introduction followed by simplification.
Claim. A definition supplying an instance of the typeclass that asserts: for any type α, light cone cone over α, and real area, the entropy of the cone satisfies entropy(cone) ≤ area / (4 λ_rec²).
background
The module supplies stub instances for hypothesis classes introduced to replace sorries, keeping them outside production namespaces. ConeEntropyFacts is the placeholder class whose sole field is the bound entropy(cone) ≤ area / (4 λ_rec²) for light cones. The upstream cone_entropy_bound theorem states exactly this inequality under the assumption of the class, noting that a full proof would require voxel counting, ledger entropy ln φ per voxel, and the holographic principle.
proof idea
The definition is realized by introducing the parameters α, cone, and area, then applying the simp tactic. This constitutes a one-line wrapper that discharges the obligation without deriving the bound from voxel or ledger structure.
why it matters
The stub makes the cone entropy bound usable downstream in the relativity fixtures, directly supporting the instance that activates cone_entropy_bound. It fills the placeholder noted in the ConeExport theorem doc-comment, which flags the need for a derivation from holographic principles and the recognition length scale. The declaration touches the open question of discharging the entropy assumption via the phi-ladder or eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.