Closure under absorption of half-factors
ProvedFiniteSplitGibbsMethodsII.halfFactorClosureLet be split data with finite , and let . Replacing by gives
If every , the coefficients remain nonnegative because they are unchanged. Separately, if and are pointwise nonnegative, then is pointwise nonnegative. No pointwise positivity conclusion is asserted without the sign condition on .
import Definitions.Def_FiniteSplitGibbsMethodsII open FiniteSplitGibbsMethodsII
theorem FiniteSplitGibbsMethodsII.halfFactorClosure :
HalfFactorClosureGate := by sorryRead-back
What the Lean code literally says, in plain math · gpt-5
For every universe-level-0 pair of types , every finite enumeration of , every function , and every split-weight datum on indexed by , let the absorbed datum keep 's coefficients and replace each feature by . Then all three of the following hold: for every , its associated weight is exactly ; if for every , then every coefficient of the absorbed datum is nonnegative; and if for every and for every , then the absorbed datum's associated weight is nonnegative for every . No finiteness assumption is made on , and the third assertion has no coefficient-sign hypothesis. If is empty, coefficient quantifiers are vacuous; if is empty, every pointwise statement over is vacuous.
Confirmed by the mission captain (proposal self-audit).