FirstPaperFeasibility.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic tests for the positive small-profile state space

Feasibility is decided by coordinate bounds, the allowed local pattern, and residual margin equations. No completion count is evaluated.

lemma OAI.ContingencyTables.SmallGraphProfiles.supported_completion_nonempty line 23

Source documentation

Equal residual totals and zero margins outside a rectangle suffice for a supported completion, including empty row or column types.

lemma supported_completion_nonempty (small : I → J → Bool)
    (p : I → Prop) (q : J → Prop)
    (hrect : ∀ i j,small i j=false ↔ p i ∧ q j)
    (R : I → ℕ) (C : J → ℕ) (ht : (∑ i,R i)=∑ j,C j)
    (hR : ∀ i,¬p i → R i=0) (hC : ∀ j,¬q j → C j=0) :
    Nonempty (LargeCompletion small R C) := by
…

def OAI.ContingencyTables.SmallGraphProfiles.profileRows line 55
Source documentation
Padded residual margins can be computed before establishing feasibility.
```
def profileRows (z : SmallProfile small) (i : I) : ℕ :=
…
```
def OAI.ContingencyTables.SmallGraphProfiles.profileColumns line 58
structure OAI.ContingencyTables.SmallGraphProfiles.ProfileFeasible line 62
Source documentation
Each field is a finite integer test on the candidate profile.
```
structure ProfileFeasible (z : SmallProfile small) : Prop where
…
```
lemma OAI.ContingencyTables.SmallGraphProfiles.profile_capacity line 71
lemma OAI.ContingencyTables.SmallGraphProfiles.physicalProfile_feasible line 75
lemma OAI.ContingencyTables.SmallGraphProfiles.profileFeasible_positive line 86
Source documentation
A passing arithmetic test constructs a completion by the greedy rectangle algorithm, proving that its weight is strictly positive.
```
lemma profileFeasible_positive (z : SmallProfile small) (h : ProfileFeasible r c z) :
    0 < hardMarginal small B r c L z := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.ProfileFeasible
def OAI.ContingencyTables.SmallGraphProfiles.stateOfFeasible line 98
Source documentation
The successful integer tests recover an actual state without searching the completion space.
```
def stateOfFeasible (z : SmallProfile small) (h : ProfileFeasible r c z) : PaperStates r c :=
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.ProfileFeasible, OAI.ContingencyTables.SmallGraphProfiles.PaperStates
lemma OAI.ContingencyTables.SmallGraphProfiles.stateOfFeasible_profile line 102
theorem OAI.ContingencyTables.SmallGraphProfiles.profileFeasible_iff line 106
Source documentation
This is the complete test for membership in the chain's state space.
```
theorem profileFeasible_iff (z : SmallProfile small) :
    ProfileFeasible r c z ↔ ∃ x : PaperStates r c,physicalProfile small B r c L x=z := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.ProfileFeasible, OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.physicalProfile
def OAI.ContingencyTables.SmallGraphProfiles.decodeProfile line 116
Source documentation
Failed candidates are discarded. Passing candidates retain all completion multiplicity through the original physical state type.
```
def decodeProfile (z : SmallProfile small) : Option (PaperStates r c) :=
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates
lemma OAI.ContingencyTables.SmallGraphProfiles.decodeProfile_eq_some_iff line 119