Additive Descent Defect Chain Law

Abstract

Additive descent defects obey the composition chain law.

Theorem 1.1 (Additive defects compose by a chain law).

$$\begin{array}{r}\forall X,Y,Z,B_C,B_D,B_E:\mathrm{Type},\\ [\mathrm{AddGroup}\left(B_D\right)],[\mathrm{AddGroup}\left(B_E\right)],\\ F:X\to Y,G:Y\to Z,\\ q_C:\mathrm{Concept}\left(X,B_C\right),q_D:\mathrm{Concept}\left(Y,B_D\right),q_E:\mathrm{Concept}\left(Z,B_E\right),\\ \overline{F}:B_C\to B_D,\overline{G}:\mathrm{AddMonoidHom}\left(B_D,B_E\right),\\ {\epsilon }_F=(q_D\circ F-\overline{F}\circ q_C),\\ {\epsilon }_G=(q_E\circ G-\overline{G}\circ q_D),\\ {\epsilon }_{GF}=(q_E\circ G\circ F-\overline{G}\circ \overline{F}\circ q_C),\\ \forall u,v\in B_D,\overline{G}(u+v)=\overline{G}(u)+\overline{G}(v),\\ {\epsilon }_{GF}={\epsilon }_G\circ F+\overline{G}\circ {\epsilon }_F.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Sufficiency/AdditiveDescentDefectChainLaw.additive_descent_defect_chain_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public definitions construct epsilon_F, epsilon_G, and epsilon_GF from the three readouts, two processes, and candidate macroscopic maps before the theorem relates those named objects.

The source declares the second macroscopic map as an ordinary function, but the equation requires it to preserve addition and subtraction. Lean records that repair as an AddMonoidHom, and the displayed additivity equation makes the added scope explicit.

After unfolding the named defects, the intermediate macroscopic readout cancels and preservation of subtraction leaves the composite defect.

References

• Truth anchor: D5/S3/ConceptDynamics/Sufficiency/AdditiveDescentDefectChainLaw.additive_descent_defect_chain_law
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition