Registry · Proposition VII.P08 conjectural formalized

VII.P08 — Each Requirement Independently Necessary

Dropping any of the six requirements admits non-τ solutions; all six are independently necessary.

Book VII Part 2 Ch. 29

Dependency Graph

Depends on (2)

VII.D37 VII.T14

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.each_requirement_necessary