module module

`IndisputableMonolith.Verification.QuarkSectorAudit`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (13)

inductive QuarkConvention L64
structure UnifiedQuarkSector L70
def currentStatus L83
structure ConventionA_Rungs L91
structure ConventionB_Residues L100
theorem different_references L109
theorem different_rung_types L116
theorem generation_spacing_differs L130
def light_quark_accuracy L135
def skeleton_only_accuracy L140
structure ReconciliationProof L148
theorem no_reconciliation_yet L159
theorem quark_problem_blocks_full_verdict L166