SymmetricChoice.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.RelF line 11
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_relation line 14
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.rel_left_congr line 26
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.WitnessIndex line 39
Source documentation
A small index set of precisely the domain-entry/condition pairs for which there is a local symmetric witness.
```
def WitnessIndex {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+2)) :=
…
```
Mentions: OAI.PartitionConsistency.Formula
instance OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.(instance at line 42) line 42
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.chosenWitness line 48
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.chosenWitness_spec line 51
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.replacementBound line 63
Source documentation
An orbit-closed bound for one Replacement problem. Instead of a uniform name-rank cutoff, take the whole set-group orbit of the ground-chosen local witnesses. This set is invariant and is still small. No symmetric maximum principle, global rank cutoff, or on-condition selection is used.
```
noncomputable def replacementBound {n} (σ : S.Name) (v : Fin n → S.Name)
    (φ : Formula (n+2)) : S.Name :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.witness_in_bound line 70
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.bounded_local_witness line 79
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ImageF line 87
Source documentation
The dense local meaning of ∃x∈σ, φ(x,y).
```
def ImageF {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+2))
    (p : P) (ν : S.Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.SingleValuedF line 93
Source documentation
Ordinary internal single-valuedness, expressed via forcing at every stronger condition.
```
def SingleValuedF {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+2)) (p : P) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.image_in_bound line 97
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.imageFormula line 116
Source documentation
The image predicate, with the set-domain as one extra parameter, retaining all quantifiers of the original formula.
```
def imageFormula {n} (φ : Formula (n+2)) : Formula (n+2) :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_imageFormula line 122
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.replacementImage line 133
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_replacementImage line 137
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.TotalFunctionalF line 145
Source documentation
The antecedent of a Replacement instance: totality with local unique witnesses, exactly as supplied by the existential forcing clause.
```
def TotalFunctionalF {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+2)) (p : P) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.singleValued_of_totalFunctional line 151
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_replacement line 164
Source documentation
Every full Replacement instance is forced. The bound depends on the particular domain, formula, and parameter tuple, and not on a prechosen class of name ranks.
```
theorem forces_replacement {n} (φ : Formula (n+2)) (p : P) :
    S.Forces Fin.elim0 p (SetLanguage.replacement φ) := by
…
```
Mentions: OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.SetLanguage.replacement
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_ZF line 206
Source documentation
Full ZF in the concrete hereditary-symmetry interpretation. The quantifier domain is the unbounded class of all HS names. Each schema instance is proved by its own actual set-name, including unrestricted Separation and Replacement.
```
theorem forces_ZF (p : P) : ∀ φ ∈ SetLanguage.ZF, S.Forces Fin.elim0 p φ := by
…
```
Mentions: OAI.PartitionConsistency.SetLanguage.ZF