GAMUT

Research record — Published from the project repository. Each record states its own date, scope and evidence status.

Research records: Proof manifest

Checked discrete proof manifest

Generated from proof-manifest.json by python3 verify.py --write-docs; verification rejects drift. required-exports.txt is the independent 256-declaration acceptance inventory inherited from reviewed Tasks 2–6. Removing a JSON entry fails even if this document is regenerated.

All names below are exact Lean declarations, including definitions supporting the stated theorems. Sources are repository-relative paths at the recorded source-remediation commit; TeX labels/functions are durable anchors. The specification’s absolute baseline links and fingerprints are historical. General lemmas sometimes allow broader arithmetic domains than MusicalDomain; the declaration signatures are authoritative for each lemma.

The proof release covers F01–F10 and the §8 regressions only. Higher geometric manuscript derivations, runtime Python/visualizer behavior, published datasets, historical attribution and musical utility are excluded. See trust and validation and source correction ledger.

F01 — Domain and action laws

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: sec:seed.

Assumptions: Positive order size for finite content; pitch size positive where needed. MusicalDomain separately records 2 ≤ n and 1 ≤ k ≤ n.

Corrections and exclusions: Patterns are injective raw tuples; pitch T/I acts on values and rotations on indices. No repeated-note or audio bridge.

Required declarations:

  • GAMUT.Discrete.Content
  • GAMUT.Discrete.MusicalDomain
  • GAMUT.Discrete.Pattern
  • GAMUT.Discrete.TIEquivalent
  • GAMUT.Discrete.content
  • GAMUT.Discrete.contentAffine
  • GAMUT.Discrete.contentTISetoid
  • GAMUT.Discrete.content_card
  • GAMUT.Discrete.content_invert
  • GAMUT.Discrete.content_invert_ti
  • GAMUT.Discrete.content_nonempty
  • GAMUT.Discrete.content_rotate
  • GAMUT.Discrete.content_transpose
  • GAMUT.Discrete.content_transpose_ti
  • GAMUT.Discrete.invert
  • GAMUT.Discrete.invert_apply
  • GAMUT.Discrete.invert_invert
  • GAMUT.Discrete.invert_transpose
  • GAMUT.Discrete.mem_content
  • GAMUT.Discrete.pitchAffine
  • GAMUT.Discrete.pitchAffine_comp
  • GAMUT.Discrete.pitchAffine_inverse
  • GAMUT.Discrete.rotate
  • GAMUT.Discrete.rotate_add
  • GAMUT.Discrete.rotate_apply
  • GAMUT.Discrete.rotate_free
  • GAMUT.Discrete.rotate_zero
  • GAMUT.Discrete.ti_refl
  • GAMUT.Discrete.ti_symm
  • GAMUT.Discrete.ti_trans
  • GAMUT.Discrete.transpose
  • GAMUT.Discrete.transpose_add
  • GAMUT.Discrete.transpose_apply
  • GAMUT.Discrete.transpose_zero

F02 — Directed gap reconstruction

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: prop:gapreconstruction.

Assumptions: Positive k; closure in ZMod n and injective partial sums for admissibility.

Corrections and exclusions: Corrected iff includes equality of actual cyclic gaps to supplied gaps, including closing edge. Integer representatives need not sum to n; unsigned distances do not reconstruct.

Required declarations:

  • GAMUT.Discrete.AdmissibleGap
  • GAMUT.Discrete.existsUnique_pattern
  • GAMUT.Discrete.gap
  • GAMUT.Discrete.gap_admissible
  • GAMUT.Discrete.gap_sum_zero
  • GAMUT.Discrete.missing_closure_counterexample
  • GAMUT.Discrete.partialSum
  • GAMUT.Discrete.partialSum_rawGap
  • GAMUT.Discrete.partialSum_successor
  • GAMUT.Discrete.partialSum_zero
  • GAMUT.Discrete.patternEquivRootGap
  • GAMUT.Discrete.rawGap
  • GAMUT.Discrete.rawGap_reconstruct
  • GAMUT.Discrete.rawGap_sum_zero
  • GAMUT.Discrete.reconstruct
  • GAMUT.Discrete.reconstruct_gap
  • GAMUT.Discrete.reconstruct_injective_iff
  • GAMUT.Discrete.reconstruct_rawGap
  • GAMUT.Discrete.reconstruct_spec_iff
  • GAMUT.Discrete.reconstruct_zero
  • GAMUT.Discrete.repeated_pitch_not_injective
  • GAMUT.Discrete.singleton_admissible_iff
  • GAMUT.Discrete.singleton_gap
  • GAMUT.Discrete.sum_zmod_eq_range
  • GAMUT.Discrete.zero_gap_collision

F03 — Fiber counts

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: prop:rootedfibrecount.

Assumptions: Positive n,k; a fixed labeled S with card S=k; root r:S.

Corrections and exclusions: k! unrestricted, (k−1)! fixed-root and cyclic counts. No quotient by content stabilizer or unchosen T/I representative.

Required declarations:

  • GAMUT.Discrete.CyclicOrders
  • GAMUT.Discrete.Orderings
  • GAMUT.Discrete.RootedFiber
  • GAMUT.Discrete.antipodal_fiber_counts
  • GAMUT.Discrete.augmented_triad_fiber_counts
  • GAMUT.Discrete.augmented_triad_transposition_symmetry
  • GAMUT.Discrete.binary_full_fiber_counts
  • GAMUT.Discrete.cyclicOrdersEquivRooted
  • GAMUT.Discrete.cyclicOrders_card
  • GAMUT.Discrete.cyclicSetoid
  • GAMUT.Discrete.full_content_fiber_counts
  • GAMUT.Discrete.normalize
  • GAMUT.Discrete.normalize_rooted
  • GAMUT.Discrete.normalize_rotate
  • GAMUT.Discrete.orderingEquiv
  • GAMUT.Discrete.orderingRotate
  • GAMUT.Discrete.orderingRotate_add
  • GAMUT.Discrete.orderingRotate_zero
  • GAMUT.Discrete.orderings_card
  • GAMUT.Discrete.pointedEquiv
  • GAMUT.Discrete.rootIndex
  • GAMUT.Discrete.rootIndex_spec
  • GAMUT.Discrete.rootIndex_unique
  • GAMUT.Discrete.rootedEquiv
  • GAMUT.Discrete.rootedFiber_card
  • GAMUT.Discrete.rooted_rotation_unique
  • GAMUT.Discrete.singleton_fiber_counts

F04 — Fourier convention adapter

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: sec:content.

Assumptions: N:Nat with NeZero N; arbitrary complex signals.

Corrections and exclusions: Negative forward sign, inverse 1/N, faithful standard character. No floating-point verification.

Required declarations:

  • GAMUT.Discrete.asymmetric_four_autocorrelation
  • GAMUT.Discrete.asymmetric_four_power
  • GAMUT.Discrete.asymmetric_four_reversed_dft
  • GAMUT.Discrete.asymmetric_four_reversed_fails
  • GAMUT.Discrete.autocorrelation
  • GAMUT.Discrete.autocorrelation_one
  • GAMUT.Discrete.autocorrelation_pitchCharacter
  • GAMUT.Discrete.dft
  • GAMUT.Discrete.dft_formula
  • GAMUT.Discrete.dft_one
  • GAMUT.Discrete.dft_pitchCharacter
  • GAMUT.Discrete.dft_zero_signal
  • GAMUT.Discrete.inverse_dft_formula
  • GAMUT.Discrete.inverse_dft_one
  • GAMUT.Discrete.pitchCharacter
  • GAMUT.Discrete.pitchCharacter_conj
  • GAMUT.Discrete.pitchCharacter_injective
  • GAMUT.Discrete.pitchCharacter_unit
  • GAMUT.Discrete.power
  • GAMUT.Discrete.reversed_autocorrelation_pitchCharacter

F05 — Finite Wiener–Khinchin

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: thm:WKcontent; thm:WKorder.

Assumptions: N positive; arbitrary complex signal; real norm-square coerced to complex.

Corrections and exclusions: Autocorrelation conjugates the unshifted sample. Power determines autocorrelation, not general signal phase.

Required declarations:

  • GAMUT.Discrete.autocorrelation_eq_iff_power_eq
  • GAMUT.Discrete.autocorrelation_eq_inverse_power
  • GAMUT.Discrete.dft_autocorrelation

F06 — Content spectrum and invariance

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: thm:WKcontent; cor:contentinvariance.

Assumptions: Positive n; finite labeled content S (empty permitted by arithmetic helpers).

Corrections and exclusions: Homometry is equality of directed counts; ZRelated additionally excludes T/I. Content power is not a complete content-class invariant.

Required declarations:

  • GAMUT.Discrete.Homometric
  • GAMUT.Discrete.ZRelated
  • GAMUT.Discrete.contentAffine_true_eq
  • GAMUT.Discrete.contentAutocorrelation
  • GAMUT.Discrete.contentDFT
  • GAMUT.Discrete.contentDFT_invert
  • GAMUT.Discrete.contentDFT_neg
  • GAMUT.Discrete.contentDFT_transpose
  • GAMUT.Discrete.contentIndicator
  • GAMUT.Discrete.contentIndicator_conj
  • GAMUT.Discrete.contentIndicator_invert
  • GAMUT.Discrete.contentIndicator_transpose
  • GAMUT.Discrete.contentPower
  • GAMUT.Discrete.contentPower_invert
  • GAMUT.Discrete.contentPower_transpose
  • GAMUT.Discrete.content_autocorrelation_eq
  • GAMUT.Discrete.content_autocorrelation_inverse
  • GAMUT.Discrete.content_autocorrelation_neg
  • GAMUT.Discrete.content_autocorrelation_zero
  • GAMUT.Discrete.content_pair_count_sum
  • GAMUT.Discrete.content_power_ti_invariant
  • GAMUT.Discrete.content_ti_invariant
  • GAMUT.Discrete.content_wiener_khinchin
  • GAMUT.Discrete.homometric_iff_power_eq

F07 — Order reconstruction and symmetries

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: prop:orderinjective; thm:WKorder; prop:reindexing; prop:ordertransinv.

Assumptions: Positive n,k; injective Pattern n k; full complex order DFT.

Corrections and exclusions: Decoder is inverse on character image. Inversion conjugates and reverses spectral indices; magnitudes/projections do not reconstruct raw patterns.

Required declarations:

  • GAMUT.Discrete.decodePitch
  • GAMUT.Discrete.decodePitch_character
  • GAMUT.Discrete.dft_conj
  • GAMUT.Discrete.dft_shift
  • GAMUT.Discrete.orderPower_invert
  • GAMUT.Discrete.orderSignal
  • GAMUT.Discrete.orderSignal_decode
  • GAMUT.Discrete.orderSignal_injective
  • GAMUT.Discrete.orderSignal_inverse
  • GAMUT.Discrete.orderSpectrum
  • GAMUT.Discrete.orderSpectrum_injective
  • GAMUT.Discrete.orderSpectrum_invert
  • GAMUT.Discrete.orderSpectrum_rotate
  • GAMUT.Discrete.orderSpectrum_transpose
  • GAMUT.Discrete.order_autocorrelation_inverse
  • GAMUT.Discrete.order_wiener_khinchin

F08 — Layered injectivity and DC

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex.

Anchors: prop:layeredinjective / prop:embeddinginjective.

Assumptions: Positive n,k; fixed cardinality k for omitted content DC; full order coordinates retained.

Corrections and exclusions: Proves only injective-embedding part of introductory C. No symplectic reduction, preferred geometry, perception or utility theorem.

Required declarations:

  • GAMUT.Discrete.LayeredCoordinates
  • GAMUT.Discrete.contentDFT_nonzero_injective_of_card
  • GAMUT.Discrete.contentDFT_zero
  • GAMUT.Discrete.contentIndicator_injective
  • GAMUT.Discrete.contentSpectrum
  • GAMUT.Discrete.contentSpectrum_nonzero_injective_of_card
  • GAMUT.Discrete.contentSpectrum_zero
  • GAMUT.Discrete.layered
  • GAMUT.Discrete.layered_injective
  • GAMUT.Discrete.nonzero_content_coordinate_card

F09 — Certified twelve-tone census

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex, visualization_handoff_pack/python/layered_bundle_visualization_starter.py.

Anchors: sec:seed; visualization generator canonical_set and enumerate_pcset_classes.

Assumptions: Exactly Finset (ZMod 12), affine transposition/inversion action, exact 12-bit masks.

Corrections and exclusions: 224 classes including empty; 223 nonempty; size vector 1,1,6,12,29,38,50,38,29,12,6,1,1. No Forte labels, all Z-pairs, JSON or sampled-fiber certification. Numeric-mask minima may differ from the visualizer’s lexicographic representatives; only orbit equivalence is compared.

Required declarations:

  • GAMUT.Discrete.CensusQuotient12
  • GAMUT.Discrete.CensusRepresentatives12
  • GAMUT.Discrete.Mask12
  • GAMUT.Discrete.NonemptyTIClasses12
  • GAMUT.Discrete.TIClasses12
  • GAMUT.Discrete.affineMask12
  • GAMUT.Discrete.affineMask12Nat
  • GAMUT.Discrete.affineMask12_bit
  • GAMUT.Discrete.affineMask12_bound
  • GAMUT.Discrete.canonical12
  • GAMUT.Discrete.canonical12_eq_iff_ti
  • GAMUT.Discrete.canonical12_le_of_ti
  • GAMUT.Discrete.canonical12_ti
  • GAMUT.Discrete.canonicalMask12
  • GAMUT.Discrete.canonicalMask12Nat
  • GAMUT.Discrete.canonicalMask12_card
  • GAMUT.Discrete.canonicalMask12_idempotent
  • GAMUT.Discrete.canonicalMask12_singleton_check
  • GAMUT.Discrete.canonicalMask12_spec
  • GAMUT.Discrete.censusContentSetoid12
  • GAMUT.Discrete.censusQuotient12_card
  • GAMUT.Discrete.censusQuotient12_count
  • GAMUT.Discrete.censusQuotientEquiv12
  • GAMUT.Discrete.censusRepresentativeCount12
  • GAMUT.Discrete.censusRepresentativeCount12_all
  • GAMUT.Discrete.censusRepresentativeCount12_by_size
  • GAMUT.Discrete.censusRepresentativeCount12_certificate
  • GAMUT.Discrete.censusRepresentativeCount12_nonempty
  • GAMUT.Discrete.decode12
  • GAMUT.Discrete.decode12_affine
  • GAMUT.Discrete.decode12_bijective
  • GAMUT.Discrete.decode12_encode
  • GAMUT.Discrete.decode12_encodeExecutable
  • GAMUT.Discrete.decode12_injective
  • GAMUT.Discrete.decode12_nonempty_iff
  • GAMUT.Discrete.decode12_unique
  • GAMUT.Discrete.decode12_zero
  • GAMUT.Discrete.encode12
  • GAMUT.Discrete.encode12Executable
  • GAMUT.Discrete.encode12Executable_eq
  • GAMUT.Discrete.encode12_decode
  • GAMUT.Discrete.fixedMaskCertificate12
  • GAMUT.Discrete.fixedMaskCertificate12_exact
  • GAMUT.Discrete.foldMinPair_attained12
  • GAMUT.Discrete.foldMinPair_le_acc12
  • GAMUT.Discrete.foldMinPair_le_mem12
  • GAMUT.Discrete.mask12Equiv
  • GAMUT.Discrete.mask12_highBit
  • GAMUT.Discrete.mem_fixedMaskCertificate12
  • GAMUT.Discrete.nonemptyCanonicalMasks12
  • GAMUT.Discrete.nonemptyCanonicalMasks12_card
  • GAMUT.Discrete.nonemptyCanonicalMasks12_eq
  • GAMUT.Discrete.nonemptyTIClasses12Equiv
  • GAMUT.Discrete.nonemptyTIClasses12_card
  • GAMUT.Discrete.numericMaskCertificate12
  • GAMUT.Discrete.numericMaskCertificate12_bound
  • GAMUT.Discrete.numericMaskCertificate12_exact
  • GAMUT.Discrete.reflectMask12
  • GAMUT.Discrete.reflectMask12_bit
  • GAMUT.Discrete.reflectMask12_bound
  • GAMUT.Discrete.rotateMask12
  • GAMUT.Discrete.rotateMask12_bit
  • GAMUT.Discrete.testBit_ite_zero12
  • GAMUT.Discrete.tiClasses12Equiv
  • GAMUT.Discrete.tiClasses12_card
  • GAMUT.Discrete.tiClasses12_card_by_size
  • GAMUT.Discrete.ti_card12

F10 — Histogram adapters and exact regressions

Status: kernel-checked. Source commit: 8bd538b.

Sources: assets/Amsart/layered_symplectic_musical_space_amsart.tex, assets/Proof/layered_symplectic_musical_space.tex, MusicalEncodings/rmcp/src/rmcp/homometry.py.

Anchors: sec:content; RMCP interval_vector, cyclic_autocorrelation, homometric, gap_word.

Assumptions: Distinct twelve-tone content sets; d=1..5 for nonantipodal identity; d=6 separately.

Corrections and exclusions: F=2IV; A(0)=card S; A(6)=2IV(6). Mathematical adapter only, no verified Python binding. Gap multiset does not determine pair distances.

Required declarations:

  • GAMUT.Discrete.S0137
  • GAMUT.Discrete.S0146
  • GAMUT.Discrete.all_interval_tetrachord_histograms12
  • GAMUT.Discrete.antipodal_histograms12
  • GAMUT.Discrete.binary_musical_domains
  • GAMUT.Discrete.circularDistance12
  • GAMUT.Discrete.circularDistance12_lag
  • GAMUT.Discrete.circularDistance12_swap
  • GAMUT.Discrete.directedVector12
  • GAMUT.Discrete.foldedHistogram12
  • GAMUT.Discrete.foldedHistogram12_eq_twice_intervalVector
  • GAMUT.Discrete.foldedHistogram12_nonantipodal
  • GAMUT.Discrete.foldedVector12
  • GAMUT.Discrete.gap_multiset_exact12
  • GAMUT.Discrete.gap_multiset_not_pair_distance12
  • GAMUT.Discrete.intervalVector12
  • GAMUT.Discrete.intervalVector12_antipodal
  • GAMUT.Discrete.intervalVector12_directed_bridge
  • GAMUT.Discrete.intervalVector12_reconstruct
  • GAMUT.Discrete.intervalVector12_zero
  • GAMUT.Discrete.p0136
  • GAMUT.Discrete.p0146
  • GAMUT.Discrete.pairDistanceMultiset12
  • GAMUT.Discrete.pair_distance_multisets_exact12
  • GAMUT.Discrete.singleton_histograms12
  • GAMUT.Discrete.tetrachords_homometric
  • GAMUT.Discrete.tetrachords_not_ti
  • GAMUT.Discrete.tetrachords_zRelated
  • GAMUT.Discrete.traversalGapMultiset12
  • GAMUT.Discrete.unorderedVector12

Specification §8 regression map

  • smallest domains: GAMUT.Discrete.binary_musical_domains, GAMUT.Discrete.singleton_fiber_counts, GAMUT.Discrete.binary_full_fiber_counts, GAMUT.Discrete.full_content_fiber_counts.
  • invalid raw tuples and words: GAMUT.Discrete.repeated_pitch_not_injective, GAMUT.Discrete.zero_gap_collision, GAMUT.Discrete.missing_closure_counterexample.
  • singleton and closing edge: GAMUT.Discrete.singleton_gap, GAMUT.Discrete.singleton_admissible_iff, GAMUT.Discrete.rawGap_reconstruct, GAMUT.Discrete.existsUnique_pattern.
  • root counts and symmetric content: GAMUT.Discrete.rootedFiber_card, GAMUT.Discrete.cyclicOrders_card, GAMUT.Discrete.rotate_free, GAMUT.Discrete.antipodal_fiber_counts, GAMUT.Discrete.augmented_triad_fiber_counts, GAMUT.Discrete.augmented_triad_transposition_symmetry.
  • Fourier N=1, zero and asymmetric conjugation: GAMUT.Discrete.dft_one, GAMUT.Discrete.inverse_dft_one, GAMUT.Discrete.autocorrelation_one, GAMUT.Discrete.dft_zero_signal, GAMUT.Discrete.asymmetric_four_power, GAMUT.Discrete.asymmetric_four_reversed_fails.
  • content phase and inversion; order reversal: GAMUT.Discrete.contentDFT_transpose, GAMUT.Discrete.contentDFT_invert, GAMUT.Discrete.contentDFT_neg, GAMUT.Discrete.orderSpectrum_invert.
  • histogram zero, antipode and all-interval set: GAMUT.Discrete.intervalVector12_zero, GAMUT.Discrete.intervalVector12_antipodal, GAMUT.Discrete.intervalVector12_reconstruct, GAMUT.Discrete.singleton_histograms12, GAMUT.Discrete.antipodal_histograms12, GAMUT.Discrete.all_interval_tetrachord_histograms12.
  • nontrivial Z witness and gap counterexample: GAMUT.Discrete.tetrachords_homometric, GAMUT.Discrete.tetrachords_not_ti, GAMUT.Discrete.tetrachords_zRelated, GAMUT.Discrete.gap_multiset_exact12, GAMUT.Discrete.pair_distance_multisets_exact12, GAMUT.Discrete.gap_multiset_not_pair_distance12.
  • census empty, singleton, full and stabilizers: GAMUT.Discrete.canonicalMask12_singleton_check, GAMUT.Discrete.decode12_nonempty_iff, GAMUT.Discrete.tiClasses12_card_by_size, GAMUT.Discrete.nonemptyTIClasses12_card, GAMUT.Discrete.canonical12_eq_iff_ti.