Registry · Proposition V.P11 tau-effective formalized

V.P11 — Gap refinement coherence

The total gap element is invariant under refinement: Delta_tot^(n+1) = Delta_tot^(n) as elements of the omega-germ completion. The refined inner sum over p_{n+1}/p_n subarcs at depth n+1 reproduces the coarser gap at depth n.

Book V Part 2 Ch. 11

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookV.GravityField.FrameHolonomy

Symbol: Tau.BookV.GravityField.GapRefinementCoherence