PreprocessingFamilyBridge.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact serialized family tables at actual regularization vertices

The geometric family maps request zero to a one-vertex table. Empty clouds in regularization instead remain empty. The bridge therefore requires positive cloud size, derived here from each actual original or dummy vertex.

theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.rotationWords_resizeTable line 21
Source documentation
Transporting only the size equality leaves every serialized rotor entry unchanged; no relabeling or alternative numbering is introduced.
```
theorem rotationWords_resizeTable {n m q : Nat} (h : n = m)
    (table : ExpanderTables.Table n q) :
    rotationWords (resizeTable h table) = rotationWords table := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.ExpanderTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.familyRotor_eq_familyCloudTable line 30
Source documentation
This left side is definitionally the output MachineRegularFamily.rotor for the request on its physical core tape 4. The right side is exactly the archive expected on core tape 7 by the internal-row machine.
```
theorem familyRotor_eq_familyCloudTable (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (hk : 0 < cloudSize t v) :
    encodeWords (rotationWords (ExpanderTables.family H
      (PreprocessingLevels.boundedLevel (cloudSize t v)))) =
      encodeWords (rotationWords (familyCloudTable H t v)) := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table, OAI.MaxCutGames.Foundations.PCP.ExpanderTables.family, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dart line 41
Source documentation
An actual original dart supplies a member of its owner's cloud.
```
theorem cloudSize_pos_of_dart (t : GraphTables.Table) (e : Fin t.darts) :
    0 < cloudSize t t.rows[e].tail := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.padding_zero_of_cloudSize_zero line 47
Source documentation
An empty cloud has no padding vertices either.
```
theorem padding_zero_of_cloudSize_zero (t : GraphTables.Table) (v : Fin t.vertices)
    (hk : cloudSize t v = 0) : padding t v = 0 := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dummy line 52
Source documentation
Every actual dummy vertex also belongs to a positive original cloud.
```
theorem cloudSize_pos_of_dummy (t : GraphTables.Table) (v : Fin t.vertices)
    (j : Fin (padding t v)) : 0 < cloudSize t v := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_paddedCloud line 61
Source documentation
The same positivity fact for the common local coordinate interface.
```
theorem cloudSize_pos_of_paddedCloud (t : GraphTables.Table) (v : Fin t.vertices)
    (x : PaddedCloud t (padding t) v) : 0 < cloudSize t v := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingFamilyBridge.familyCloudWords_of_zero line 71
Source documentation
The zero-cloud branch remains genuinely empty, including its serialized rotor archive. It is not replaced by the geometric family at request zero.
```
theorem familyCloudWords_of_zero (H : BaseTable) (t : GraphTables.Table)
    (v : Fin t.vertices) (hk : cloudSize t v = 0) :
    encodeWords (rotationWords (familyCloudTable H t v)) = [] := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.GraphTables.Table