landauFactsStub
plain-language theorem explainer
landauFactsStub supplies a stub instance of the LandauCompositionFacts hypothesis class inside the relativity fixtures module. It lets asymptotic arguments that rely on big-O composition with arbitrary functions proceed without a verified proof of the property. The definition is a one-line wrapper that directly discharges the goal by exact application of the input hypothesis, serving as a placeholder to keep sorries out of production code.
Claim. A noncomputable definition that instantiates the hypothesis class asserting composition bounds for big-O notation: for functions $f,g,h : ℝ → ℝ$ and point $a ∈ ℝ$, if $f = O(g)$ at $a$ then $h ∘ f = O(h ∘ g)$ at $a$.
background
The module Relativity.NewFixtures supplies stub instances for hypothesis classes introduced to replace sorries, keeping them outside production namespaces to maintain a clear trust boundary. LandauCompositionFacts is the class from the Landau analysis module whose single field encodes the required composition property for big-O relations. The upstream theorem bigO_comp_continuous states the same property as a placeholder: if $f = O(g)$ at $a$ then $h(f(x)) = O(h(g(x)))$ at $a$ for any $h$.
proof idea
The definition constructs the instance by setting the bigO_comp_continuous field to a tactic block that introduces the variables f, g, h, a and the hypothesis hf, then applies exact to discharge the goal directly from hf.
why it matters
This definition completes the stub setup for LandauCompositionFacts, allowing relativity arguments that depend on asymptotic composition bounds to compile without unresolved sorries. It supports the fixtures layer that bridges analytic tools to the Recognition Science forcing chain (T0–T8) and the Recognition Composition Law by keeping placeholder hypotheses isolated. The open question it touches is the eventual replacement of the stub with a verified proof of the composition property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.