isFinerThan'_trans
plain-language theorem explainer
Transitivity of the finer-than relation on recognizers allows composition of refinement chains into a single directed system. Researchers constructing effective manifolds under the U2 refinement convergence hypothesis cite this result to justify monotone sequences indexed by natural numbers. The argument is a direct term-mode composition that applies the second refinement map to the output of the first.
Claim. If recognizer $r_1$ is finer than $r_2$ and $r_2$ is finer than $r_3$, then $r_1$ is finer than $r_3$, for recognizers $r_i$ over common base $C$ with event types $E_i$.
background
The EffectiveManifold module formalizes structural conditions under which directed refinements of recognition quotients produce an effective manifold, addressing open problems U1-U4 that correspond to Assumption 2.11 in the paper. IsFinerThan' is the refinement ordering on Recognizer objects; DirectedRefinement packages a monotone sequence of such recognizers indexed by ℕ. Upstream structures supply the J-cost convexity from PhysicsComplexityStructure, the active edge count A from IntegrationGap, and the spectral emergence of gauge content and generations from SpectralEmergence.
proof idea
The proof is a one-line term-mode wrapper: it feeds the output of the first hypothesis directly into the second hypothesis on identical inputs c₁, c₂, h. No auxiliary lemmas are applied; transitivity follows immediately from the functional definition of the IsFinerThan' predicate.
why it matters
The result is required by the DirectedRefinement structure that encodes the directed system for U2 refinement convergence. It supplies the transitivity needed to close chains in the effective-manifold hypothesis bundle, linking to the eight-tick octave and phi-ladder constructions elsewhere in the framework. Without it, monotone refinement sequences indexed by ℕ could not be assembled into a single limit object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.