the book of the seed
the book of the seed (lean-only reading; the instrument reads terms, never prose)
the census [grown/Room.lean]: 167 declarations (26 carriers, 141 theorems), 141 receipts
the frontier [grown/Room.lean] — 18 leaves no organ in the house cites yet (read from the elaborator):
the_carrier_merges_only_the_alike
the_terminus_takes_every_carrier
the_held_name_their_darkness
the_still_map_carries
the_unencumbered_are_welcome
true_or_reads
the_rest_reads
a_merging_map_has_no_section
the_enrolled_stay_enrolled
the_seat_is_load_bearing_in_the_same_click
the_unenrolled_are_no_member
the_wear_is_a_reading
everyone_means_each
the_circle_stays_dark
the_book_is_the_answer_space
the_orbit_is_the_book
the_census_of_orders_is_exact
the_direction_is_even_money
cited only from above [grown/Room.lean] — 20 organs no organ of their own storey cites, seated by a storey that stands on it:
the_carriers_compose ← Face
the_first_mark_reads ← Face
eq_of_beq ← Face
filter_holds ← Face
mem_filter_intro ← Face
and_congr_first ← Face
and_congr_second ← Face
and_regroups ← Face
the_append_rests ← Face
beq_self ← Face
len_replicate ← Face
the_unit_word_is_its_count ← Face
ble_le_add_left ← Face
mul_spreads ← Face
ble_le_add ← Face
apart_filter ← Face
mul_one_reads ← Face
the_hallway_is_too_small ← Face
no_mark_lights_itself ← Face
the_key_is_cut_from_the_room ← Face
the census [grown/Face.lean]: 226 declarations (79 carriers, 147 theorems), 147 receipts
the frontier [grown/Face.lean] — 90 leaves no organ in the house cites yet (read from the elaborator):
the_interview_crosses_the_carrier
a_guest_blind_reading_is_a_face_reading
the_pairing_is_unique
any_ready_greeter_is_the_greeter
the_host_serves_both_branches
the_sharpening_is_exact
the_origin_is_the_pairs_unit
the_unheard_hands_compose
the_yield_fixes_the_agreed
the_window_agrees_or_names_the_gap
the_agreed_window_sounds_as_one
the_mutual_records_ride_together
the_gap_is_minted_at_the_meeting
one_face_many_seats
the_seat_map_carries_the_conduct
the_seats_stack_backward
the_ear_and_the_voice_commute
the_ear_crosses_the_seat
the_voice_crosses_the_seat
the_carrier_was_a_seating
the_obs_carries_to_the_one_face
no_face_reads_the_guest
the_guest_is_real
the_turn_returns
the_crossing_returns
hosting_associates
hosting_associates_back
the_branches_come_home
the_deferral_is_free
the_holding_returns
the_face_was_a_held_door
every_door_reading_is_a_face
the_measurement_is_a_meeting
the_host_was_a_reseat
the_probe_boards_as_the_guest
the_meeting_was_a_self_meeting
the_self_meeting_reads_the_guest
a_guest_mover_is_unheard
the_origin_merges_every_seat
the_still_hand_is_unheard
the_maintenance_is_the_identitys_hom
the_spoken_arrives_at_the_face
the_speaker_rides_unread
the_listening_turn_is_the_yield
the_two_listeners_restore_the_table
the_ode_comes_home
the_air_gap_wears_the_one_face
the_retuned_seat_walks_the_translated_word
the_pace_wears_the_tallys_voice
any_two_readings_agree
the_revision_is_a_reading
the_trivial_revision_changes_nothing
the_type_is_a_reading
the_customs_keep_the_still_world
the_customs_stack_forward
the_census_checksums_with_the_polygon_cutters
the_muffled_tally_is_the_resting_counter
the_lift_peeks_the_out
the_lift_feeds_the_step
the_unit_machine_steers_itself
the_comparison_mints_a_face
the_concord_reads_both_models
the_interview_crosses_the_seat
no_interview_parts_the_origin
the_manifest_is_natural
a_stage_may_ground_a_stage
lineages_compose
every_seat_is_a_reading_of_the_record
the_curtain_is_exact
the_revision_multiplies_the_reading
the_muffler_banks_the_run
the_rep_lands_where_it_is_fed
the_drained_is_on_spec
recording_the_recording_grounds
the_mutual_recording_is_unheard
two_seats_record_each_other
the_handshake
only_the_unheard_survives_the_sounding
correct_maintenance_has_no_signature
the_pace_is_carried_onto_the_flip
the_buffer_is_invisible
the_drain_settles
the_lift_is_the_conduct
the_concord_is_the_meetings_own
the_census_is_exact
the_clock_is_a_room
room_margin_flywheel_door
the_clock_writes_its_sequence
entanglement_is_the_loop
three_is_the_width_of_contact
cited only from above [grown/Face.lean] — 2 organs no organ of their own storey cites, seated by a storey that stands on it:
differOnly ← Witness
the_replay_is_the_machine ← Seek
the census [grown/Witness.lean]: 18 declarations (7 carriers, 11 theorems), 11 receipts
the frontier [grown/Witness.lean] — 8 leaves no organ in the house cites yet (read from the elaborator):
seat
a_narrower_seat_reads_no_more
the_seat_that_hears_it_reads_it
the_witness_parts_what_the_face_parts
the_room_is_the_widest_seat
the_witness_is_a_face
a_wall_at_the_witness
forever_hold_your_peace
the census [grown/Toy.lean]: 6 declarations (2 carriers, 4 theorems), 4 receipts
the frontier [grown/Toy.lean] — 4 leaves no organ in the house cites yet (read from the elaborator):
the_toy_counts
the_toy_parks
the_toy_resumes
the_toy_flips_back
the census [grown/Counter.lean]: 29 declarations (12 carriers, 17 theorems), 17 receipts
the frontier [grown/Counter.lean] — 16 leaves no organ in the house cites yet (read from the elaborator):
empty
a_name_reads_itself
the_first_sighting_is_free
a_backed_sighting_seats
an_unbacked_sighting_waits
the_seated_stay_seated
the_held_name_what_they_wait_on
weight_zero_is_backed
a_sighting_that_cites_only_itself_never_seats
two_sightings_that_cite_each_other_stay_dark
the_key_is_cut_from_the_room
a_sighting_is_load_bearing_in_the_same_round
the_gate_hears_only_the_receipt
the_vow_is_the_empty_receipt
a_receipt_keeping_rebody_is_unheard
the_verdict_survives_the_rebody
the census [grown/Seek.lean]: 11 declarations (2 carriers, 9 theorems), 9 receipts
the frontier [grown/Seek.lean] — 7 leaves no organ in the house cites yet (read from the elaborator):
a_failed_move_leaves_no_trace
a_closing_move_is_recorded
the_replay_is_the_search
the_audition_cannot_part_them
the_search_starts_empty
the_search_and_its_replay_are_alike
the_search_has_no_memory
the census [grown/Roster.lean]: 7 declarations (3 carriers, 4 theorems), 4 receipts
the frontier [grown/Roster.lean] — 2 leaves no organ in the house cites yet (read from the elaborator):
a_yes_reaches_the_sheet
reseating_keeps_the_sheets_count
the verbs [bin/counter]: 9 dispatched — what in the house runs each:
grow ← ci pages README CLAUDE.md page counter
probe ← README CLAUDE.md
book ← README CLAUDE.md page
shapes ← CLAUDE.md
gate ← ci README CLAUDE.md
chart ← README CLAUDE.md page
schema ← README CLAUDE.md page treaty
treaty ← ci README CLAUDE.md
page ← pages README
the frontier of verbs — 0 verbs nothing in the house runs but their own usage line:
the vestibule (typed vacancies, supports named):
[assays/eih.held]
-- the vestibule of EVERYONE IS HERE: the disagreements between the product as its team describes it
-- and the treaty as it stands, each a statement in the assay's own terms and the darkness it waits on.
-- a held statement seats when what it waits on arrives: the customer's word, a carrier, a reach of the
-- drawer's fragment, or a seating in the treaty's translator. read by bin/counter book.
-- the first round (2026-09-04, Abe's answers through isaac) seated six statements into the assay
-- (the_audience_hears_the_receipt_by_name, outside_the_audience_hears_no_receipt, the_sender_is_never_asked,
-- the_same_page_counts_only_within_earshot, the_payer_is_the_owner_or_the_host, edit_is_within_sight and
-- its two instances), refuted one (a member is a Membership; guests are never members; who can be asked is
-- the audience of the channel minus the sender), and left these.
-- Abe, in the room (2026-09-04): the day-of sheet is everyone's to edit with a memory, anyone opens a task and
-- only its owner, the couple, or the planner closes it — "yep that's great" — seated as
-- anyone_may_open_a_task and the_day_of_sheet_is_everyones_to_edit; the day lane's exclusion from tasks
-- still waits on lanes as a carrier, below.
-- the sixth round (the house's turn): Same page is a drawn sum — stated as a sum (List.sum over the
-- requests the viewer hears, mapped through tally) and read by the drawer as an aggregate, its two laws
-- re-proved over the filter; the season's total the same way, a face applied inside a lambda read as a
-- call to the face's function. a structural recursion (undo) and a pair-valued reading (venueTable) stay
-- beyond, and a list of lists (seasonView) is held as undrawn: the shadow holds no jagged array.
-- the seventh round (the house's turn): a lane is a member's sub-seat over the pages — memberSees subtracts
-- and never adds (lanes_shrink_never_lock, restated at the member), the day lane sees no task list and keeps
-- the day-of sheet, an edit is within the lane; the two page-number lists the assay carried since its first
-- day retired for the real thing.
-- the vestibule is empty (2026-09-04, isaac's move): the business, parked by Abe until a studio arrives,
-- cleared — if it is needed it comes back by being asked for; the repo does not remember on his behalf.
-- a held statement here is a disagreement between the customer's word and the treaty; today there is none.
the tense guard: this is the book, not the prediction — the choice is the rider's. 🤲