Corpus v3 · Formal theorem
cid005308
FTH0046canonicalv1crt_extension_b (theorem)
/-- [I.L08] CRT Extension: tower coherence constrains function output via the reduce map. The output at stage k is always reduced mod primorial k — this is the vertical consistency that enables extension. For the B-sector: reduce(f.b_fun(n, l), k) = f.b_fun(n, k) for k ≤ l. -/
Formalization
lean_axiom_freesorries: 0project axioms: 0
Identifiers
Aliases & legacy IDs
crt_extension_bcrt-extension-bTauLib.BookI.Holomorphy.Thinness::crt_extension_bRelease lines
corpus_v2corpus_v3_workingVersion & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.