Proposition-valued final assembly [connes-000J]

✍️source

theoremAtheoremA

L∃∀NAGENTDRAFTED

Keep final assembly proposition-valued. Section 7 combines previously proved endpoints. It does not accept a broad record containing the desired conclusion as a field. This “certificate isolation” makes #print axioms meaningful and lets semantic review trace each conjunct to the file where its mathematics occurs.

The nonisomorphism conjunct is stated directly as the absence of a multiplicative equivalence, \(\neg \operatorname {Nonempty}(\Gamma _1\simeq \Gamma _2)\), rather than through a project-local synonym. This is Lean's standard expression for the absence of a group isomorphism, so the result proved in Section 6 can be used directly.

The same assembly pattern applies when a linear paper proof crosses topology, analysis, finite computation, and algebraic transport: export small propositions from those layers, then combine them only at the theorem boundary.