TauLib · API Book II

TauLib.BookII.Mirror.Inventory

TauLib.BookII.Mirror.Inventory

The rewiring table: a complete inventory of the 12 structural sign-changes between orthodox and tau approaches.

Registry Cross-References

  • [II.D72] The Rewiring Table – RewiringRow, full_rewiring_table, rewiring_table_complete

Mathematical Content

II.D72 (The Rewiring Table): The rewiring table is the definitive inventory of Part XI. Each row records one sign level, the orthodox choice, the tau equivalent, and the structural trade-off. The table has exactly 12 rows, one for each sign level in the classification (II.D68).

The table serves as a reading guide: for each row, the reader can trace the change from orthodox to tau and understand the structural reason for the switch. The trade-offs are not arbitrary – they are forced by the foundational choices (K0-K6 axioms, prime polarity, split-complex scalars).

Part XI summary statistics:

  • 7 definitions (D68-D74)

  • 4 theorems (T43-T46)

  • This inventory module

Tau.BookII.Mirror.RewiringRow

source structure Tau.BookII.Mirror.RewiringRow :Type

[II.D72] A single row of the rewiring table: one sign level, the orthodox choice, the tau equivalent, and the trade-off.

  • level : SignLevel
  • orthodox : String
  • tau_equiv : String
  • tradeoff : String Instances For

Tau.BookII.Mirror.instReprRewiringRow

source instance Tau.BookII.Mirror.instReprRewiringRow :Repr RewiringRow

Equations

  • Tau.BookII.Mirror.instReprRewiringRow = { reprPrec := Tau.BookII.Mirror.instReprRewiringRow.repr }

Tau.BookII.Mirror.instReprRewiringRow.repr

source def Tau.BookII.Mirror.instReprRewiringRow.repr :RewiringRow → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Mirror.full_rewiring_table

source def Tau.BookII.Mirror.full_rewiring_table :List RewiringRow

[II.D72] The full rewiring table: all 12 rows. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Mirror.rewiring_table_complete

source theorem Tau.BookII.Mirror.rewiring_table_complete :full_rewiring_table.length = 12

[II.D72] The rewiring table has exactly 12 rows.

Tau.BookII.Mirror.row_orthodox_nonempty

source def Tau.BookII.Mirror.row_orthodox_nonempty (r : RewiringRow) :Bool

Each row has a nonempty orthodox description. Equations

  • Tau.BookII.Mirror.row_orthodox_nonempty r = decide (r.orthodox.length > 0) Instances For

Tau.BookII.Mirror.row_tau_nonempty

source def Tau.BookII.Mirror.row_tau_nonempty (r : RewiringRow) :Bool

Each row has a nonempty tau description. Equations

  • Tau.BookII.Mirror.row_tau_nonempty r = decide (r.tau_equiv.length > 0) Instances For

Tau.BookII.Mirror.row_tradeoff_nonempty

source def Tau.BookII.Mirror.row_tradeoff_nonempty (r : RewiringRow) :Bool

Each row has a nonempty trade-off description. Equations

  • Tau.BookII.Mirror.row_tradeoff_nonempty r = decide (r.tradeoff.length > 0) Instances For

Tau.BookII.Mirror.all_orthodox_rows_nonempty

source theorem Tau.BookII.Mirror.all_orthodox_rows_nonempty :full_rewiring_table.all row_orthodox_nonempty = true

All orthodox descriptions are nonempty.

Tau.BookII.Mirror.all_tau_rows_nonempty

source theorem Tau.BookII.Mirror.all_tau_rows_nonempty :full_rewiring_table.all row_tau_nonempty = true

All tau descriptions are nonempty.

Tau.BookII.Mirror.all_tradeoff_rows_nonempty

source theorem Tau.BookII.Mirror.all_tradeoff_rows_nonempty :full_rewiring_table.all row_tradeoff_nonempty = true

All trade-off descriptions are nonempty.

Tau.BookII.Mirror.table_levels

source def Tau.BookII.Mirror.table_levels :List SignLevel

Extract the sign levels from the rewiring table. Equations

  • Tau.BookII.Mirror.table_levels = List.map Tau.BookII.Mirror.RewiringRow.level Tau.BookII.Mirror.full_rewiring_table Instances For

Tau.BookII.Mirror.table_levels_match

source theorem Tau.BookII.Mirror.table_levels_match :table_levels = allSignLevels

The table levels match the canonical sign level list.

Tau.BookII.Mirror.table_covers_all_levels

source theorem Tau.BookII.Mirror.table_covers_all_levels :table_levels.length = allSignLevels.length

The table covers all sign levels (same length and same elements).

Tau.BookII.Mirror.part_xi_definitions

source def Tau.BookII.Mirror.part_xi_definitions :ℕ

Part XI definition count (D68-D74). Equations

  • Tau.BookII.Mirror.part_xi_definitions = 7 Instances For

Tau.BookII.Mirror.part_xi_theorems

source def Tau.BookII.Mirror.part_xi_theorems :ℕ

Part XI theorem count (T43-T46). Equations

  • Tau.BookII.Mirror.part_xi_theorems = 4 Instances For

Tau.BookII.Mirror.part_xi_total_entries

source def Tau.BookII.Mirror.part_xi_total_entries :ℕ

Part XI total formal entries. Equations

  • Tau.BookII.Mirror.part_xi_total_entries = Tau.BookII.Mirror.part_xi_definitions + Tau.BookII.Mirror.part_xi_theorems Instances For

Tau.BookII.Mirror.part_xi_entry_count

source theorem Tau.BookII.Mirror.part_xi_entry_count :part_xi_total_entries = 11

Part XI has 11 formal entries total.

Tau.BookII.Mirror.part_xi_modules

source def Tau.BookII.Mirror.part_xi_modules :ℕ

Part XI module count. Equations

  • Tau.BookII.Mirror.part_xi_modules = 4 Instances For

Tau.BookII.Mirror.part_xi_module_count

source theorem Tau.BookII.Mirror.part_xi_module_count :part_xi_modules = 4

Four modules in Part XI.

Tau.BookII.Mirror.table_12

source theorem Tau.BookII.Mirror.table_12 :full_rewiring_table.length = 12

Tau.BookII.Mirror.rows_orthodox

source theorem Tau.BookII.Mirror.rows_orthodox :full_rewiring_table.all row_orthodox_nonempty = true

Tau.BookII.Mirror.rows_tau

source theorem Tau.BookII.Mirror.rows_tau :full_rewiring_table.all row_tau_nonempty = true

Tau.BookII.Mirror.rows_tradeoff

source theorem Tau.BookII.Mirror.rows_tradeoff :full_rewiring_table.all row_tradeoff_nonempty = true

Tau.BookII.Mirror.levels_match

source theorem Tau.BookII.Mirror.levels_match :table_levels = allSignLevels